Hacktoberfest 2026：メンテナが10月に向けて印を付けた、オープンで初心者向けの issue。 Hacktoberfest の issue を見る

Remove `do` blocks from generated Lean code when possible

オープン
  • 何か問題がありますか？
#4,755 コメント 0 件 リアクション 0 件 担当者 0 名 GitHub で見る

まだ誰も着手していません。

評価

難易度
4/5
見積もり時間
3〜5日
初心者へのやさしさ
38/100
issue の種類
リファクタリング
明瞭さ
おおむね明確
活発さ
停滞
領域
compilers

調査の方向性

Start by locating the code-generation path that emits Lean function definitions, then inspect how Option-returning functions and their dependencies are represented. The change is complete when unnecessary do blocks are omitted, while blocks that chain Option-returning functions remain and dependent total functions can use non-Option signatures.

索引モデルが issue の本文から書いたものです。

説明

lean4-backend

The Lean generated code currently uses more do blocks for function definitions than strictly necessary, as an example

def _742a262 : SortScheduleConst → SortSchedule → Option SortInt
  | SortScheduleConst.Rb_SCHEDULE_ScheduleConst, SortSchedule.CONSTANTINOPLE_EVM => do
    let _Val0 <- «_*Int_» 2 1000000000000000000
    return _Val0
  | _, _ => none

could be defined as

def _742a262 : SortScheduleConst → SortSchedule → Option SortInt
  | SortScheduleConst.Rb_SCHEDULE_ScheduleConst, SortSchedule.CONSTANTINOPLE_EVM => «_*Int_» 2 1000000000000000000
  | _, _ => none

In particular, unless the do block is used to chain functions that return an Option type, it can be removed.

Additionally, functions which depend on total functions could be redefined without the do block once their dependencies are stripped of the Option return type. For example

def _432555e : SortWordStack → SortInt → Option SortInt
    | SortWordStack.«_:__EVM-TYPES_WordStack_Int_WordStack» _Gen0 WS, SIZE => do
      let _Val0 <- «_+Int_» SIZE 1
      let _Val1 <- sizeWordStackAux WS _Val0
      return _Val1
    | _, _ => none

Once «_+Int_» and sizeWordStackAux return a SortInt type instead of Option SortInt, it could be redefined as the following or similar

def _432555e : SortWordStack → SortInt → SortInt
    | SortWordStack.«_:__EVM-TYPES_WordStack_Int_WordStack» _Gen0 WS, SIZE =>
      let _Val0 := «_+Int_» SIZE 1
      sizeWordStackAux WS _Val0
    | _, _ => 0
主要言語
Python
スター
594
フォーク
164
30日以内にマージされた PR はありません

環境構築

はじめの一歩

  1. issue を最後まで読み、次にプロジェクトのコントリビューションガイドを読みます。
  2. 着手することを issue にコメントします — 二人が同じ作業をするのを防げます。
  3. リポジトリをフォークし、ブランチを切って変更します。
  4. issue 番号を参照したプルリクエストを送ります。

runtimeverification/k のほかの issue

runtimeverification/k の issue をすべて見る

似ている issue

Python の issue をもっと見る

新しい issue をメールで受け取る

初心者向けの GitHub issue を短くまとめたダイジェスト。