mathlib rebuilding all the time

Stream: new members

[Paul Nelson]

Hello. I'm trying to get lean working on macos, but am having trouble with Mathlib wanting to rebuild all the time in new projects (although not in the MIL project, which works fine). I've followed the instructions at https://leanprover-community.github.io/install/macos.html, https://leanprover-community.github.io/install/macos_details.html and https://stackoverflow.com/questions/77280192/mathlib-keeps-rebuilding-even-after-i-lake-exe-cache-get.

The last link suggests that the issue might be that my lean version is 4.4.0, while .lake/packages/mathlib/lean-toolchain is "leanprover/lean4:v4.5.0-rc1" for new projects (and "leanprover/lean4:v4.4.0-rc1" for MIL). I can't seem to get elan to switch to 4.5.0. Here's some terminal output in case it's of any use: lean.txt. Any suggestions welcome!

[Alex Kontorovich]

Once someone helps you with this and you get Lean up and running, let's formalize some subconvexity bounds! :)

[Alex J. Best]

The lean version elan uses depends on what is in the file lean-toolchain elan should handle things automatically to use whatever that version is.
Do I understand that you have created a project depending on mathlib? In that case you probably want to copy the lean-toolchain file from .lake/packages/mathlib/lean-toolchain to the root directory of your project, so that they use the same version

[Alex J. Best]

If you've done that and it still isn't working can you paste the ouput of elan show here

[Alex J. Best]

You should probably also uninstall the brew version of lean, that wont be much use

[Paul Nelson]

Thanks. I believe that I did create a project depending upon mathlib, following the instructions at the links in my message:

lake +leanprover/lean4:nightly-2023-02-04 new Foo math
cd Foo
lake update
lake exe cache get
mkdir Foo

the lean-toolchain file in both the root of the project and .lake/packages/mathlib say the same thing, namely leanprover/lean4:v4.5.0-rc1

brew does not seem to think that the brew version of lean is installed. I tried "brew uninstall lean". It appears in that homebrew folder, but I feel like elan is putting that symlink there. There are some details on this in the file I attached to my message

here's my current output from elan show (also in the attachment):

% elan show
elan show
installed toolchains

---

stable (default)
leanprover-community/lean:3.42.1
leanprover-community/lean:3.49.1
leanprover/lean4:nightly-2023-02-04
leanprover/lean4:stable
leanprover/lean4:v4.3.0-rc1
leanprover/lean4:v4.4.0-rc1
leanprover/lean4:v4.5.0-rc1
4.5.0-rc1

active toolchain

---

leanprover/lean4:v4.4.0-rc1 (overridden by '/Users/au710211/lean/mathematics_in_lean/lean-toolchain')
Lean (version 4.4.0-rc1, commit b0fe9d6cdca8, Release)

[Paul Nelson]

sorry, that "elan show" wasn't the most relevant one, since I ran it from a different directory. Running from "Foo" gives:

au710211@d51735 Foo % elan show
elan show
installed toolchains

---

stable (default)
leanprover-community/lean:3.42.1
leanprover-community/lean:3.49.1
leanprover/lean4:nightly-2023-02-04
leanprover/lean4:stable
leanprover/lean4:v4.3.0-rc1
leanprover/lean4:v4.4.0-rc1
leanprover/lean4:v4.5.0-rc1
4.5.0-rc1

active toolchain

---

leanprover/lean4:v4.5.0-rc1 (overridden by '/Users/au710211/lean/Foo/lean-toolchain')
Lean (version 4.5.0-rc1, commit b614ff1d12bc, Release)

[Paul Nelson]

if I run it from a non-project directory, then it shows:

active toolchain

---

stable (default)
Lean (version 4.4.0, commit ca7d6dadb9e1, Release)

[Alex J. Best]

Ok that second one seems fine (in Foo), if you run lake exe cache get then lake build in that directory what is the full output

[Paul Nelson]

au710211@d51735 Foo % lake exe cache get
lake exe cache get
No files to download
Decompressing 4066 file(s)
unpacked in 36051 ms
au710211@d51735 Foo % lake build
lake build
[1/2] Building Foo
au710211@d51735 Foo %

[Ruben Van de Velde]

