Using a read-only lib.

Stream: lean4

[Patrick Massot]

@Mac Malone How are we meant to use a library from a read-only folder? The naive idea of having require foo from "/usr/lib/foo" in the main project lakefile doesn't work. lake build ran from the main project seems to try to write at least in /usr/lib/foo/.lake/lakefile.olean.trace and /usr/lib/foo/.lake/lakefile.olean.lock. Having this difficult to setup is a huge regression compared to Lean 3. This is a very common case when teaching. It was already very useful in Lean 3 but now that Mathlib is 4Gb it becomes unavoidable.

[Mac Malone]

A read-only package folder is not currently a supported use case. Lake is expected to be reading-and writing from a build directory within the package folder. Changing this is possible, but had not yet come up as a priority. For comparison, Cargo will also fail if a crate is read-only.

[Kim Morrison]

Is there an issue for this? If not, let's make one asap, and then see what needs to be done to resolve it.

For teaching this is really important.

[Yury G. Kudryashov]

Did you try symlinking (or hardlinking) all files?

[Yury G. Kudryashov]

I know, this is a workaround, not a solution.

[Mac Malone]

It seems that it may also be worth clarifying whther Is the ultimate goal here specifically to support read-only packages or more generally to have a package cache / shared a dependent package across multiple projects.

[Yury G. Kudryashov]

I think that the goal is to have a shared dependency but this dependency has to be read-only if we don't want students to mess with other students' projects.

[Kim Morrison]

I don't think read-only packages per se are anyone's requirement. I think there are two things going on:

1. We need to support people with very limited writable storage (but larger read-only storage).
2. We need to do this soon, as currently someone investigating whether they can teach a Lean course may conclude that they can't because of this issue.

The combination of those two suggest that the path forward should be:

• lake just shrugs and does it's best when it can't write to a read-only directory
• later, a package cache / sharing dependent packages can provide a better solution.

[Patrick Massot]

