Run lean from command line inside project

Stream: general

[Jason Rute]

I'm having a lot of trouble searching for this. Lets say I have a project (maybe just with Mathlib) and I want to run lean myfile.lean from the command line (say I'm trying to benchmark a new tactic). I know I can sort of do this with lake build myfile.lean, but is there a way (or any reason to) do it with lean instead? Naively lean myfile.lean won't work since it can't recognize imports like import Mathlib.

[Jason Rute]

I guess while I'm asking, I can also ask about the lean --server. How can that be run from within a project?

[Adam Topaz]

Does lake env lean foobar.lean work?

[Ruben Van de Velde]

Lake is exactly the tool to handle lean with imports. What's the goal in avoiding it?

[Jason Rute]

@Ruben Van de Velde I don't need to build a file, just check it. (But maybe that isn't a big difference in execution time and doesn't matter.)

[Jason Rute]

@Adam Topaz Yes, that is it! (I was mistakenly trying exe instead of env.) I assume this also works for lake env lean --server.

[Adam Topaz]

it should yes

[Adam Topaz]

but there may be another way to run the server with lake? I'm not sure

[Jason Rute]

@Ruben Van de Velde To be clear, I was avoiding lake build not lake entirely. Another thing for example is that lake env lean gives more computer-readable error messages than lake build.

[Mac Malone]

laker serve is the Lake replacement for lean --server.

[Mac Malone]

You can also use lake lean myfile.lean to have Lake build the imports of the file (if necessary) before run it via lean.

[Utensil Song]

lean4_jupyter uses lake env repl to ensure it works well with projects.

In general one would want to use lake to take care of things, or one will be writing code that duplicates lake, but subject to the risks of random Lean internal changes.

If lake build is not run beforehand, lake env lean might still suffer at lease slow startup, which might affect your benchmark, unless you intend to also benchmark deps handling time and the build time of the target file. lake exe something will also handle deps and build.

[Utensil Song]

I was also surprised by the fact that lake clean will download all deps again, if I run rm -rf .lake first.

[Utensil Song]

And that lake is silent during the process, until it finishes fetching all git repos. An impatient user will thought that it's trying to clean up a huge amount of files which might be dangerous, and abort the process, until trying it again in a container then is rest assured by that it's just fetching deps.

[Utensil Song]

Mac Malone said:

You can also use lake lean myfile.lean to have Lake build the imports of the file (if necessary) before run it via lean.

Just noticed this in the change log, this is really nice!

image.png