Running from the command line

Stream: new members

[Moshe Kamensky]

Hi There, it's a bit silly, but I can't find instructions for using lean from the command line. All documentation I see requires me to open a project in vscode (which I don't use). Is it possible to "run" a proof from the command line (I'm not sure what I'm expecting to see actually). I tried

lean Foo.lean

but I get errors about missing Mathlib.

Thanks!

[Ruben Van de Velde]

You can use lake build from the command line

[Ruben Van de Velde]

I highly recommend using an IDE, though

[Moshe Kamensky]

Thanks. I tried running it, and it still working... I have an extremely simple proof there (just playing around to get the idea), should it be taking so long?

[Ruben Van de Velde]

What kind of output is it showing?

[Moshe Kamensky]

I left it for the moment, so I don't have the precise message, but it was building over 1400 items

[Ruben Van de Velde]

Did you run lake exe cache get?

[Moshe Kamensky]

Yes

[Kevin Buzzard]

It should not be taking so long, and you shouldn't need to build anything. lake exe cache get should download all precompiled binaries for you, if you've got lean installed and have a correctly formatted lean project with mathlib as a dependency.

[Moshe Kamensky]

Thanks. I now tried it again, and it ran faster, possibly I made a mistake before. At any rate, I don't see any result of this run, the last thing it says is [1946/1947] Building Lean4Try. Does it simply exit with status 0 when the proof is correct?

[Kevin Buzzard]

That looks good, because that file looks like yours rather than anything in mathlib. Yes it will end with status 0 if the proof compiles.

[Moshe Kamensky]

Thanks!

[Moshe Kamensky]

So, when I have a proof I’d like to verify, I should always make it a part of a project?

[Kevin Buzzard]

I think you are very very limited in what you can do outside of the project set-up. For example you have no control over which version of lean or mathlib you're using because this data is not in your lean file, so with 100% probability your code will break at some point as it rots (mathlib updates about 20 times a day and makes no promises regarding backwards compatibility). Also I don't think you can use any imports outside of the project framework.

[Moshe Kamensky]

Thanks again!