The requirement is to be able to use Lean for teaching. Here the typical scenario is that student work in a computer lab where they have a small home directory but can access a system lib (or part of a teacher's home) in read-only.

[Patrick Massot]

Even without storage constraint it looks utterly crazy to me to tell students: in order to use Lean the only thing that is possible is that each student install mathlib in their home because it cannot be installed system-wide.

[Patrick Massot]

And again this was a complete non-issue with Lean 3. And I would have never imagined this could be an issue, even in my worst nightmares of the night before a new class starts.

[Mac Malone]

Patrick Massot I sympathsize with problem. Python's Anaconda gave me similar woes when trying to sandbox student notebooks. (Conda requires write access to sahred packages.) The way I solved it was precisely by ensuring each user had there own installation. AFAIK, that is the only way to achieve that in Python (e.g., see this StackOverflow question).

[Patrick Massot]

I've never heard of a programming language where you cannot install a library system-wide because using a library requires write access to the library folder.

[Patrick Massot]

I don't know what you are talking about when suggesting Python suffers from this. I have hundreds of python libs installed system wide and I don't need to sudo in order to use them.

[Kyle Miller]

Yury G. Kudryashov said:

Did you try symlinking (or hardlinking) all files?

It seems like this could work -- link the .lake/packages directory to a read only one, with pre-build oleans. Is there anything that could go wrong here, assuming that the main project has an unchanging manifest and lean-toolchain?

[Patrick Massot]

I will try after dinner.

[Kyle Miller]

If it does work, there could be a script in the meantime to set that kind of project up automatically. Maybe in the future lake might have some way to have pre-built libraries that you can link into your project like this? I hesitate suggesting to modify the lakefile with paths, since you should be able to, as a use, have your dependencies come from wherever you want.

[Mac Malone]

@Kyle Miller Unfortunately, that will not work. Lake currently writes to the .lake directory of dependent packages.

[Yury G. Kudryashov]

That's why I suggested symlinking all files by using something like lndir

[Kyle Miller]

When does it write to the .lake/packages/*/.lake directories? Does lake need to if everything is up-to-date?

[Kyle Miller]

(And let's assume that these are dependent packages that have been set aside to be dependent for some particular project, like a project students download for their course.)

[Mac Malone]

Patrick Massot said:

I don't know what you are talking about when suggesting Python suffers from this. I have hundreds of python libs installed system wide and I don't need to sudo in order to use them.

That has not been my experience (or that of the StackOverflow users in the question I linked). Are you sure those libraries are stored in a read-only location? In fact, there is a PIP Issues about it not supporitng read-only source trees. The key way it can get around this is by doing an "out-of-tree" build which means hoisting all the build results to the downstream package (which is exactly what you are trying to avoid here).

[Kyle Miller]

Back to caches, isn't a difference is that usually Python packages come with a cache of pre-built pyc files?

[Mac Malone]

My big confusion here is that it is not clear to me what one is expecting Lake to be doing if it cannot write files. The fundamental purpose of Lake is to write files (build modules and manage packages).

[Yury G. Kudryashov]

If it needs to rebuild a file in a package that is in a read-only directory, then IMHO it should fail.

[Mac Malone]

@Yury G. Kudryashov The problem is that for Lake to know whether it needs to build files, it often needs to write files (e.g., write lock files, download caches / metadata, etc.) so it needs somewhere to put those.

[Mac Malone]

However, despite this, there does exist some limited set of features (e.g., lake env and perhaps lake serve) that could conceivably be made to to work without write access.

[Mario Carneiro]

If everything is up to date, I don't see why lake would need to write any files

[Kyle Miller]

Does lake need to write a lockfile before checking that things are up-to-date? If so, maybe Lake can see if the directory is readonly and skip writing the lockfile?

[Mario Carneiro]

why would it even need to write-lock the directory if it isn't writing anything?

[Mac Malone]

It needs to read-lock?

[Mario Carneiro]

why is that a thing

[Mac Malone]

My goal here is to draw out more details of the intended use case and see if there that issue can be addressed (since the more general one sounds infeasible).

[Mario Carneiro]

what is the "more general one" in your mind?

[Mario Carneiro]

I agree with Kyle that if the directory is readonly then there is no need to read-lock

[Mac Malone]

Kyle Miller said:

Does lake need to write a lockfile before checking that things are up-to-date? If so, maybe Lake can see if the directory is readonly and skip writing the lockfile?

Interstingly, you have proposed the exact feature that was turned down by the Cargo team to address a similar issue.

However, I do think something like this could work.

[Kyle Miller]

An alternative idea I thought of was to have lake check for the existence of a .lake/packages/foo/readonly file, in case checking for readonly privileges is sketchy for some reason.

[Kyle Miller]

(Lake packages shouldn't have a readonly file themselves -- this is something you'd do to a dependency. It could be an error for Lake packages to have this file, that way it's free to use for this purpose.)

[Mac Malone]

Mario Carneiro said:

If everything is up to date, I don't see why lake would need to write any files

If everything is in fact "up-to-date" in the most complete sense of the word, I don't think Lake will try to write anything. Partick's initial example was a lakefile.olean.trace which should not be written again after it is written once if the configuration does not change.

[Mario Carneiro]

Does that use case actually work currently?

[Mario Carneiro]

it sounds like the writing of the lockfile will cause problems

[Mac Malone]

Lake only writes to the lock file if it needs to reconfigure.

[Mario Carneiro]

I would define an "up-to-date dependency" as containing olean.trace files

[Mario Carneiro]

Maybe this issue needs a MWE

[Mac Malone]

However, I think the problem may be that you need to acquire a write handle on a file to acquire a FS lock (even a read /shared lock) on the file (at least on Windows) and that may break on a read-only file.

[Mario Carneiro]

I guess the trouble is that lakefile.olean.trace files are not shipped by cache

[Mario Carneiro]

plus there are potentially some OS dependency issues with shipping everything in .lake to students

[Kyle Miller]

If we're in a shared filesystem situation, that might not be an issue since students wouldn't be downloading anything from that cache, assuming the dependency is fully built and on that shared filesystem

[Kyle Miller]

I think this is the setup that Patrick in particular wants to support. There are computer labs he uses for teaching.

[Mario Carneiro]

right, the point is that you need a special process to be able to set up that shared filesystem correctly though

[Patrick Massot]

Mac, we can't possibly be talking about the same thing. I can tell you there is no user-writable folder in my /usr/lib/python3/dist-packages. Why would there be?

[Patrick Massot]

I don't want to update or compile anything here. I want a fully compiled Mathlib living in a system-wide location that users can't write to without sudo.

[Mario Carneiro]

the easiest way would be to just set up a lake project similar to a student project, but using the admin account / with the shared FS being writable so that lake sets up the files the way it wants; then hopefully student projects will see that the dependency is already set up correctly and not do any further modification

[Patrick Massot]

And /usr/lib/ghc/ is also not writable.

[Mario Carneiro]

it's not clear to me whether the case I just described is in fact broken currently. Patrick do you have a repro?

[Patrick Massot]

I can tell you what I tried. I created a new user on my computer. Then I logged as this user and downloaded the verbose-lean4 library and fully build it. Then I made the whole folder readable to everybody. I switched back to my normal user and created a Lean project with the require line I indicated at the very beginning of this thread.

[Mario Carneiro]

See whether it makes a difference if you create a project depending on verbose-lean4 from the first user

[Mario Carneiro]

i.e. it might be that lake sets things up differently for root packages vs dependencies

[Mario Carneiro]

did the aforementioned .lake/lakefile.olean.trace and .lake/lakefile.olean.lock files already exist?

[Patrick Massot]

No they didn't.

[Mac Malone]

In particular, the fact that is was writing lakefile.olean.lock is concerning. That implies Lake was trying to reconfigure the package.

[Mario Carneiro]

What is the trigger for that?

[Mac Malone]

Patrick's answer of them not existing already is one reason.

[Mac Malone]

I am confused as to how he built the package without getting a lakefile.olean.trace in the process. though.

[Patrick Massot]

And also I doesn't only happen to me. We are having discussion because other people asked my help after hitting this wall.

[Patrick Massot]

I don't understand what you want me to try.

[Mac Malone]

Do you think you could provide a list of shell commands to repro this?

[Patrick Massot]

I will try to produce this list.

[Patrick Massot]

Maybe I will try without creating a new user, simply using sudo to put files in a read-only place.

[Mario Carneiro]

1. Make user newuser
2. Create project verbose-lean4 in /usr/lib/verbose-lean4 or wherever, with write access only by newuser
3. lake build verbose-lean4
4. Create project myproj in /home/newuser/myproj, require verbose-lean4 from "/usr/lib/verbose-lean4"
5. lake build myproj
6. switch to otheruser
7. Create project otherproj in /home/otheruser/otherproj, require verbose-lean4 from "/usr/lib/verbose-lean4"
8. lake build otherproj

[Patrick Massot]

You are making it more complicated than needed. I already fails with only one project depending on a readonly lib, no need to have two.

[Mario Carneiro]

my hope is that steps 1-5 will produce a /usr/lib/verbose-lean4 which is in the right state to be used in step 8

[Mario Carneiro]

if you skip steps 4-5 (which I think you did) some files may not be generated and cause a failure in step 8

[Mario Carneiro]

myproj is not actually being used here, it is only something which gets lake to compile verbose-lean4 as a dependency

[Patrick Massot]

I see.

[Patrick Massot]

I will try it here.

[Patrick Massot]

So you say we are missing a lake actually-build command?

[Patrick Massot]

Trying your procedure I realize the whole thing is doomed anyway because the dummy project in the middle is recloning its own copy of Mathlib instead of using the one that is already present and compiled in the verbose-lean4/.lake folder.

[Patrick Massot]

So I guess the actual project will also do this and we will end up duplicating Mathlib anyway.

[Patrick Massot]

Although I guess I could require verbose-lean4 and mathlib from the student project, although it certainly sounds stupid.

[Mario Carneiro]

yeah I think you have to do that

[Mario Carneiro]

also all of mathlib's dependencies...

[Mario Carneiro]

I think this is what "not a supported use case" looks like

[Patrick Massot]

Do you think I can do require foo from "/usr/lib/foo/.lake/lake-packages/mathlib" or will lake insist that mathlib should really be duplicated in /usr/lib?

[Mario Carneiro]

I think you can do that

[Patrick Massot]

The trick with the dummy package in the middle doesn't work.

[Patrick Massot]

Building the dummy package does not make the lib usable. lake still want to write in verbose-lean4/.lake/lakefile.olean.trace

[Patrick Massot]

And just in case someone asks when I'm away: all those projects have the same lean-toolchain file.

[Patrick Massot]

@Mac Malone even if you can't fix lake, can you at least write a message saying: I acknowledge that Python and Rust allow you to use a library that is installed on your system in a folder you can't write to? And that those Python and Rust discussions you linked to earlier have nothing to do with the current conversation?

[Mario Carneiro]

Patrick Massot said:

Building the dummy package does not make the lib usable. lake still want to write in verbose-lean4/.lake/lakefile.olean.trace

Does the lakefile.olean.trace file exist now?

[Mario Carneiro]

does building the dummy package create it and then delete it again or something?

[Mac Malone]

@Patrick Massot To clarify, I do think this use case is important and I do want to do the best I can to support it. We are currrently brainstorming ideas on how to do this. Our understanding of your constraints is as follows:

• In order to save space, Lake should be able to make use of a single shared hardcopy of the package (particularly, the soure files and build artifacts).
• Users must not be able to modify each other's instance of the shared package.
• Each user should be using the same version / configuration of the shared package.

[Julian Berman]

(Probably there's lots of prior art that might be useful, but perhaps PNPM can be of some inspiration as well: https://pnpm.io/motivation )

[Mac Malone]

@Julian Berman Yeah, a content-addressed store would certainly be the ideal way to solve this. That would likely be a longer-term solution, though.

[Joachim Breitner]

For me, writing to the location listed in requires violates the principle of least surprise: it seems to specify the location of sources, and I would not expect it to behave fundamentally different if there is a remote (e.g. git) location or a local (file) location, and would have expected that all intermediate files are written to the current project's .lake directory.

In particular I'd be surprised if this may modify files there. Maybe that other project has different toolchain or dependencies? I may be surprised to see those build files disappear, or see odd interactions if I rebuild there

But I admit that I wouldn't even expect it to share build artifacts with that other location, even though I can see why some would want or even expect that. And that may make it tricky.

[Kim Morrison]

Just noting in this thread that @Mac Malone has already made some initial progress on this problem, at lean#3254.

[Mac Malone]

To add on to @Scott Morrison's note, I believe lean4#3254 should fix the lakefile.olean.trace issue and a fully "up-to-date" read-only dependency should work with that PR release. I have tested it locally with a root-owned copy of mathlib and a user-level project and it worked for me, but I would be happy to have others test it as welll and see if they encoutner any errors.

[Patrick Massot]

What is the procedure to test this branch locally? Is there a toolchain we can give to elan?

[Mac Malone]

@Patrick Massot Yes, you can use leanprover/lean4-pr-releases:pr-release-3254 as your Lean toolchain to use the version of Lean from the PR. Right now there is only a Linux version, but I will get the CI to fix that shortly.

[Patrick Massot]

Thanks.

[Mac Malone]

Also, mathlib has been built on the release, so lake exe cache get should work as well (and did in my testing).

[Sebastian Ullrich]

@Patrick Massot Just to be clear, are we talking about the read-only folder being on some base image that is copied to each machine or on a network drive? In the latter case, access times would be a separate concern. But perhaps people here already have experience with serving mathlib oleans over the network?

[Patrick Massot]

I don't know the exact setup used by the colleagues who asked me this question. But both should work. Of course accessing Mathlib over the network will probably be slower but there is nothing Lean can do about that.

[Eric Wieser]

Mario Carneiro said:

I agree with Kyle that if the directory is readonly then there is no need to read-lock

I imagine that we don't care about this at all, but presumably this can fail when the directory is readonly to one user but writeable to another, and the latter is performing modifications.

[Kyle Miller]

I suppose that's a good reason to have a way to lock it permanently with a lockfile (like that readonly file suggestion)

[Patrick Massot]

I see a Mathlib branch at https://github.com/leanprover-community/mathlib4/commits/lean-pr-testing-3254/ whose name is promising but it doesn't seem to have oleans, even if I require the previous commt on that branch. Is it meant to have some?

[Kim Morrison]

Patrick Massot said:

but there is nothing Lean can do about that.

Well, in principle it could, by using ltar on the fly.

[Mauricio Collares]

Related: I love the Lean 4 mmap-able oleans, but symlinking .lake to a /run or /dev/shm subdirectory (two world-writable RAM-backed directories mounted by default in most Linux distros) could be a hacky way to get around disk space limitations if you have enough RAM; as long as you run lake exe cache get in every session, this simulates Lean 3 behaviour in a way.

[Patrick Massot]

Patrick Massot said:

I see a Mathlib branch at https://github.com/leanprover-community/mathlib4/commits/lean-pr-testing-3254/ whose name is promising but it doesn't seem to have oleans, even if I require the previous commit on that branch. Is it meant to have some?

@Mario Carneiro do you know the answer to this question?

[Mario Carneiro]

@Patrick Massot works fine for me on 0279e4fc

[Pierre Boutry]

Dear all, I am one of the colleagues Patrick mentioned. The PR seems to solve the issue. I will confirm this soon but regardless of the outcome of the other test that we will do tonight, I'd like to thank @Patrick Massot for raising the issue and @Mac Malone for the fix :)

[Pierre Boutry]

I have a follow-up question. Feel free to move my question to another topic if here is not the place to ask such a question. With our setup we get many warnings. So to give some details, we are using the https://github.com/PatrickMassot/verbose-lean4/tree/master project. I modified its lakefile.lean to the following thing.

import Lake
open Lake DSL

package verbose where
  leanOptions := #[
    ⟨`pp.unicode.fun, true⟩, -- pretty-prints `fun a ↦ b`
    ⟨`autoImplicit, false⟩,
    ⟨`relaxedAutoImplicit, false⟩,
    ⟨`pp.proofs.withType, false⟩]

require mathlib from git
  "https://github.com/leanprover-community/mathlib4.git"@"lean-pr-testing-3254"

@[default_target]
lean_lib Verbose where

I also modified the lean-toolchain file so it contains leanprover/lean4-pr-releases:pr-release-3254.

And for the "package" that contains the exercises for the students I have the following for the lakefile.lean.

import Lake
open Lake DSL

package «FCR» where

require verbose      from "/adhome/p/pi/pierre.boutry/FCR-LEAN-SETUP/verbose-lean4"
require mathlib      from "/adhome/p/pi/pierre.boutry/FCR-LEAN-SETUP/verbose-lean4/.lake/packages/mathlib"
require std          from "/adhome/p/pi/pierre.boutry/FCR-LEAN-SETUP/verbose-lean4/.lake/packages/std"
require Qq           from "/adhome/p/pi/pierre.boutry/FCR-LEAN-SETUP/verbose-lean4/.lake/packages/Qq"
require aesop        from "/adhome/p/pi/pierre.boutry/FCR-LEAN-SETUP/verbose-lean4/.lake/packages/aesop"
require proofwidgets from "/adhome/p/pi/pierre.boutry/FCR-LEAN-SETUP/verbose-lean4/.lake/packages/proofwidgets"
require Cli          from "/adhome/p/pi/pierre.boutry/FCR-LEAN-SETUP/verbose-lean4/.lake/packages/Cli"
require importGraph  from "/adhome/p/pi/pierre.boutry/FCR-LEAN-SETUP/verbose-lean4/.lake/packages/importGraph"

@[default_target]
lean_lib FCR where

When doing lake build one sees many warnings.

[Pierre Boutry]

Warning: .lake/packages/std/Std/Data/Int/Order.lean not found. Skipping all files that depend on it
Warning: .lake/packages/std/Std/Data/List/Basic.lean not found. Skipping all files that depend on it
Warning: .lake/packages/std/Std/Util/TermUnsafe.lean not found. Skipping all files that depend on it
Warning: .lake/packages/std/Std/Tactic/OpenPrivate.lean not found. Skipping all files that depend on it
Warning: .lake/packages/std/Std/Lean/Meta/DiscrTree.lean not found. Skipping all files that depend on it
Warning: .lake/packages/std/Std/Lean/NameMapAttribute.lean not found. Skipping all files that depend on it
Warning: .lake/packages/std/Std/Data/Option/Basic.lean not found. Skipping all files that depend on it
Warning: .lake/packages/std/Std/Tactic/CoeExt.lean not found. Skipping all files that depend on it
Warning: .lake/packages/std/Std/Tactic/Ext/Attr.lean not found. Skipping all files that depend on it
Warning: .lake/packages/std/Std/Tactic/Lint.lean not found. Skipping all files that depend on it
Warning: .lake/packages/std/Std/Tactic/Relation/Rfl.lean not found. Skipping all files that depend on it
Warning: .lake/packages/std/Std/Tactic/Relation/Symm.lean not found. Skipping all files that depend on it
Warning: .lake/packages/std/Std/CodeAction/Attr.lean not found. Skipping all files that depend on it
Warning: .lake/packages/std/Std/Tactic/Lint/Basic.lean not found. Skipping all files that depend on it
Warning: .lake/packages/std/Std/Lean/Expr.lean not found. Skipping all files that depend on it
Warning: .lake/packages/std/Std/Classes/Dvd.lean not found. Skipping all files that depend on it
Warning: .lake/packages/std/Std/Data/String/Basic.lean not found. Skipping all files that depend on it
Warning: .lake/packages/std/Std/Util/LibraryNote.lean not found. Skipping all files that depend on it
Warning: .lake/packages/std/Std/Data/Rat/Basic.lean not found. Skipping all files that depend on it
Warning: .lake/packages/std/Std.lean not found. Skipping all files that depend on it
Warning: .lake/packages/std/Std/Lean/Command.lean not found. Skipping all files that depend on it
Warning: .lake/packages/std/Std/Tactic/LabelAttr.lean not found. Skipping all files that depend on it
Warning: .lake/packages/std/Std/Classes/SetNotation.lean not found. Skipping all files that depend on it
Warning: .lake/packages/std/Std/Tactic/Ext.lean not found. Skipping all files that depend on it
Warning: .lake/packages/std/Std/Logic.lean not found. Skipping all files that depend on it
Warning: .lake/packages/std/Std/Tactic/Simpa.lean not found. Skipping all files that depend on it
Warning: .lake/packages/std/Std/Data/Nat/Lemmas.lean not found. Skipping all files that depend on it
Warning: .lake/packages/std/Std/WF.lean not found. Skipping all files that depend on it
Warning: .lake/packages/std/Std/Lean/Parser.lean not found. Skipping all files that depend on it
Warning: .lake/packages/std/Std/Tactic/LeftRight.lean not found. Skipping all files that depend on it
Warning: .lake/packages/std/Std/Data/HashMap/Basic.lean not found. Skipping all files that depend on it
Warning: .lake/packages/std/Std/Lean/SMap.lean not found. Skipping all files that depend on it
Warning: .lake/packages/std/Std/Linter/UnreachableTactic.lean not found. Skipping all files that depend on it
Warning: .lake/packages/std/Std/Util/ExtendedBinder.lean not found. Skipping all files that depend on it
Warning: .lake/packages/std/Std/Lean/Syntax.lean not found. Skipping all files that depend on it
Warning: .lake/packages/std/Std/Data/Bool.lean not found. Skipping all files that depend on it
Warning: .lake/packages/std/Std/Tactic/RCases.lean not found. Skipping all files that depend on it
Warning: .lake/packages/aesop/Aesop.lean not found. Skipping all files that depend on it
Warning: .lake/packages/Qq/Qq.lean not found. Skipping all files that depend on it
Warning: .lake/packages/importGraph/ImportGraph/Imports.lean not found. Skipping all files that depend on it
Warning: .lake/packages/std/Std/Lean/Meta/Inaccessible.lean not found. Skipping all files that depend on it
Warning: .lake/packages/std/Std/Util/Cache.lean not found. Skipping all files that depend on it
Warning: .lake/packages/std/Std/Tactic/TryThis.lean not found. Skipping all files that depend on it
Warning: .lake/packages/std/Std/Control/Nondet/Basic.lean not found. Skipping all files that depend on it
Warning: .lake/packages/std/Std/Util/Pickle.lean not found. Skipping all files that depend on it
Warning: .lake/packages/std/Std/Tactic/SolveByElim.lean not found. Skipping all files that depend on it
Warning: .lake/packages/std/Std/Data/MLList/Heartbeats.lean not found. Skipping all files that depend on it
Warning: .lake/packages/std/Std/Tactic/Replace.lean not found. Skipping all files that depend on it
Warning: .lake/packages/std/Std/Data/List/Init/Lemmas.lean not found. Skipping all files that depend on it
Warning: .lake/packages/std/Std/Data/MLList/Basic.lean not found. Skipping all files that depend on it
Warning: .lake/packages/std/Std/Tactic/GuardMsgs.lean not found. Skipping all files that depend on it
Warning: .lake/packages/Qq/Qq/Match.lean not found. Skipping all files that depend on it
Warning: .lake/packages/std/Std/CodeAction.lean not found. Skipping all files that depend on it
Warning: .lake/packages/proofwidgets/ProofWidgets/Component/MakeEditLink.lean not found. Skipping all files that depend on it
Warning: .lake/packages/proofwidgets/ProofWidgets/Component/OfRpcMethod.lean not found. Skipping all files that depend on it
Warning: .lake/packages/std/Std/Lean/CoreM.lean not found. Skipping all files that depend on it
Warning: .lake/packages/Qq/Qq/MetaM.lean not found. Skipping all files that depend on it
Warning: .lake/packages/std/Std/Tactic/SolveByElim/Backtrack.lean not found. Skipping all files that depend on it
Warning: .lake/packages/std/Std/Tactic/Basic.lean not found. Skipping all files that depend on it
Warning: .lake/packages/std/Std/Data/List/Lemmas.lean not found. Skipping all files that depend on it
Warning: .lake/packages/std/Std/Data/RBMap/Basic.lean not found. Skipping all files that depend on it
Warning: .lake/packages/std/Std/Tactic/HaveI.lean not found. Skipping all files that depend on it
Warning: .lake/packages/std/Std/Tactic/Exact.lean not found. Skipping all files that depend on it
Warning: .lake/packages/std/Std/Data/Fin/Basic.lean not found. Skipping all files that depend on it
Warning: .lake/packages/std/Std/Data/Option/Lemmas.lean not found. Skipping all files that depend on it
Warning: .lake/packages/std/Std/Data/Int/DivMod.lean not found. Skipping all files that depend on it
Warning: .lake/packages/std/Std/Tactic/Lint/Misc.lean not found. Skipping all files that depend on it
Warning: .lake/packages/std/Std/Tactic/Omega.lean not found. Skipping all files that depend on it
Warning: .lake/packages/std/Std/Tactic/NoMatch.lean not found. Skipping all files that depend on it
Warning: .lake/packages/std/Std/Tactic/Alias.lean not found. Skipping all files that depend on it
Warning: .lake/packages/std/Std/Data/BitVec.lean not found. Skipping all files that depend on it
Warning: .lake/packages/std/Std/Data/DList.lean not found. Skipping all files that depend on it
Warning: .lake/packages/std/Std/Data/RBMap/Lemmas.lean not found. Skipping all files that depend on it
Warning: .lake/packages/std/Std/Classes/Order.lean not found. Skipping all files that depend on it
Warning: .lake/packages/std/Std/Data/Nat/Gcd.lean not found. Skipping all files that depend on it
Warning: .lake/packages/std/Std/Data/Option/Init/Lemmas.lean not found. Skipping all files that depend on it
Warning: .lake/packages/std/Std/Tactic/Where.lean not found. Skipping all files that depend on it
Warning: .lake/packages/proofwidgets/ProofWidgets/Component/PenroseDiagram.lean not found. Skipping all files that depend on it
Warning: .lake/packages/proofwidgets/ProofWidgets/Presentation/Expr.lean not found. Skipping all files that depend on it
Warning: .lake/packages/std/Std/Data/List/Perm.lean not found. Skipping all files that depend on it
Warning: .lake/packages/std/Std/Data/HashMap/WF.lean not found. Skipping all files that depend on it

It would be nice to understand how to avoid them. They are actually surprising as the files can be found.

[Pierre Boutry]

Before checking whether they were there or not, I thought that maybe they were not downloaded as they were not required to build verbose-lean4. So I tried adding the dependencies for these packages in the lakefile.lean in the following way. It changed nothing but I prefer to specify it in case someone thinks it might allow to get rid of these warnings. And sorry for the multiple messages but the length of the warnings made posting this in one message impossible as I was going above the 10k characters allowed by message.

import Lake
open Lake DSL

package verbose where
  leanOptions := #[
    ⟨`pp.unicode.fun, true⟩, -- pretty-prints `fun a ↦ b`
    ⟨`autoImplicit, false⟩,
    ⟨`relaxedAutoImplicit, false⟩,
    ⟨`pp.proofs.withType, false⟩]

require mathlib      from git
  "https://github.com/leanprover-community/mathlib4"      @ "lean-pr-testing-3254"
require std          from git
  "https://github.com/leanprover/std4"                    @ "nightly-testing-2024-02-02"
require Qq           from git
  "https://github.com/leanprover-community/quote4"        @ "master"
require aesop        from git
  "https://github.com/leanprover-community/aesop"         @ "master"
require proofwidgets from git
  "https://github.com/leanprover-community/ProofWidgets4" @ "v0.0.27"
require Cli          from git
  "https://github.com/leanprover/lean4-cli"               @ "main"
require importGraph  from git
  "https://github.com/leanprover-community/import-graph"  @ "main"

@[default_target]
lean_lib Verbose where

[Kim Morrison]

@Pierre Boutry I don't have time to look at this all now. Could you please try to simplify your setup by using nightlies rather than lean-pr-testing-NNNN branches?

[Kim Morrison]

lean4#3254 merged 5 days ago. Hopefully you can find a nightly-YYYY-MM-DD that postdates that, and for which nightly-testing-YYYY-MM-DD exists on both Std and Mathlib.

[Kim Morrison]

If such a date does not exist, please complain. :-)

[Kim Morrison]

Mathlib has not been able to keep up recently, unfortunately, so the problem may be there.

[Pierre Boutry]

Scott Morrison said:

lean4#3254 merged 5 days ago. Hopefully you can find a nightly-YYYY-MM-DD that postdates that, and for which nightly-testing-YYYY-MM-DD exists on both Std and Mathlib.

I'll look at this tomorrow them. The next lab session is in 9 hours with a night in between so I would not want to mess up the setup. After the lab I will have plenty of time to do some tests.

[Kim Morrison]

(But do note that you are well beyond the "officially supported" setup here. :-) If you want to use Mathlib with a nightly or pr-testing-release, you're sort of expected to do the patching yourself. :-)

[Pierre Boutry]

Scott Morrison said:

(But do note that you are well beyond the "officially supported" setup here. :-) If you want to use Mathlib with a nightly or pr-testing-release, you're sort of expected to do the patching yourself. :-)

Is there a release to be expected soon with the merge PR btw?

[Kim Morrison]

Releases happen monthly. This patch will land in v4.7.0-rc1, targeted for March 1.

[Pierre Boutry]

Great :)

[Kim Morrison]

Assuming Mathlib is building against nightlies on the nightly-testing branch at that point, we will try to move Mathlib to that release the same day.

[Kim Morrison]

(But that assumption is currently invalid, so ...)

[Pierre Boutry]

I think the next lab would be on the 14th so maybe there is some hope.

[Kim Morrison]

We'll see what we can do.

[Kim Morrison]

I admit I am horrified to discover that someone is using a lean-pr-testing-NNNN branch in a lab with live humans. :-)

[Pierre Boutry]

Thanks. And no worries. It isn't really problematic. During the first session, I just had some students killing the program once they saw so many warnings and then I had to help those one by one which wasted some time. But I'll warn the ones I'll have tomorrow that it is to be expected hoping it is enough :)

[Pierre Boutry]

Scott Morrison said:

I admit I am horrified to discover that someone is using a lean-pr-testing-NNNN branch in a lab with live humans. :-)

When you read the above topic you'll understand. There was no prior way of sharing the mathlib. We have about 200 students so I'd rather avoid having about 1TB of mathlib on the university server :)

[Kim Morrison]

Sorry about this. I very much understand the problem with using shared distributions of Lean libraries, and am looking forward to having this behind us. I didn't mean that you were doing something wrong. The "horrified" was more along the lines of worried about what I got myself into by automating the production of the lean-pr-testing-NNNN branches!

[Pierre Boutry]

Scott Morrison said:

Pierre Boutry I don't have time to look at this all now. Could you please try to simplify your setup by using nightlies rather than lean-pr-testing-NNNN branches?

I have now switched to a newer version of lean, i.e. the content for my lean-toolchain is now leanprover/lean4:v4.7.0-rc2, and I still get the same warnings.

To provide some detail, here is the content of my lakefile.lean:

import Lake
open Lake DSL

package <C2><AB>FCR<C2><BB> where

require verbose      from "/adhome/p/pi/pierre.boutry/test/FCR/verbose-lean4"
require mathlib      from "/adhome/p/pi/pierre.boutry/test/FCR/verbose-lean4/.lake/packages/mathlib"
require std          from "/adhome/p/pi/pierre.boutry/test/FCR/verbose-lean4/.lake/packages/std"
require Qq           from "/adhome/p/pi/pierre.boutry/test/FCR/verbose-lean4/.lake/packages/Qq"
require aesop        from "/adhome/p/pi/pierre.boutry/test/FCR/verbose-lean4/.lake/packages/aesop"
require proofwidgets from "/adhome/p/pi/pierre.boutry/test/FCR/verbose-lean4/.lake/packages/proofwidgets"
require Cli          from "/adhome/p/pi/pierre.boutry/test/FCR/verbose-lean4/.lake/packages/Cli"
require importGraph  from "/adhome/p/pi/pierre.boutry/test/FCR/verbose-lean4/.lake/packages/importGraph"

@[default_target]
lean_lib FCR where

[Pierre Boutry]

A related question is if it it possible to define a variable that would contain the path /adhome/p/pi/pierre.boutry/test/FCR/verbose-lean4 in order to avoid the tedious and error prone repetition.

[Kevin Buzzard]

I don't have any real understanding of what you're actually supposed to be doing here, but let me make the following comment: I also have a project which needs mathlib, aesop, proof widgets, std etc but I don't have anything like this in my lakefile.lean (I just looked): the only thing I have is

package FLT where

require mathlib from git "https://github.com/leanprover-commu
nity/mathlib4.git"

and all the other stuff gets pulled in automatically as they're all dependencies of mathlib. My understanding is that doing it this way guarantees that the versions of all the mathlib dependencies are then sorted out by mathlib so I don't get issues with dependency conflicts. Sorry in advance if this is no help to you.

[Pierre Boutry]

Kevin Buzzard said:

I don't have any real understanding of what you're actually supposed to be doing here, but let me make the following comment: I also have a project which needs mathlib, aesop, proof widgets, std etc but I don't have anything like this in my lakefile.lean (I just looked): the only thing I have is

package FLT where

require mathlib from git "https://github.com/leanprover-commu
nity/mathlib4.git"

and all the other stuff gets pulled in automatically as they're all dependencies of mathlib. My understanding is that doing it this way guarantees that the versions of all the mathlib dependencies are then sorted out by mathlib so I don't get issues with dependency conflicts. Sorry in advance if this is no help to you.

I could drop this lines in another context. But here it is the package for a course. Given that there are more than 200 students following this course and that the mathlib takes up more than 4 GB of disk space, we wanted to share it. This is why I have these lines.

[Pierre Boutry]

I have downloaded the dependencies in my homedir and the students use them so as to avoid having more than 800 GB taken on the server.

[Pierre Boutry]

But yes I assume I would not have these warnings if I did not have these lines.

[Damiano Testa]

With respect to the shortening, does this work?

abbrev root : String := "/adhome/p/pi/pierre.boutry/test/FCR/verbose-lean4"
abbrev pack : String := "/.lake/packages/"

require verbose      from root
require mathlib      from root ++ pack ++ "mathlib"
require std          from root ++ pack ++ "std"
require Qq           from root ++ pack ++ "Qq"
require aesop        from root ++ pack ++ "aesop"
require proofwidgets from root ++ pack ++ "proofwidgets"
require Cli          from root ++ pack ++ "Cli"
require importGraph  from root ++ pack ++ "importGraph"

[Kim Morrison]

@Pierre Boutry, I'm sorry, I'm not sure what is going on here. Unfortunately this is a situation that is hard to debug remotely.

Could you try to come up with a minimal example of these warnings?

e.g. write a script that downloads a dependency into a fixed path, and uses the minimum number of dependencies possible? Or alternatively prepare a git repo that just has the upstream repo committed directly into the repo?

I think that to get to the bottom of this you're going to need to provide just a few lines that someone can type into a shell on a fresh computer (with elan installed, of course), and observe your problem.

[Kim Morrison]

@Pierre Boutry, the warning message you're reporting doesn't come from Lake or Lean itself, but rather from the cache tool provided in Mathlib. (Normally run via lake exe cache get.)

In your setup, you shouldn't be running cache at all: it's definitely not going to cope with read only directories. (Of course, you may want to run it before moving to the students's perspective, as you'll need to have all the oleans in place for them manually.)

[Kim Morrison]

You've said above that lake build produced those warnings.

[Kim Morrison]

That doesn't make sense to me: lake build does not result in lake exe cache get running (one day! :-), so I don't see a code path that could get from lake build to these warnings.

[Kim Morrison]

Are you in fact running some other command when you see these warnings?

[Pierre Boutry]

Damiano Testa said:

With respect to the shortening, does this work?

abbrev root : String := "/adhome/p/pi/pierre.boutry/test/FCR/verbose-lean4"
abbrev pack : String := "/.lake/packages/"

require verbose      from root
require mathlib      from root ++ pack ++ "mathlib"
require std          from root ++ pack ++ "std"
require Qq           from root ++ pack ++ "Qq"
require aesop        from root ++ pack ++ "aesop"
require proofwidgets from root ++ pack ++ "proofwidgets"
require Cli          from root ++ pack ++ "Cli"
require importGraph  from root ++ pack ++ "importGraph"

Thank you it works and does exactly what I had in mind.

[Eric Wieser]

Pierre Boutry said:

I could drop this lines in another context. But here it is the package for a course. Given that there are more than 200 students following this course and that the mathlib takes up more than 4 GB of disk space, we wanted to share it. This is why I have these lines.

I'd be curious to hear @Mac Malone's take on whether this this the right solution; as far I'm aware, your choices are:

• do what you're doing: override the origin of all your transitive dependencies
• modify the lakefile.lean within your local copies of transitive dependencies, to refer to each other

[Pierre Boutry]

I do not say it is the right solution. Just one that fits our needs. I would adapt it if there is a right solution of course.

[Pierre Boutry]

Scott Morrison said:

Pierre Boutry, I'm sorry, I'm not sure what is going on here. Unfortunately this is a situation that is hard to debug remotely.

Could you try to come up with a minimal example of these warnings?

e.g. write a script that downloads a dependency into a fixed path, and uses the minimum number of dependencies possible? Or alternatively prepare a git repo that just has the upstream repo committed directly into the repo?

I think that to get to the bottom of this you're going to need to provide just a few lines that someone can type into a shell on a fresh computer (with elan installed, of course), and observe your problem.

I will try.

[Pierre Boutry]

Scott Morrison said:

Pierre Boutry, the warning message you're reporting doesn't come from Lake or Lean itself, but rather from the cache tool provided in Mathlib. (Normally run via lake exe cache get.)

In your setup, you shouldn't be running cache at all: it's definitely not going to cope with read only directories. (Of course, you may want to run it before moving to the students's perspective, as you'll need to have all the oleans in place for them manually.)

I only run lake exe cache get to get the dependencies for verbose-lean. And then for the "package" that depends on it I simply do lake build.

[Kim Morrison]

Ah, okay. lake exe cache get is not going to work if your lakefile has relative paths: the warnings are not really surprising.

[Kim Morrison]

You're more or less responsible at this point to put the oleans in the right place.

[Kim Morrison]

But it sounds like your students won't see any warnings, right? So all is well?

[Pierre Boutry]

Scott Morrison said:

Ah, okay. lake exe cache get is not going to work if your lakefile has relative paths: the warnings are not really surprising.

I do not do lake exe cache get there. Only for verbose-lean. I taught this morning and do so again this afternoon. I'll write a script to replicate the bug afterwards. I believe it will make things clearer.

[Pierre Boutry]

Scott Morrison said:

But it sounds like your students won't see any warnings, right? So all is well?

They do. At least it did this morning and the last time I tested. Let's see once I will have sent the script.

[Kim Morrison]

If your students are seeing it, that it means that lake exe cache get is running in their system. That is not going to work.

[Pierre Boutry]

#!/usr/bin/bash

# Add the elan bin from my (pierre.boutry) home to the path of each student
touch ~/.profile
[ -d ~/.elan ] || ln -s /adhome/p/pi/pierre.boutry/.elan/ ~/.elan
grep -q "export PATH=\"\$HOME\/\.elan\/bin:\$PATH\"" ~/.profile || echo 'export PATH="$HOME/.elan/bin:$PATH"' >> ~/.profile
export PATH="$HOME/.elan/bin:$PATH"

# Install the Lean4 VS Code extension (the folder is less than 3MB so I think it won't be a problem to not share it)
code --install-extension leanprover.lean4

# Copy the skeleton of the erxercises for the labs to the root of the home dir of the students and build the package
MyCurrentPath=$PWD
mkdir -p ~/FCR/FCR
mkdir -p ~/FCR/.vscode
cd ~/FCR
cp /adhome/p/pi/pierre.boutry/FCR-LEAN-SETUP/FCR/FCR.lean       .
cp /adhome/p/pi/pierre.boutry/FCR-LEAN-SETUP/FCR/lakefile.lean  .
cp /adhome/p/pi/pierre.boutry/FCR-LEAN-SETUP/FCR/lean-toolchain .
cp /adhome/p/pi/pierre.boutry/FCR-LEAN-SETUP/FCR/.vscode/settings.json .vscode/
[ -f ~/FCR/FCR/TP1.lean ] || cp /adhome/p/pi/pierre.boutry/FCR-LEAN-SETUP/FCR/FCR/TP1.lean FCR/
[ -f ~/FCR/FCR/TP2.lean ] || cp /adhome/p/pi/pierre.boutry/FCR-LEAN-SETUP/FCR/FCR/TP2.lean FCR/
lake build
cd $MyCurrentPath

This won't allow to reproduce the bug as it is just the script, that I also want to cleanup, that sets things up for them. As you can see there is no lake exe cache get there.

[Kim Morrison]

The warning messages you quoted above are definitely from cache. So the challenge is to work out which step is running it.

[Pierre Boutry]

Locating it should be easy. I can just try to comment out lines and see the minimal number of comments needed to avoid them. Then it will mean that the commented line(s) are the ones triggering lake exe cache get.

[Kevin Buzzard]

Oh surely it's lake build

[Kevin Buzzard]

I am not an expert in the infrastructure so do take this message with a pinch of salt. But my memory is that lake build was changed relatively recently to do lake exe cache get first, because people were complaining that obviously if you want to build your project then you always want to download all relevant oleans first.

Apologies if this is a red herring.

[Ruben Van de Velde]

I don't think that's true, Kevin. I think you remember lake update calling lake exe cache get in projects that depend on mathlib

[Eric Wieser]

I think lake build might do a lake update if the manifest is out of date with the lakefile?

[Kevin Buzzard]

Aah maybe that's what I'm remembering

[Eric Wieser]

There's a flag you can set to tell lake update not to run cache get

[Jon Eugster]

Eric Wieser said:

There's a flag you can set to tell lake update not to run cache get

You can set the env variable MATHLIB_NO_CACHE_ON_UPDATE=1, which can be looked up in mathlib's lakefile.lean

And lake build warns you about an outdated lake_manifest.json, but I don't think it runs lake update, unless there is no lake_manifest.json at all.
(which is the case in the script posted above, so yes, here lake build will call the lake post-update-hook which calls lake exe cache get)

[Pierre Boutry]

Jon Eugster said:

MATHLIB_NO_CACHE_ON_UPDATE=1

Thanks as your mention of fact that an outdated, or in my case missing, lake_manifest.json file leads to warning made me realize I was not copying it to their copy. It seems to do the trick now. I have asked someone else to test to confirm. Thank you :)