CLI fails silently on v4.30.0+ when using module system
Chưa có ai nhận issue này.
Đánh giá
- Độ khó
- 3/5
- Thời gian dự kiến
- 1-2 ngày
- Mức phù hợp với người mới
- 52/100
Hướng nghiên cứu
Bắt đầu với repository MWE gồm hai commit được liên kết và so sánh hành vi của nó trên v4.29.1 và v4.30.0, tập trung vào Main.lean và khai báo module của nó. Theo dõi cách lean4-cli phát hiện và gọi entry point meta main công khai. Hoàn thành khi một Main.lean dựa trên module được thực thi bình thường thay vì âm thầm trở thành no-op, trong khi trường hợp file thuần túy hiện có vẫn hoạt động.
Do mô hình lập chỉ mục viết ra từ nội dung của issue.
Mô tả
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.
- Ngôn ngữ chính
- Lean
- Star
- 123
- Fork
- 30
- Merge trung bình
- 4 phút
- Pull request đã merge (30 ngày)
- 5
Chuẩn bị môi trường
Dự án này không cung cấp dev container, Dockerfile hay hướng dẫn đóng góp, nên bạn cần tự thiết lập môi trường: hãy bắt đầu từ README và xem hướng dẫn đóng góp lần đầu của chúng tôi để biết các bước chung.
Bắt đầu từ đâu
- Đọc hết issue, rồi đọc hướng dẫn đóng góp của dự án.
- Bình luận trên issue rằng bạn sẽ nhận — tránh hai người làm cùng một việc.
- Fork repository và làm thay đổi trên một nhánh.
- Mở pull request có tham chiếu số hiệu của issue.
Issue khác của leanprover/lean4-cli
-
enhancement
Độ khó 5/5 Hơn một tuần Mức phù hợp với người mới 25/100
leanprover/lean4-cli#2 ·
Tất cả issue của leanprover/lean4-cli
Issue tương tự
-
Độ khó 2/5 1-3 giờ Mức phù hợp với người mới 74/100
datahub-project/datahub#20399 · 1 bình luận ·
Maintainer thường phản hồi trong vòng 1 ngày
-
enhancement
Độ khó 2/5 1-3 giờ Mức phù hợp với người mới 72/100
charmbracelet/glow#1058 ·
Maintainer thường phản hồi trong vòng 1 ngày
-
comp/cli comp/cron P3 type/feature
Độ khó 2/5 1-3 giờ Mức phù hợp với người mới 70/100
NousResearch/hermes-agent#137599 ·
Maintainer thường phản hồi trong vòng 1 ngày
-
api bug macos maintainer-needed p2 triaged
Độ khó 2/5 1-3 giờ Mức phù hợp với người mới 66/100
Maintainer thường phản hồi trong vòng 1 ngày
-
area::tern-term difficulty::easy good first issue kind::bug triage::ready
Độ khó 1/5 1-3 giờ Mức phù hợp với người mới 94/100