(don't let it run for more than a few minutes)

[Paul Nelson]

it's already done. that was it

[Paul Nelson]

I mean, I ran this command already when I set the project up, don't have the full output from that one. could try creating a fresh project and sharing what it says then

[Ruben Van de Velde]

Sounds like it worked

[Ruben Van de Velde]

This is the output you should be getting

[Paul Nelson]

OK, but when I open it (in VSCode or Emacs, I've tried both), it's very often saying something like "imports out of date, need to rebuild mathlib", which then takes a long time

[Paul Nelson]

opening it in VSCode just now, it says "Imports of 'test.lean' are out of date and must be rebuilt."

[Paul Nelson]

here are the contents of test.lean, for whatever that's worth:

import Mathlib
import Mathlib.Algebra.Module.Basic
import Mathlib.Algebra.Algebra.Subalgebra.Basic

example (R V : Type) [CommRing R] [AddCommGroup V] [Module R V] (s : Set (Module.End R V)) (v : V) : (Subalgebra.centralizer R s) →ₗ[R] V := by
  have f1 : (Module.End R V) →ₗ[R] V := ((1 : (Module.End R V) →ₗ[R] (Module.End R V)).smulRight v)
  have f2 : (Subalgebra.centralizer R s) →ₗ[R] (Module.End R V) := (Subalgebra.val (Subalgebra.centralizer R s)).toLinearMap
  exact f1.comp f2

[Ruben Van de Velde]

I'd wonder if there are stray lean or VS code processes getting in the way

[Paul Nelson]

I've been wondering that too, been trying to keep a fresh one isolated for a bit, and no issues so far

[Paul Nelson]

I was using emacs to work through the MIL exercises

[Paul Nelson]

which are with 4.4.0 mathlib

[Paul Nelson]

and I have no sense of how it spins up lean processes to work with lsp-mode there

[Paul Nelson]

and how they'd interfere with lean processes that should be for different projects

[Paul Nelson]

have you seen situations where stray processes play some role?

[Paul Nelson]

after editing for awhile, I got the message "lean version changed" and was prompted to restart lean. Then I saw the following in the "output" console:

lean +leanprover/lean4:stable --version
Lean (version 4.4.0, commit ca7d6dadb9e1, Release)

/Users/au710211/lean/Goo> lean +leanprover/lean4:v4.5.0-rc1 --version
Lean (version 4.5.0-rc1, commit b614ff1d12bc, Release)

/Users/au710211/lean/Goo> lean +leanprover/lean4:v4.5.0-rc1 --version
Lean (version 4.5.0-rc1, commit b614ff1d12bc, Release)

/Users/au710211/lean/Goo> lean +leanprover/lean4:v4.5.0-rc1 --version
Lean (version 4.5.0-rc1, commit b614ff1d12bc, Release)

[Error - 18:48:46] Stopping server timed out
Watchdog error: Got shutdown request, expected an exit notification

now this project (like all the others I've tried before it) is in the broken state where it constantly tries to rebuild mathlib. it remains in this state after quitting all editors and killing all lake/lean processes

[Paul Nelson]

I've checked that no files in my project folder (other than the source files I was editing) have actually changed. so I guess what I'd like to understand is, where might this "broken state" be stored, and how might I go about reverting it?

[Paul Nelson]

maybe a concrete question in that direction would be, when lean says it's rebuilding mathlib, where is it actually storing the result of that build? doesn't seem to be anywhere in my project folder

[Mauricio Collares]

Paul Nelson said:

maybe a concrete question in that direction would be, when lean says it's rebuilding mathlib, where is it actually storing the result of that build? doesn't seem to be anywhere in my project folder

.lake/build inside the project directory, or .lake/packages/PACKAGE/.lake/build for dependencies

[Paul Nelson]

ah, there it is, thanks (Goo/.lake/packages/mathlib/.lake/build/lib)

[Mauricio Collares]

You can try nuking the .lake directory and then running lake exe cache get! to download everything from scratch

[Paul Nelson]

thanks, will try

[Paul Nelson]

the folder where the offensive compilation seems to happen is Goo/.lake/packages/mathlib/.lake/build/lib. Do I infer correctly that you're suggesting I nuke Goo/.lake/packages/mathlib/.lake, or the parent .lake?

[Mauricio Collares]

lake exe cache get! will recreate everything from scratch, so deleting the parent .lake seems more likely to fix your problem

[Paul Nelson]

ok, thanks! seems like that should at least let me "medicate" the issue for now

[Paul Nelson]

ok, thanks! seems like that should at least let me "medicate" the issue for now

[Paul Nelson]

I thought I'd ask if the following is normal behavior:

1. In my project folder, I do rm -rf .lake followed by lake exe cache get!, as suggested above.
2. I open .lake/packages/mathlib in vscode (or some .lean file from it in emacs -- get the same result either way)
3. vscode immediately tells me that imports are out of date and need to be rebuilt. (emacs just starts building those imports.) this takes a while.

[Mauricio Collares]

This is not normal. Do you have any unsaved changes to VS Code tabs corresponding to mathlib files?

[Paul Nelson]

I have everything closed (emacs and vscode), then I open just a single file from ./lake/packages/mathlib (say in vscode, using Finder to select the file), it offers to open the project containing the file, and then the above happens. there are no changes to any of the mathlib files, and this happens immediately after doing rm -rf etc as above

[Sebastian Ullrich]

Step 2 is wrong, you need to open the root project in VS Code. You can then still open individual files from that directory (or jump to them via go-to-definition on imports)

[Paul Nelson]

step 2 I'm just doing to try to diagnose the issue that creeps in when I open the root project and work on stuff manually that way.

[Paul Nelson]

it seems to happen randomly after I've been editing for a while and using "goto definition" to visit mathlib files, but hasn't been fully reproducible

[Paul Nelson]

but the above steps do seem to be reproducible

[Paul Nelson]

(I assume you mean "wrong" as in "that's not what you want to do when you're actually working on your project in practice")

[Paul Nelson]

or do you mean that the above behavior is to be expected when I do those steps (even if they're not the appropriate steps in practice)?

[Sebastian Ullrich]

I don't know but the tooling certainly doesn't expect you to do it like that. Can you reproduce the issue when opening the root project in VS Code and then jumping to Mathlib.lean?

[Paul Nelson]

doing things the normal way (opening a project and jumping around), the issue just seems to creep in at random, forcing me to run step (1) every now and then. I haven't yet found a completely reproducible recipe or pattern, but will pay attention

[Paul Nelson]

I'll also mention that I'm mainly using emacs/lean4-mode, don't know if that might be an issue

[Sebastian Ullrich]

It may or may not be the case that lean4-mode makes the same mistake as your step 2 above. Unlike vscode-lean4, it can automatically select project roots.

[Paul Nelson]

I noticed just now that lean4-mode spawns a separate lsp process for mathlib

[Paul Nelson]

seems suspicious

[Sebastian Ullrich]

Indeed, same issue

[Paul Nelson]

do you know if many people here use lean4-mode? or is it basically unofficially unsupported as far as mathlib is concerned

[Sebastian Ullrich]

I assume it isn't many people. Development of lean4-mode has effectively halted as well.

[Paul Nelson]

I see, OK

[Paul Nelson]

do you happen to know if the correct approach (e.g., what happens in vscode when everything is working correctly) is just to have one lsp process for the whole thing, and to view mathlib as belonging to the parent project?

[Alex J. Best]

Is this https://github.com/leanprover/lean4-mode/pull/48 ? Except that that patch would no longer work as we now have .lake instead of lake-packages (and that directory name is configurable by the user anyway)

[David Renshaw]

I use emacs with lean4-mode for mathlib and some things that depend on mathlib. I find some things annoying, like it always asks "do you want to watch all files in <project root>" even if the right answer is seems to always be "no", and I have developed a habit of eagerly restarting emacs and/or doing git clean to clear out state e.g. when I switch branches. But for the most part it works well enough, and it certainly does not need to rebuild mathlib all the time.

[David Renshaw]

Actually, come to think of it, I do remember an issue on MacOS where if I'm in a project that depends on mathlib and I jump to definition of something inside of mathlib, somehow just visiting that file makes the lean server think that it needs to rebuild a bunch of stuff. I think this started happening some time between 0 and 9 months ago.

[Paul Nelson]

yeah, I think the issue alex pointed to is exactly the one

[Paul Nelson]

I was about to try to work out something similar

[Paul Nelson]

david, regarding "do you want to watch all files", I'm using (setq lsp-enable-file-watchers nil)

[Paul Nelson]

OK, so I guess the question is: what would nowadays be appropriate way to determine that a repo (like the mathlib subfolder of a project) is intended to be a subproject rather than a project?

[Paul Nelson]

also, david or anyone, I've been accumulating some lean4-mode tweaks at https://github.com/ultronozm/czm-lean4.el

[David Renshaw]

8. Line wrapping for the goal window, with visual indicators where it wraps.

:100:

[Paul Nelson]

Alex J. Best said:

Is this https://github.com/leanprover/lean4-mode/pull/48 ? Except that that patch would no longer work as we now have .lake instead of lake-packages (and that directory name is configurable by the user anyway)

do you know what sorts of things people use in practice other than ".lake"?

[Mauricio Collares]

lake-packages was renamed to .lake/packages as the default in v4.4.0

[Alex J. Best]

Paul Nelson said:

Alex J. Best said:

Is this https://github.com/leanprover/lean4-mode/pull/48 ? Except that that patch would no longer work as we now have .lake instead of lake-packages (and that directory name is configurable by the user anyway)

do you know what sorts of things people use in practice other than ".lake"?

I think nobody changes the default in practice :wink:, I'm just making the point that a more robust thing to do (more with respect to lean/lake itself changing than users) is to ask lake for this directory somehow.

[Paul Nelson]

OK, makes sense. I made ".lake" a customization option, see https://github.com/ultronozm/lean4-mode. seems to be working well for me now, thanks for your help!

[Richard Copley]

Paul Nelson said:

also, david or anyone, I've been accumulating some lean4-mode tweaks at https://github.com/ultronozm/czm-lean4.el

There's also my eglot fork. (Eglot is an LSP library with some advantages over lsp-mode and some missing features. It is in core Emacs.)

[Paul Nelson]

speak of the devil, I've been playing with that just the last few mins

[Paul Nelson]

looks great

[Paul Nelson]

I'm on your master branch

[Paul Nelson]

I've noticed thus far only that complete-at-point seems to be less useful than in the vanilla lean4, is that a known issue?

[Paul Nelson]

if I do "LinearMap.d" and complete-at-point, I don't get anything in your fork, but do in the basic one (actually it's working now, I'll keep playing)

[Paul Nelson]

maybe just an eglot deficiency

[Paul Nelson]

but if so, maybe it could be complemented by something more rudimentary

[Richard Copley]

Sebastian Ullrich said:

I assume it isn't many people.

A self-fulfilling prophecy. It would attract more users if it worked better. And yet there are several forks, a number of unreviewed issues and PRs, and people discuss it here now and then.

Development of lean4-mode has effectively halted as well.

Do you still want to be the maintainer? If not, and if there is anyone around who does use it and care about it, it could at least tick over and be kept working.

[Richard Copley]

Paul Nelson said:

I've noticed thus far only that complete-at-point seems to be less useful than in the vanilla lean4, is that a known issue?

Thanks! I should probably add something like this to README.md:

(with-eval-after-load 'lean4-mode
  (define-key lean4-mode-map [?\t] #'company-indent-or-complete-common)
  (add-hook 'lean4-mode-hook #'company-mode))

[Paul Nelson]

ah, OK, great, thanks

[Paul Nelson]

the only other thing I've noticed is that M-. seems to successfully jump less often (I seem to recall in the lsp variant that it would correctly jump even in code that was still under the "yellow bar", while here it seems to jump successfully only for code that has been checked), maybe this is another low-level eglot/lsp issue

[Richard Copley]

I hadn't noticed, but that is handled by eglot and xref, and is probably all done by completely different code than under lsp-mode.

[Paul Nelson]

gotcha

[Richard Copley]

Alex J. Best said:

Paul Nelson said:

Alex J. Best said:

Is this https://github.com/leanprover/lean4-mode/pull/48 ? Except that that patch would no longer work as we now have .lake instead of lake-packages (and that directory name is configurable by the user anyway)

do you know what sorts of things people use in practice other than ".lake"?

I think nobody changes the default in practice ;), I'm just making the point that a more robust thing to do (more with respect to lean/lake itself changing than users) is to ask lake for this directory somehow.

I didn't see the point in updating the PR. The way it's done in my fork is workable but awkward. (The user can configure root directories by name, and excluded directories where the server will never start, using custom. If no applicable config is found, I look for the topmost ancestor directory with a lakefile.lean and start the server there.) Open to suggestions.

[Paul Nelson]

I saw this and feel you've addressed the issue elegantly in your fork

[Paul Nelson]

I guess if I had just started with your fork I'd have saved a bit of time

[Richard Copley]

In the vanilla version, the info-view is invalidated on every mouse-move (and there's a debouncing thing to mitigate the appalling fallout) :smile:

[Kevin Buzzard]

Is there any way of changing the title of this thread so that it more accurately captures the useful information contained within it?