Mathlib Global Installation

Stream: mathlib4

[Jon Eugster]

Does anybody have experience with getting a global mathlib installation to work? The background is that I want a fixed mathlib version built on the university server so that all students' lake projects reference this one as they don't have space for there own mathlib each. I'm facing in particular a few issues:

1. the lakefile seems to only allow relative paths require mathlib from ".."/"mathlib4", but not absolute ones, is that true?
2. even with the downloaded cache in the mathlib4 repo, opening the repo with the local mathlib import seems to try and rebuild all of mathlib. (and yes, the toolchain is correctly set)
3. this local import still clones all packages mathlib depends on into myproject/lake-packages/std and thelike.

Can anybody explain why any of these things happen? And does anybody know how to get a centralised mathlib? Do I need to manually put simlinks inside myproject/lake-packages/ maybe?

[Alexander Bentkamp]

Jon and I will probably use a custom packagesDir (https://github.com/leanprover/lake#package-configuration-options) instead. But still, it's weird that the local mathlib dependency does not work properly.

[Scott Morrison]

@Mac Malone may be able to answer questions 1. and 3., or otherwise record issues for them to address later.

[Scott Morrison]

2. sounds like a problem with cache (provided by Mathlib). If you could provide an easy to reproduce setup that shows this problem that would be helpful.

[Mac Malone]

@Jon Eugster Some answers:

1. Lake does do anything special to forbid them. However, as Lake may relocated package (as you see in 3), absolute paths will break often. This is because Lake prepends local requires with the prefix of the package, package directory, and workspace they are situated in.
2. Cache hard codes the directory structure of where it expects mathlib to be based on the default Lake setup. It does not use Lake's information. It assumes mathlib is either the root package or located with a folder called lake-packages.
3. Lake stores all non-local packages in the dependency tree with the workspace's packages directory (i.e., by default, lake-packages). You could can tell it store them elsewhere via the packagesDir configuration,, but that will still break cache.

[Scott Morrison]

@Mac Malone, can you advise how cache could get this information from lake?

[Scott Morrison]

In the long run this will just be taken over by cache's replacement, but it sounds like a fix for this is warranted now if possible.

[Mac Malone]

@Scott Morrison It would be a non-trivial addition and add non-trivial overhead (as it would need to either get lake to give them information to it or load the Lake configuration).

[Scott Morrison]

Is this on your roadmap? Should we create an issue for being able to access this information? Or should cache resort to regex'ing the lakefile for now? I don't particularly mind which, but this use case (deployment for a university course) seems worth supporting even if very hackily.

[Eric Wieser]

I think https://github.com/leanprover/lean4/pull/2542 is perhaps related here?

[Scott Morrison]

Indeed. Perhaps all the information needed is available in this incantation:

lake +leanprover/lean4-pr-releases:pr-release-2542 dump-config | jq -c '.packages[] | {dir, remoteUrl, libs: [.libs[] | {name, srcDir, roots}]}'

[Scott Morrison]

{"dir":"./lake-packages/std","remoteUrl":"https://github.com/leanprover/std4","libs":[{"name":"Std","srcDir":".","roots":["Std"]}]}
{"dir":"./lake-packages/Qq","remoteUrl":"https://github.com/gebner/quote4","libs":[{"name":"Qq","srcDir":".","roots":["Qq"]}]}
{"dir":"./lake-packages/aesop","remoteUrl":"https://github.com/JLimperg/aesop","libs":[{"name":"Aesop","srcDir":".","roots":["Aesop"]},{"name":"AesopTest","srcDir":".","roots":["AesopTest"]}]}
{"dir":"./lake-packages/Cli","remoteUrl":"https://github.com/mhuisi/lean4-cli","libs":[{"name":"Cli","srcDir":".","roots":["Cli"]}]}
{"dir":"./lake-packages/proofwidgets","remoteUrl":"https://github.com/EdAyers/ProofWidgets4","libs":[{"name":"ProofWidgets","srcDir":".","roots":["ProofWidgets"]}]}
{"dir":".","remoteUrl":null,"libs":[{"name":"Mathlib","srcDir":".","roots":["Mathlib"]},{"name":"Cache","srcDir":".","roots":["Cache"]},{"name":"MathlibExtras","srcDir":".","roots":["MathlibExtras"]},{"name":"Archive","srcDir":".","roots":["Archive"]},{"name":"Counterexamples","srcDir":".","roots":["Counterexamples"]},{"name":"ImportGraph","srcDir":".","roots":["ImportGraph"]},{"name":"docs","srcDir":".","roots":["docs"]}]}

[Scott Morrison]

I am liking lean4#2542. :-)

[Jon Eugster]

Thanks for the insight! I think my problem is not directly that cache breaks, but rather, that lake/lean is not able to use the build of a package. Here is a MWE:

git clone https://github.com/leanprover-community/mathlib4.git
cd mathlib4
lake exe cache get        # works all fine
cd ..
lake new MyProject
cp mathlib4/lean-toolchain MyProject/
cd MyProject
nano lakefile.lean                 # add `require mathlib from ".." / "mathlib4"`
nano MyProject.lean           # add `import Mathlib`
lake build                 # builds mathlib from scratch

Now, I think I start to understand why: The .oleans from the cache command are in mathlib4/build/lib/ but it seems that you can't use these when mathlib is imported as local packages, because we only use built oleans that lie inside MyProject/build/lib and there is nothing there yet. Does that sound correct @Mac Malone ?

[Mac Malone]

@Jon Eugster Lake does not hoist build files (currently). Thus, what you are doing there should work.

[Mac Malone]

I am confused why it is not.

[Mac Malone]

Is is just rebuilding mathlib or is it also rebuilding its dependencies?

[Mac Malone]

(I am most interested in what proof widgets is doing)

[Jon Eugster]

both. Although the dependencies I get because they are not actually the same ones, but clones thereof (MyProject/lake-packages/std as opposed to mathlib4/lake-packages/std) and there is no inherit reason these two have to be the same. And then mathlib has to be rebuilt against these new clones (which might apriori be different versions)

"Does not hoist", doesn't that mean you are expecting this to fail? Or do I missunderstand what hoist means?

[Mac Malone]

@Jon Eugster No, I am not expecting this to fail. "Hoist" here means copy the build files of a dependencies build directory into the root's build directory (which Lake does not do). It does however "hoist" dependencies (e.g., put mathlib's dependencies in MyProject's lake-packages rather than mathlib's).

