System-wide Lean install

Stream: lean4

[Patrick Massot]

I need to prepare distribution of Lean for my teaching. With Lean 3 it was super easy, I was able to make a debian package for my IT people and they would happily install it. The debian package was super simple, it would dump to /usr/lib the content of the lib folder in a Lean release (say https://github.com/leanprover-community/lean/releases/download/v3.51.1/lean-3.51.1-linux.tar.gz) and to /usr/bin the content of the bin folder. It was nice and tidy because the lib folder contained exactly one thing: a lean folder. I thought it would be the same with Lean 4, only 50 times bigger. But I see

ls ~/.elan/toolchains/leanprover--lean4---v4.15.0/lib
clang         libatomic.so.1      libclang-cpp.so.15  libLLVM-15.so     libz.so.1
crt1.o        libatomic.so.1.2.0  libc++.so           libLLVM.so        libz.so.1.2.11
crti.o        libc++.a            libc++.so.1         libunwind.a       Mcrt1.o
crtn.o        libc++abi.a         libc++.so.1.0       libunwind.so      Scrt1.o
gcrt1.o       libc++abi.so        libgcc_s.so         libunwind.so.1
glibc         libc++abi.so.1      libgcc_s.so.1       libunwind.so.1.0
lean          libc++abi.so.1.0    libgmp.a            libuv.a
libatomic.so  libclang-cpp.so     libLLVM-15.0.1.so   libz.so

so I clearly don’t to put that in /usr/lib/, that would very likely brick the system for everybody. Is there anything I can do @Sebastian Ullrich?

[Patrick Massot]

Needless to say, storing a Lean toolchain in students home is completely impossible.

[Sebastian Ullrich]

Where are you planning to store Mathlib?

[Sebastian Ullrich]

I don't know much about Debian packaging but the usual solution is to install everything into a separate directory such as /opt/lean4 or /usr/local/lean4. The only additional step is that you then need to get that path's bin/ into PATH or into the VS Code settings

[Patrick Massot]

Ok, I didn’t think about using a /opt folder.

[Patrick Massot]

I’ll try that.

[Patrick Massot]

Thanks

[Mauricio Collares]

Hot take: This would be easier if the Lean community wasn't so opposed to distros packaging individual versions of lean. It is an important use case (downloading non-distro-provided binaries from the internet is a risk in general, although it is very convenient for upstream), and it wouldn't be impossible to print out diagnostic error messages in case of toolchain mismatches when the user's not using elan.

[Mauricio Collares]

I do agree that not using elan is a bad idea if you're contributing to mathlib, though.

[Sebastian Ullrich]

Even just having two different courses that want to use Lean may make a single global installation awkward very quickly

[Patrick Massot]

That applies to any software, and never preventing people packaging stuff.

[Patrick Massot]

And to be honest we’re not yet having to face two Lean courses in the same department.

[Patrick Massot]

I thought the issue of system-wide install of libs was solved last year, but it doesn’t seem true. What is the current workaround?

[Patrick Massot]

I have

cat lakefile.toml

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

[[lean_lib]]
name = "Test"

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


[[require]]
name = "mathlib"
path = "/opt/lean/lib/mathlib"

$ lake build
info: test: no previous manifest, creating one from scratch
info: toolchain not updated; already up-to-date
error: permission denied (error code: 13)
  file: /opt/lean/lib/mathlib/.lake/lakefile.olean.lock

[Patrick Massot]

Needless to say, the copy of Mathlib in /opt/lean is fully compiled.

[Patrick Massot]

@Mac Malone and @Sebastian Ullrich, almost one year after #lean4 > Using a read-only lib. , what is the current status? I know I should have asked one month ago before investing so much into trying to prepare some teaching using Lean 4, but my memory from last year thread was that there was a solution. The issue is simple. I want to teach using Lean in a computer lab. I cannot have a copy of Lean+mathlib into each student home. It’s not even a size only issue, the home directories are remote and accessing them would kill usability of Lean. I can ask once to put stuff in /opt/ on all machines. The Lean toolchain and Mathlib need to live there. Then students will have exercises files and a course specific small lib in their home folder. Currently I have in /opt/lean the content of my .elan/toolchains/leanprover--lean4---v4.15.0 and a compiled mathlib. I guess I should also put the dependencies of mathlib somehow. Then what? How do I create a project in user space that will access those resources without have write-access to /opt/lean?

[Sebastian Ullrich]

As far as I know, it trying to create lakefile.olean.lock means that it believes the lakefile.olean is not up to date, so we would have to debug why it thinks that.

I guess I should also put the dependencies of mathlib somehow

Should they not already be part of the same mathlib/.lake directory?

[Patrick Massot]

I don’t know. The whole thing is a complete mystery to me.

[Patrick Massot]

It’s many orders of magnitude more mysterious than the Lean 3 analogue where you had lean files and olean files and nothing else.

[Patrick Massot]

Since this week office hours were cancelled, maybe we could have some office hours about that?

[Patrick Massot]

But really I hope the spec is pretty clear and reproducible.

[Patrick Massot]

One way to say it is: how can I put stuff in a read-only folder and then modify the lakefile/lake-manifest/lean-toolchain at https://github.com/PatrickMassot/verbose-lean4/ so that it sues the read-only folder.

[Sebastian Ullrich]

This is the extent of my knowledge, Mac will have to take over

[Patrick Massot]

The actual situation is slightly more complex because I have a lib with exercises depending on Verbose-lean, but I could simply put Verbose-lean inside to get back to the previous case.

[Patrick Massot]

And in the mean time I get emails from my colleagues who teach with me but never use Lean otherwise. They ask why we are switching to Lean 4 which has no tada emoji when a proof is complete and where the goal display depends randomly on the cursor position :cry:

[Patrick Massot]

The pressure from them to switch back to Lean 3 is pretty strong, but that lake question may settle it anyway.

[Marc Huisinga]

Patrick Massot said:

where the goal display depends randomly on the cursor position :cry:

Please file a bug report in the Lean 4 repository.

[Patrick Massot]

Maybe I’m making progress. I try to use sudo lake on my machine until I reach a fixed point and then can use lake as a normal user.

[Patrick Massot]

Now I need to copy back the resulting /opt folder into user space, turn into a deb file again, install the deb file and pray.

[Patrick Massot]

I really hope next year this will be unneeded and I’ll attend Lean Together instead.

[Patrick Massot]

It seems to work! Now I need to try in a VM with a fresh Linux Mint install.

[Sebastian Ullrich]

Was there something specific you had to change? Or fix unclear?

[Patrick Massot]

From last year thread by Pierre I took the idea of putting all dependencies of mathlib as top-level require in lakefile.toml. So I have a version of Verbose-lean whose lakefile.toml is:

name = "verbose"
defaultTargets = ["Verbose"]

[leanOptions]
pp.unicode.fun = true
autoImplicit = false
relaxedAutoImplicit = false
pp.proofs.withType = false

[[require]]
name = "mathlib"
path = "/opt/lean/lib/mathlib"
rev = "v4.15.0-patch1"

[[require]]
name = "aesop"
path = "/opt/lean/lib/aesop"

[[require]]
name = "batteries"
path = "/opt/lean/lib/batteries"

[[require]]
name = "Cli"
path = "/opt/lean/lib/Cli"

[[require]]
name = "importGraph"
path = "/opt/lean/lib/importGraph/"

[[require]]
name = "LeanSearchClient"
path = "/opt/lean/lib/LeanSearchClient/"

[[require]]
name = "plausible"
path = "/opt/lean/lib/plausible"

[[require]]
name = "proofwidgets"
path = "/opt/lean/lib/proofwidgets/"

[[require]]
name = "Qq"
path = "/opt/lean/lib/Qq"

[[lean_lib]]
name = "Verbose"

And then there was the trick of using sudo /opt/lean/bin/lake build from user space before being able to do the same without sudo.

[Patrick Massot]

I did something really stupid: I created a VM with only 25Gb of disk space…

[Patrick Massot]

While I’m creating a new VM, my colleague sent me an email saying she asked ChatGPT to fix Lean 4 and the answer was we should write

import tactic
-- Tactique pour afficher un message lorsque tous les buts sont résolus
meta def show_message_if_done : tactic unit :=
do
  goals ← tactic.get_goals,   -- Récupère la liste des buts actuels
  if goals.empty then         -- Si aucun but n'est restant
    io.println "Gagné",       -- Affiche "Gagné"
  else
    return ()                 -- Sinon, ne rien faire
-- Exemple d'utilisation de cette tactique
example : 1 + 1 = 2 :=
begin
  refl,
  show_message_if_done,  -- Vérifie si tous les buts sont résolus
end

[Patrick Massot]

I would say this is a nice effort by ChatGPT. And also it’s clear I won’t be able to force my colleague to use Lean 4 if I don’t implement something like this in my exercise macro.

[Patrick Massot]

I’m not only writing this because I’m waiting on the VM. I think it’s an interesting data point for the core team. I didn’t anticipate the reaction to this issue would be so strong.

[Henrik Böving]

Luckil it's trivial:

import Lean

open Lean

elab "show_message_if_done" : tactic => do
  let goals ← Elab.Tactic.getGoals
  if goals.isEmpty then
    logInfo "Gagné"

example : 1 + 1 = 2 := by
  rfl
  show_message_if_done

[Patrick Massot]

I know that detecting the absence of goals trivial, and chatGPT almost got it right. I need a better version because logInfo is not really the right, but I’ll do it.

[Patrick Massot]

I can play with such things now that the deb file seems to be working. Of course I won’t know for sure until it’s deployed into actual computer labs instead of a VM, but I cannot do anything more at this stage.

[Kim Morrison]

(This is not relevant for Patrick this week, but for the future.)

I think we should set up a test case, that is run e.g. by Mathlib CI, that verifies that a project with local links to all dependencies in read-only directories works.

This would be an analogue of the new DownstreamTest directory we've installed in Mathlib, which verifies that a downstream-of-Mathlib project can successively retrieve and use the Mathlib cache. (Importantly, this is part of Mathlib, so it gets tested on every nightly release of Lean.)

This might be a variant of the existing DownstreamTest, but we run the test inside bubblewrap to ensure that it works even if the ../ path is (virtually) read-only.

[Patrick Massot]

This would indeed be very nice. And documenting the whole thing would be very nice.

[Kim Morrison]

I think something we need to make system-wide installs sane is the option to tell Lake that when we use path = "/x/y/z", transitive dependencies of that require should live in the .lake folder of that path, not in the local .lake folder. This would remove the need to inline all the [[require]] statements for transitive dependencies as Patrick has done above.

@Mac Malone, is this a possibility? I hope it is. :-)

