CLI fails silently on v4.30.0+ when using module system
まだ誰も着手していません。
評価
調査の方向性
リンクされた2コミットのMWEリポジトリから始め、v4.29.1とv4.30.0での動作を比較し、Main.leanとそのモジュール宣言に焦点を当てます。lean4-cliが公開されたmeta mainエントリポイントをどのように検出して呼び出すかを追跡します。モジュールベースのMain.leanが暗黙にno-opになるのではなく通常どおり実行され、既存のプレーンファイルの場合も引き続き動作すれば完了です。
索引モデルが issue の本文から書いたものです。
説明
Up to v4.29.1, it was possible to use the module system for the entry point of an executabl (Main.lean in the template lake projects). In v4.30.0 this will cause lean4-cli to fail silently resulting in a no-op when the executable is called.
Reproduction
I've created an MWE-repo with 2 commits, one working in v4.29.1 and one failing in v4.30.0:
https://github.com/joneugster/lean-cli-bug-demo/commits/main/
The key is that Main.lean contains
module
...
public meta def main (args : List String) : IO UInt32 :=
i18n.validate args
If module is removed from Main.lean turning it into a plain Lean file, it works again.
- 主要言語
- Lean
- スター
- 120
- フォーク
- 30
- 平均マージ
- 5分
- マージ済み PR（30日）
- 4
コントリビューションガイド
このリポジトリのコントリビューションガイドは索引されていません
はじめの一歩
- issue を最後まで読み、次にプロジェクトのコントリビューションガイドを読みます。
- 着手することを issue にコメントします — 二人が同じ作業をするのを防げます。
- リポジトリをフォークし、ブランチを切って変更します。
- issue 番号を参照したプルリクエストを送ります。
leanprover/lean4-cli のほかの issue
-
enhancement
難易度 5/5 1週間以上 初心者へのやさしさ 25/100
leanprover/lean4-cli#2 ·
leanprover/lean4-cli の issue をすべて見る
似ている issue
-
area: harness bug status: needs-triage
難易度 2/5 1〜3時間 初心者へのやさしさ 75/100
Human-Agent-Society/reef#625 ·
-
module: core
難易度 2/5 1〜3時間 初心者へのやさしさ 75/100
bigbluebutton/bigbluebutton#25849 ·
-
難易度 2/5 1〜3時間 初心者へのやさしさ 75/100
vercel-labs/just-bash#464 ·
-
難易度 2/5 1〜3時間 初心者へのやさしさ 75/100
-
area:sandbox documentation enhancement platform:linux
難易度 1/5 1時間未満 初心者へのやさしさ 85/100
anthropics/claude-code#96664 ·