Mathlib import performance in neovim

Stream: mathlib4

[Greg Shuflin]

I'm using this neovim plugin: https://github.com/Julian/lean.nvim

I'm noticing that when I have import Mathlib in a file, neovim gets really bogged down. I think it is recompiling Mathlib every time, and I'm not sure why it's doing that since compiling the same project locally with Mathlib already compiled on the system doesn't seem to be this slow. Anything I can try?

[Yury G. Kudryashov]

Can you close all lean files, killall lean (OS-dependent, means killing all lean processes), lake build the project, then open the file again?

[Greg Shuflin]

Yury G. Kudryashov said:

Can you close all lean files, killall lean (OS-dependent, means killing all lean processes), lake build the project, then open the file again?

looks like nvim still wants to do something with the import Mathlib line that takes a long time and results in displaying "Processing file..." in the output pane in the editor

[Greg Shuflin]

also when I recompile I get a bunch of warnings from the mathlib code taht aren't in my code, is that normal?

[Yury G. Kudryashov]

What warnings?

[Yury G. Kudryashov]

Does "long time" mean "tens of seconds", "minutes", or "tens of minutes"?

[Greg Shuflin]

Yury G. Kudryashov said:

Does "long time" mean "tens of seconds", "minutes", or "tens of minutes"?

minutes

[Greg Shuflin]

Yury G. Kudryashov said:

What warnings?

pages of stuff like:

warning: ././.lake/packages/mathlib/././Mathlib/Tactic/NormNum/BigOperators.lean:101:6: `Mathlib.Meta.List.range_succ_eq_map'` is missing a doc-string, please add one.
Declarations whose name ends with a `'` are expected to contain an explanation for the presence of a `'` in their doc-string. This may consist of discussion of the difference relative to the unprimed version, or an explanation as to why no better naming scheme is possible.
note: this linter can be disabled with `set_option linter.docPrime false`
warning: ././.lake/packages/mathlib/././Mathlib/Tactic/NormNum/BigOperators.lean:176:6: `Mathlib.Meta.Multiset.range_zero'` is missing a doc-string, please add one.
Declarations whose name ends with a `'` are expected to contain an explanation for the presence of a `'` in their doc-string. This may consist of discussion of the difference relative to the unprimed version, or an explanation as to why no better naming scheme is possible.
note: this linter can be disabled with `set_option linter.docPrime false`
warning: ././.lake/packages/mathlib/././Mathlib/Tactic/NormNum/BigOperators.lean:179:6: `Mathlib.Meta.Multiset.range_succ'` is missing a doc-string, please add one.
Declarations whose name ends with a `'` are expected to contain an explanation for the presence of a `'` in their doc-string. This may consist of discussion of the difference relative to the unprimed version, or an explanation as to why no better naming scheme is possible.
note: this linter can be disabled with `set_option linter.docPrime false`
warning: ././.lake/packages/mathlib/././Mathlib/Tactic/NormNum/BigOperators.lean:245:6: `Mathlib.Meta.Finset.range_zero'` is missing a doc-string, please add one.
Declarations whose name ends with a `'` are expected to contain an explanation for the presence of a `'` in their doc-string. This may consist of discussion of the difference relative to the unprimed version, or an explanation as to why no better naming scheme is possible.
note: this linter can be disabled with `set_option linter.docPrime false`
warning: ././.lake/packages/mathlib/././Mathlib/Tactic/NormNum/BigOperators.lean:248:6: `Mathlib.Meta.Finset.range_succ'` is missing a doc-string, please add one.
Declarations whose name ends with a `'` are expected to contain an explanation for the presence of a `'` in their doc-string. This may consist of discussion of the difference relative to the unprimed version, or an explanation as to why no better naming scheme is possible.
note: this linter can be disabled with `set_option linter.docPrime false`
⚠ [5585/11444] Replayed Mathlib.Tactic.NormNum.LegendreSymbol
warning: ././.lake/packages/mathlib/././Mathlib/Tactic/NormNum/LegendreSymbol.lean:162:8: `Mathlib.Meta.NormNum.jacobiSymNat.qr₁'` is missing a doc-string, please add one.
Declarations whose name ends with a `'` are expected to contain an explanation for the presence of a `'` in their doc-string. This may consist of discussion of the difference relative to the unprimed version, or an explanation as to why no better naming scheme is possible.
note: this linter can be disabled with `set_option linter.docPrime false`
⚠ [5623/11444] Replayed Mathlib.Topology.Algebra.Module.LinearPMap
warning: ././.lake/packages/mathlib/././Mathlib/Topology/Algebra/Module/LinearPMap.lean:97:8: `LinearPMap.closure_def'` is missing a doc-string, please add one.
Declarations whose name ends with a `'` are expected to contain an explanation for the presence of a `'` in their doc-string. This may consist of discussion of the difference relative to the unprimed version, or an explanation as to why no better naming scheme is possible.
note: this linter can be disabled with `set_option linter.docPrime false`
⚠ [5645/11444] Replayed Mathlib.Topology.Category.Profinite.Nobeling

