CLI fails silently on v4.30.0+ when using module system
还没有人认领这个 Issue。
评估
调研方向
从链接的两次提交的 MWE repository 开始，比较它在 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
- 星标
- 121
- 派生
- 30
- 平均合并
- 5 分钟
- 30 天内合并 PR
- 4
环境准备
这个项目没有提供开发容器、Dockerfile 或贡献指南，环境需要你自己搭建：先看它的 README，通用步骤见我们的新手贡献指南。
从这里开始
- 先读完整个 Issue，再读项目的贡献指南。
- 在 Issue 下留言说明你要接手 —— 这能避免两个人做同样的事。
- Fork 仓库，在一个分支上完成修改。
- 提交 Pull Request，并在描述里引用这个 Issue 编号。
leanprover/lean4-cli 的其他 Issue
-
enhancement
难度 5/5 一周以上 新手友好度 25/100
leanprover/lean4-cli#2 ·
查看 leanprover/lean4-cli 的全部 Issue
相似的 Issue
-
难度 2/5 1-3 小时 新手友好度 72/100
-
area:cli bug
难度 2/5 1-3 小时 新手友好度 72/100
维护者通常 1 天内回复
-
难度 2/5 1-3 小时 新手友好度 72/100
维护者通常 1 天内回复
-
难度 2/5 1-3 小时 新手友好度 82/100
维护者通常 1 天内回复
-
type/automation type/performance
难度 2/5 1-3 小时 新手友好度 62/100
维护者通常 2 天内回复