How to quickly run a lean file?

Stream: general

[Jiaming Shan]

On minif2f dataset I generated a lot of proof and want to check validity of these proof. Each proof is a single lean file, so I only want to run one file. Howevery, I can't find good way to do this. Now I use lake exe repl to do this. Some time it works but sometimes don't know why, lake exe repl cannot run any command and just stuck at the first input command(input is command\n\n). Also, I find it strange to use repl to do this simple thing, though a benefit to use repl is that I can let all proof to share the import environment to cut the time. Another method I found (lake run) is just too time consuming on my labtop (maybe my config have problem?). I want to run these lean files as fast(<0.1s or <1s) as possible. What should I do?

[Auguste Poiroux]

Using the REPL to just run Lean files might indeed be a bit of an overkill. But as you said, the main benefit of the REPL is that you can reuse environments, thus speeding up proof checks by quite a lot in comparison to running complete files. In general, I found it is an order in magnitude faster on traditional benchmarks (miniF2f and ProofNet). In the kimina report, they also say they get a 10x speedup. Yesterday, I posted a message in #Machine Learning for Theorem Proving on how to do this with LeanInteract (see this topic), but you can reimplement this directly using the REPL :)

[Jiaming Shan]

What blocks me now is that strangely REPL don't work these days (it works before). Sometimes it just don't respond. Is there any potential thing I can do, like caching?

[Auguste Poiroux]

If you delete your .lake folder and rerun lake build it might fix some issues. But I am not sure how you are using the REPL. If you import Mathlib in your commands, you should make sure that it is added to the lakefile, otherwise it will not work. Or you can use LeanInteract, which does all this for you under the hood. To have Mathlib, you can configure the REPL by running something like this config = LeanREPLConfig(lean_version="v4.18.0", project=TempRequireProject("mathlib")).

[Eric Wieser]

But as you said, the main benefit of the REPL is that you can reuse environments, thus speeding up proof checks by quite a lot in comparison to running complete files

Does the repl produce oleans when used in this way?

[Eric Wieser]

Probably any check against miniF2F should:

• Run leanchecker against the found proof oleans
• Do an axiom check (maybe REPL already does this)

[Auguste Poiroux]

The pickle feature of the repl produces olean files, but I am not sure these will be compatible with leanchecker.

[Jiaming Shan]

I tried LeanInteract and it works! Thanks a lot!

[Jiaming Shan]

But for tactic mode (or say with in a 'by' block), can't I just run a code block (just as the cmd mode)? I don't want to split my proof to tactics line by line and run in tactic mode. It seems that I can not save the state within a by block except that I use sorry and enter tactic mode, but if I do that I cannot run code block directly.The reason I want to do that is: I want to run a lot of proof with only 1 line is different, so I want to save the proof state above that line (it'swithin a 'by' block!) and only run the code behind that line, so maximized redundant run time can be saved.

[Mario Carneiro]

if you are changing lines within a by block, then you are in tactic mode

[Mario Carneiro]

you can't run commands in tactic mode because they would terminate the tactic block you are in

[Mario Carneiro]

Eric Wieser said:

But as you said, the main benefit of the REPL is that you can reuse environments, thus speeding up proof checks by quite a lot in comparison to running complete files

Does the repl produce oleans when used in this way?

I don't think the REPL ever produces oleans

[Mario Carneiro]

(the oleans produced by pickle are not real oleans, they can only be read by unpickle)

[Auguste Poiroux]

Jiaming Shan said:

But for tactic mode (or say with in a 'by' block), can't I just run a code block (just as the cmd mode)? I don't want to split my proof to tactics line by line and run in tactic mode. It seems that I can not save the state within a by block except that I use sorry and enter tactic mode, but if I do that I cannot run code block directly.The reason I want to do that is: I want to run a lot of proof with only 1 line is different, so I want to save the proof state above that line (it'swithin a 'by' block!) and only run the code behind that line, so maximized redundant run time can be saved.

There are two ways to deal with this:

• In tactic mode, you add parentheses around your proof: (\n<your-proof>). The breakline is important. However, I am not sure if this works in all cases. If someone can confirm this that would be amazing :pray:
• The other option is to replace the sorry by the proof before sending the theorem in command mode. And you do that for each proof.

[Auguste Poiroux]

Oh, I misread your comment. Forget the second option I mentioned.
So, you can run the first part of your proof in tactic mode by sending (\n<proof-part-1>) as a tactic, and then you can send (\n<proof-part-2>) as the next tactic. You then check the proof_status attribute of the response. If it says Completed, the proof type-checks. Let me know how this goes.

[Auguste Poiroux]

Actually the second option kind of work as well if you end the first part of the proof with sorry. Then, you still have to continue with tactic mode though

[Jiaming Shan]

Sorry but the problem of REPL go back again even if I use LeanInteract. That's because previously I actually implemented something that is exactly the same as LeanInteract and that doesn't work because REPL doesn't work (or say unstable, will stuck at command import Mathlib, sometime it can run very fast and sometime it will stuck forever). So 9 hours ago it works and now it stuck. @Auguste Poiroux

[Jiaming Shan]

And after I ./clear-lean-cache it works again, and then after some run or passed some time it fails again

[Auguste Poiroux]

Interesting, if possible, would you mind sharing a minimal example causing this?

[Jiaming Shan]

from lean_interact import LeanREPLConfig, LeanServer, Command, TempRequireProject

config = LeanREPLConfig(verbose=True, project=TempRequireProject("mathlib")) # download and build Lean REPL
server = LeanServer(config) # start Lean REPL

response = server.run(Command(cmd="import Mathlib")) #stucks here
print(response)

# Execute with options to get tactics information
response = server.run(Command(cmd="theorem ex (n : Nat) : n = 5 → n = 5 := by simp", all_tactics=True)) #works here
print(response)

# Continue in the same environment
# response = server.run(Command(cmd="#check ex", env=response.env))  #works here
# print(response)

[Jiaming Shan]

Or this is more fundemental:

lake exe repl
{"cmd":"import Mathlib"}

And it doesn't respond. I tried this on two different machines but they both had't respond on this command (while responding {"cmd":"#check 1+1"}).
Though I haven't find any issue talking about this in lean repl github.

[Auguste Poiroux]

I am a bit surprised as well. The only case I know where the repl freezes like this is when there is not enough memory left. Are you trying to limit the memory of the process? Or are you running on a system with limited memory / high memory usage besides the repl?

[Jiaming Shan]

I think it doesn't? For the remote machine, I run this command as soon as I start the machine, so it will have a lot of memory to use.

[Auguste Poiroux]

This is curious, and I unfortunately didn't manage to reproduce this behavior. Can you try these different things and report what they do:

• Running {"cmd":"import Mathlib"}. If it freezes, stop the process and retry. If you do this multiple times, does it always hang?
• Running {"cmd":"import Lean"} or other imports
• Running {"cmd":"import Mathlib\n#check 1+1"} or other variants with more than just imports
• Any other idea you come up with to help narrow down the issue
  Try to do that while running htop in another terminal to check memory and CPU usage.

[Auguste Poiroux]

Another thing I am thinking of: it is possible that, for some reasons, Lean tries to recompile Mathlib from scratch when you send the command {"cmd":"import Mathlib"}, hence the freeze. I don't know why this would happen though.
Let me know what the experiments above return, we will probably have more information about this.

[Jiaming Shan]

For remote machine with enough memory and CPU, only import Mathlib doesn't work, import Lean and non-import calculation works. But after some time I tried import Mathlib and it worked again. It's so unstable that multiple tries at different time gives different results.

[Jiaming Shan]

And for my personal computer (which is slower),
{"cmd":"#check 1+1"} works,
and {"cmd":"import Mathlib"} sometimes works but sometimes not (when it works, it takes more than 1 min to get the result)

[Auguste Poiroux]

This is interesting that you get the same issue on several computers. Which version of the repl are you using? I imagine you get the same issues with LeanInteract. Can you check again the experiments above with LeanInteract?
Which version of elan and lake are you using?

[Jiaming Shan]

For the remote computer, I tried both LeanInteract and lake exe repl, the result is the same. Also, I add elan default stable before every run.

[Jiaming Shan]

For lake verision, I have tried Lake version 5.0.0-be6c489 (Lean version 4.9.0-rc1) for lake exe repl, and the default version in LeanInteract (as the minimal code snippet shows) for LeanInteract

[Auguste Poiroux]

Oh, that's good to know. What does elan --version return?

[Jiaming Shan]

elan 4.0.0 (bb75b50d2 2025-01-30)

[Auguste Poiroux]

Lean version 4.9.0-rc1

If I understand well, you are using Lean v4.9.0-rc1 for both the raw repl and LeanInteract?

[Auguste Poiroux]

It's possible that elan default stable messes up with the repl (not sure though). What is the rationale behind running this before every run?

[Jiaming Shan]

No, LeanInteract is another lake version. I don't know how to check it.

[Jiaming Shan]

you are right, maybe I don't need elan default stable, though I don't know how to remove the effect of this command after it is run.

[Jiaming Shan]

@Auguste Poiroux Since you remind me it might be the problem of elan, I start a new env with new elan installed, and it works! Let's hope it will not have problems from now on.