[Patrick Massot]

Talking about documentation, let me record here that such “weird” setup require ask forgiveness to the VSCode extension. There is an option (thank Marc!) to switch off setup warnings that needs to be activated in order to avoid having students seeing alarming messages about elan not being found.

[Marc Huisinga]

See also this section in the vscode-lean4 manual.

[Mac Malone]

Kim Morrison said:

I think something we need to make system-wide installs sane is the option to tell Lake that when we use path = "/x/y/z", transitive dependencies of that require should live in the .lake folder of that path, not in the local .lake folder. This would remove the need to inline all the [[require]] statements for transitive dependencies as Patrick has done above.

Mac Malone, is this a possibility? I hope it is. :-)

One way to approximate this with the current behavior is to set packagesDir as Henrik did in the doc-gen4 case. Lake will use said directory to resolve all remote dependencies For example,

packagesDir = "/opt/lean/lib"

[[require]]
name = "mathlib"
rev = "v4.15.0-patch1"

Will use /opt/lean/lib to store (and retrieve) the cloned copy of Mathlib and all its transitive dependencies.

[François G. Dorais]

@Mac Malone Would it be difficult to make packagesDir an Array String to search through for a matching package?

[Mac Malone]

@François G. Dorais Nontrivial. It is oiginally designed to merely be the the place where cloned repositories are stored, so it the code is not really structured around it operating a search path.

[François G. Dorais]

Thanks. To be clear: that was an honest question and not a request. I entertained the idea for a bit but I don't think I have a current need for this feature.

[Patrick Massot]

Thanks Mac. It’s too late for this year but it may help next year (although I hope there will be an easier way to setup things by then). What led me away from this trying this option when reading doc at https://github.com/leanprover/lean4/blob/master/src/lake/README.md#layout was the “These options control the top-level directory layout of the package” which I read as saying “those options are all about stuff that live inside the working copy of your project git repository” whereas you’re saying this can refer to any folder in the system.