[Yury G. Kudryashov]

Why do you have 11K files to compile?

[Yury G. Kudryashov]

Is your project that big?

[Greg Shuflin]

no I would guess that I installed mathlib incorrectly, my project is like six files

[Yury G. Kudryashov]

Mathlib is <6K files.

[Greg Shuflin]

mathlib + batteries?

[Greg Shuflin]

I have no idea what that number is supposed to be, or even that it indicated files

[Yury G. Kudryashov]

If I run lake build in Mathlib, then it shows <6K files.

[Greg Shuflin]

I also have batteries in this project

[Yury G. Kudryashov]

What's your lakefile?

[Greg Shuflin]

name = "aoc"
version = "0.1.0"
defaultTargets = ["aoc"]

[[lean_lib]]
name = "Aoc"

[[lean_exe]]
name = "aoc"
root = "Main"

[[require]]
name = "batteries"
scope = "leanprover-community"
rev = "main"

[[require]]
name = "mathlib"
scope = "leanprover-community"

[Yury G. Kudryashov]

Mathlib already depends on batteries, so no need to add batteries as another dependency.

[Greg Shuflin]

I'm gonna try lake clean and rebuilding

[Greg Shuflin]

Yury G. Kudryashov said:

Mathlib already depends on batteries, so no need to add batteries as another dependency.

huh so does explicitly adding it mean it double-compiles?

[Yury G. Kudryashov]

I'm not sure what happens in this case. I hope, it doesn't try to recompile Mathlib against your version of batteries.

[Yury G. Kudryashov]

Do you import Mathlib in a file that has executable code?

[Yury G. Kudryashov]

If yes, then it tries to compile the whole Mathlib.

[Greg Shuflin]

hm, so should I avoid that?

[Yury G. Kudryashov]

And this can explain the huge number (most of the files are built, then compiled).

[Greg Shuflin]

I thought I had to use import Mathlib in the file in order to use it

[Yury G. Kudryashov]

You should import Mathlib.Some.File for Mathlib files that you actually need.

[Yury G. Kudryashov]

The file with the binary should have minimal dependencies.

[Greg Shuflin]

often I'm importing something because I want to #eval it in a file and see what it does

[Greg Shuflin]

and I don't know exactly what path to import

[Yury G. Kudryashov]

Then you can lake exe aoc so that all of Mathlib gets compiled.

[Yury G. Kudryashov]

About warnings: it looks like some of our "nolints" don't work well for downstream projects. @Damiano Testa wrote this linter.

[Yury G. Kudryashov]

UPD: no, I don't think that it should compile (not build) all of Mathlib on import Mathlib, so my previous advice is probably useless.

[Yury G. Kudryashov]

@Julian Berman is the author of the nvim plugin. Julian, what do you think is happening here?

[Greg Shuflin]

ok I just removed the separate batteries specification in the file and ran lake update and am rebuilding. I still see 11450 files so I guess that is batteries + mathlib

[Daniel Weber]

Greg Shuflin said:

often I'm importing something because I want to #eval it in a file and see what it does

You don't need to compile it to #eval it

[Greg Shuflin]

Daniel Weber said:

Greg Shuflin said:

often I'm importing something because I want to #eval it in a file and see what it does

You don't need to compile it to #eval it

I'm just typing #eval <some function from Mathlib> into my nvim window, I'm not telling it to compile anything explicitly

