search

leanprover / lean4

Lean 4 programming language and theorem prover
https://lean-lang.org
Apache License 2.0
4.6k stars 407 forks source link

RFC: `lake run` with no default script should fail #2660

Open kim-em opened 1 year ago

kim-em commented 1 year ago

lake run --help says "A bare lake run command will run the default script(s) of the root package".

However if I run lake run in a project with no scripts at all, it returns silently with exit code 0. Should it instead indicate that something is wrong?

tydeu commented 1 year ago

Maybe a warning would be appropriate?

kim-em commented 1 year ago

I think a nonzero exit code is good too. Surely it is a mistake to call lake run when you don't have a default. No point letting people mistakenly think it is doing something.

tydeu commented 1 year ago

@semorrison

Surely it is a mistake to call lake run when you don't have a default.

Not necessarily. Automation across multiple packages may want to run whatever default scripts on in a package for testing or data collection purposes and be happy to skip over packages without default scripts. I think what is preferable is hard to determine without use cases or failure cases.

kim-em commented 1 year ago

I guess so. If a warning is okay I think that would be kind to users.

Kha commented 1 year ago

I agree with Scott fwiw, surely Lake not running something when I tell it to run something is an error condition.

Automation across multiple packages may want to run whatever default scripts on in a package for testing or data collection purposes and be happy to skip over packages without default scripts

This is what we have || true for.