Noob question about Lean 4 without VS Code

Stream: new members

[Andy Jiang]

Hi,

I have a basic question. I just want to be able to check some simple proofs in the command line in the easiest way possible (preferably without the use of editors). What I would like is just to run lean --run file.lean and have it import Mathlib without errors. What is the easiest way to do that? I managed to get it to run once (lol!) using lake build. But I can't even figure out how to run the code again without change lol. Please only command line tools and no interactive tools please, I want to automate eventually the process in python later and I want it to be as simple as possible.

thanks in advance.

[Richard Copley]

You don't need to (and cannot) run a proof: there is no executable code associated with it. The verification of the proof is purely type checking, and happens during the build stage done by lake build. The tools are not set up for building the same thing more than once. You'll get the same messages on standard output each time anyway, so saving the messages for future reference (lake build >> log, less log) should be enough. But you can force a rebuild with the usual tricks: delete the output files (the ".oleans"), or change the last-modified time of the input files.

[Andy Jiang]

OK this makes sense! It was just confusing to me bc I put some print "hello" in the main and I couldn't get that to run twice. But it makes sense that I can just check if the compile succeeds to see the proof worked. OK thanks

[Richard Copley]

When lake does rebuild a file, you can see the command(s) it runs with lake build --verbose. You can run those commands directly (no tricks needed).