Speeding up the lean infoview

Stream: new members

[Jakob Scholbach]

What are ways to speed up the interactive lean parser in VS Code? I often have a situation where the program takes minutes to check if my code works. In the case I just have I have edited a file that was already part of mathlib (category/arrows.lean). That file does compile and the lean infoview is reasonably quick to update. However, another file that builds upon arrows.lean is extremely slowly / not at all reacting in the infoview. Thanks!

[Yakov Pechersky]

Have you done lean --make your/path/to/target.lean? That will compile oleans for that file and all dependencies

[Jakob Scholbach]

No, I have not. Do I need to do that regularly?

[Jakob Scholbach]

By your/path/to/target.lean/ you mean the git repo folder containing the mathlib copy? (I am working in a copy of mathlib).

[Thomas Browning]

Oleans can help. If you're working on a branch of mathlib, then you can make your change to an existing file, push, wait a couple hours, and then do leanproject get-cache

[Johan Commelin]

@Jakob Scholbach Yeah, if there are 10 files between arrows.lean and the file you work on, Lean has to do a lot of work in between.

[Johan Commelin]

So it makes sense to recompile before resuming work on your file

[Johan Commelin]

If you ever edit logic.basic you will have the joy of waiting for 2 hours before mathlib is recompiled :grinning:

[Yury G. Kudryashov]

Unless you use lean --old

[Yury G. Kudryashov]

With --old Lean will assume that your changes to logic/basic don't affect the files you did not edit.

[Yury G. Kudryashov]

Of course, this doesn't work if you change the type of a def/lemma.

[Yury G. Kudryashov]

(as opposed to adding new defs/lemmas)

[Jakob Scholbach]

Ah, that is good. In my case I just added a def to arrow.lean, which wouldn't affect anything else. So, I run lean --old in the terminal once and then this will do it?

[Yury G. Kudryashov]

No, you need to pass --old argument to the lean server process.

[Yury G. Kudryashov]

This should be somewhere in the lean extension settings (I'm using Emacs, so can't help with the details).

[Bryan Gin-ge Chen]

In VS Code, you'd add --old to the box under "Extra command-line options for the Lean server" in the extension settings.

[Scott Morrison]

I'd advise not getting too complicated with lean --old. If you're plugged into power, just leave lean --make current_work.lean buzzing along in a terminal...

[Yury G. Kudryashov]

I always pass --old to lean server and run lean --make current_work.lean from time to time.

[Scott Morrison]

Maybe I should try this more!