[Greg Shuflin]

but yeah I've definitely noticed nvim getting sluggish when it's compiling in the background

[Yaël Dillies]

Greg Shuflin said:

and I don't know exactly what path to import

You can import Mathlib then use #min_imports

[Greg Shuflin]

Yaël Dillies said:

Greg Shuflin said:

and I don't know exactly what path to import

You can import Mathlib then use #min_imports

what is #min_imports?

[Yaël Dillies]

Try it :wink:

[Greg Shuflin]

where in the documentation can I find it? I am not sure what effect I shoudl expect frrom just typing it randomly into source code

[Yaël Dillies]

import Mathlib

lemma factorial_pos (n : ℕ) : 0 < n.factorial := by exact?

#min_imports

[Greg Shuflin]

Greg Shuflin said:

where in the documentation can I find it? I am not sure what effect I shoudl expect frrom just typing it randomly into source code

unexpected token '#'; expected command

[Yaël Dillies]

Have you tried my above code snippet?

[Yaël Dillies]

There is a button in the top right of the code snippet. Try clicking on it

[Greg Shuflin]

sure that works in the lean playground, and doesn't work in my code.

[Greg Shuflin]

I'm not sure what the rules are for when you can use #min_imports, or what it should be doing

[Greg Shuflin]

is it documented?

[Yaël Dillies]

Yes, like anything in Lean you can Ctrl + click on it to see where it is defined

[Greg Shuflin]

in what program?

[Yaël Dillies]

In vscode it certainly works. I don't know about emacs and neovim but hopefully they have analogous keybindings

[Yaël Dillies]

I will tell you what import you need, since I don't know how to jump to definition in neovim. Try import Mathlib.Tactic.Common

[Kevin Buzzard]

Isn't the problem here nothing to do with neovim or imports but simply that the Lakefile shouldn't be mentioning batteries?

[Julian Berman]

I am flying today and tomorrow so I'm not sure how closely I'll be able to read the thread, but yeah I'm a bit confused about the neovim-specific bit. Has the lakefile been fixed, what does it look like now?

[Julian Berman]

OK I see you said you removed it.

[Julian Berman]

Greg Shuflin said:

Yury G. Kudryashov said:

Can you close all lean files, killall lean (OS-dependent, means killing all lean processes), lake build the project, then open the file again?

looks like nvim still wants to do something with the import Mathlib line that takes a long time and results in displaying "Processing file..." in the output pane in the editor

So is this the issue? When you say "takes a long time" and displays that processing message -- I see you said "minutes" to how long that is -- import Mathlib is "expected" to take on the order of a minute or two to run depending on your machine (in any project at this point). Is that what you're seeing?

[Kevin Buzzard]

You've run lake exe cache get right? Can you reproduce the slowness on the command line?

[Greg Shuflin]

Kevin Buzzard said:

You've run lake exe cache get right? Can you reproduce the slowness on the command line?

so I have typed that command, but I am not sure if it actually ran as intended. I think what I originally did was add the lines to my lakefile.toml that involved importing Mathlib, and then ran lake exe cache get, ran into some error message that said I should run lake update, and then ran that, and that seemed to take a long time. but I forget exactly what things I tried at this point. I should say that I am pretty new to lean and dont' have a great intuitive sense of what commands do what or should do what but might be buggy

[Greg Shuflin]

Kevin Buzzard said:

Isn't the problem here nothing to do with neovim or imports but simply that the Lakefile shouldn't be mentioning batteries?

I originally had both batteries and mathlib as separate [[require]] lines in my lakefile.toml, I didn't realize that only mathlib was necessary until this thread I think

[Greg Shuflin]

anyway, it looks like the behavior I'm seeing now is that if I open up a new file in my lake project in neovim, and type import Mathlib into it, I'm seeing processing file... in the evaluation pane for a few seconds (less than 10), and then the pane is capable of e.g. giving answers to #eval lines

[Julian Berman]

That sounds like everything is working then for now to me

[Julian Berman]

Right?

[Greg Shuflin]

I think so

[Julian Berman]

Great!

[Julian Berman]

Complain if anything seems improvable (in neovim or otherwise)!