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.
Up to v4.29.1, it was possible to use the module system for the entry point of an executabl (
Main.leanin the template lake projects). In v4.30.0 this will causelean4-clito 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.leancontainsIf
moduleis removed fromMain.leanturning it into a plain Lean file, it works again.