Zulip Chat Archive

Stream: new members

Topic: Does lean-mode hang often

Julin S (Mar 02 2023 at 14:22):

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

Julin S (Mar 02 2023 at 14:23):

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

Johan Commelin (Mar 02 2023 at 16:21):

Do you have a precompiled mathlib?

Kevin Buzzard (Mar 02 2023 at 16:21):

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 (Mar 02 2023 at 16:49):

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 (Mar 02 2023 at 16:49):

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

Julin S (Mar 02 2023 at 16:49):

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 (Mar 02 2023 at 16:54):

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

Kevin Buzzard (Mar 02 2023 at 18:46):

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 (Mar 05 2023 at 16:17):

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.

Last updated: Dec 20 2023 at 11:08 UTC