[Mac Malone]

@Jon Eugster In addition to the relative import, you could also try setting MyProject's packagesDir to mathlib's lake-packages. For example:

package MyProject where
  packagesDir := ".." / "mathlib4" / "lake-packages"
  -- ...

[Jon Eugster]

Yea, Alex & I thought, the solution would be to do lake exe cache get && lake build inside MyProject, then take MyProject/lake-packages (which includes mathlib and all) and copy this manually to a central location and reference it with packagesDir. Your suggestion sounds quite similar to that. Ofc that's quite a hack, but I think that should would

[Jon Eugster]

Mac Malone said:

Jon Eugster No, I am not expecting this to fail. "Hoist" here means copy the build files of a dependencies build directory into the root's build directory (which Lake does not do). It does however "hoist" dependencies (e.g., put mathlib's dependencies in MyProject's lake-packages rather than mathlib's).

Now Im confused that Im expecting it to fail. When calling lake build inside MyProject, where exactly would you expect it to find the (mathlib/std)-olean files?

[Mac Malone]

@Jon Eugster Lake would expect to find mathlib's OLeans in ../mathlib4/build/lib and std's in MyProject/lake-packages/std/build/lib (without the change to packagesDir). Why that is not working confuses me too.

[Jon Eugster]

Mac Malone said:

Jon Eugster Lake would expect to find mathlib's OLeans in ../mathlib4/build/lib and std's in MyProject/lake-packages/std/build/lib. Why that is not working confuses me too.

and then it would use the mathlib-oleans mixed with std-oleans that might have a completely incompatible version? I agree though that your expectations are how I'd hoped it would work

I thought the entire point of the flat package structure was that if I update std to a newer version in my project, then all of mathlib would be rebuild against this newer version instead of relying on the std-version it was written for.

[Mac Malone]

Jon Eugster said:

and then it would use the mathlib-oleans mixed with std-oleans that might have a completely incompatible version?

No, it would/should rebuild them if the versions do not match. In fact, the current problem is that it thinks they do not for some reason despite the fact it should be getting which versions of mathlib's dependencies to download into MyProject's lake-packages from mathlib. (Unless MyProject is requesting new versions in its lakefile.lean?)

[Alexander Bentkamp]

@Mac Malone I tried the approach using packagesDir you suggested. It seems to work fine if all users have write access to the packagesDir. But I'd prefer to get it to work without write access if possible. Without write access, I get:

$ lake build
error: permission denied (error code: 13)
  file: /home/eugster/cgbf2023/lake-packages/std/build/lib/Std/Lean/Command.trace
error: permission denied (error code: 13)
  file: /home/eugster/cgbf2023/lake-packages/std/build/lib/Std/Tactic/Unreachable.trace
error: permission denied (error code: 13)
  file: /home/eugster/cgbf2023/lake-packages/std/build/lib/Std/Lean/Parser.trace
error: permission denied (error code: 13)
...

Why do the trace files need to be rewritten? lake exe cache get has already been performed by the other user who has write access.

[Mac Malone]

Alexander Bentkamp said:

Why do the trace files need to be rewritten? lake exe cache get has already been performed by the other user who has write access.

Was lake exe cache get and lake build run. Usually there are some files that still need to be built once after a lake exe cache get.

[Alexander Bentkamp]

Yes, I also ran lake build via the priviledged user.

[Alexander Bentkamp]

could it be that it happens because there are two different users?

[Mac Malone]

Alexander Bentkamp said:

Yes, I also ran lake build via the priviledged user.

Ah, this may be the problem. If the file is owned by a privileged user, and unprivileged user may be be unable to read it (which would prevent their Lake from checking the traces). Can you check the permissions on the file and ensure that it is readable by everyone (and probably do the same for the oleans and ileans as well).

[Alexander Bentkamp]

I set all files and directories to chmod 755. The trace files are definitely readable by the unpriviledged user.

[Kevin Buzzard]

When developing NNG and trying to get dev containers to work I once ended up with root downloading a bunch of files into lake-packages. I made all of them 777 expecting it would just fix the problem, but to my surprise it didn't. I didn't investigate any further though, I just deleted lake-packages

[Alexander Bentkamp]

Okay, that must have been something else. chmod 777 solves the issue. I'd just prefer not to give write access. Maybe it's because none of my two users is root?

[Mac Malone]

@Alexander Bentkamp That is weird. Lake shouldn't need write access to verify the files are up-to-date (and from Lake's code I cannot see a place where it would be trying to gain it). If you could produces a #mwe example of such a permissions error that may help debug it.

[Alexander Bentkamp]

Ok, I'll try.

[Alexander Bentkamp]

Sorry, can't reproduce it. It seems to go wrong only in our computer lab...

[Mac Malone]

Ah, the wonderful world of Heisenbugs. :sweat: