Does lean-mode hang often

Stream: new members

[Julin S]

Is it just me or is the lean-mode of emacs often not-so-responsive?

[Julin S]

lean --server seems to take up quite a lot of RAM as well..

[Johan Commelin]

Do you have a precompiled mathlib?

[Kevin Buzzard]

This is not a question about finite fields so should go in its own thread. Have you compared with VS Code? Lean is sometimes not-so-responsive -- it's just thinking. My question is: are you sure this is an emacs issue rather than a lean issue? But this discussion should be taking place in another thread anyway.

[Julin S]

I had been using lean from emacs via the lean-mode.

Quite often response is quite slow and sometimes hangs altogether.

Usually, a check mark (✓) shows up when lean isn't busy thinking. But even the check mark is visisble, sometimes the goal won't change.

I think I'm using a precompiled version of mathlib. Because I can see a bunch of .olean files. That means precompiled version, right?

(Came from here).

[Julin S]

Thanks. Made a new thread here: https://leanprover.zulipchat.com/#narrow/stream/113489-new-members/topic/Does.20lean-mode.20hang.20often

[Julin S]

And.. uh.. I don't fancy using vscode.. So not sure if this is a problem there as well.

The computer I'm on has got ample amount of RAM left over even when running lean.

Although the lean process seem to be taking lot of RAM at least sometimes.

[Notification Bot]

5 messages were moved here from #new members > Finite fields in lean by Eric Wieser.

[Kevin Buzzard]

Some proofs can be slow. Maybe you just wrote a slow proof. Can you give a #mwe of the problem? This might be nothing to do with emacs and might just be Lean being slow. There is set_option profiler true -- if this is reporting large times then it's nothing to do with emacs.

[Tomas Skrivan]

I personally have problems with lean-mode for the last month or two. Very often I have to reload file dependencies(without changing imported files!) to get correct type checking and syntax highlighting, emacs sometimes refuses to type check newly written stuff. Restarting the whole lean-mode helps sometimes too. Occasionally, I have to restart emacs altogether as the performance gets really bad.

I was unable to figure out what is the problem :( but I'm definitely not running out of memory.