Disable lake post-hook when importing mathlib?

Stream: mathlib4

[Joachim Breitner]

It seems that since two days, lake update in a repository that imports mathlib does “stuff” (override my local toolchain, run lake cache). Is there a way to disable that, i.e. “import mathlib without post hooks”? It may not be the right thing to do in all cases, e.g. when I am intentionally testing a fork of lean.

Also (minor!) annoyances: the lean-toolchain file in mathlib has no terminating newline, and it seems to guess a wrong location for elan:

could not execute external process '/home/jojo/.elan/bin/elan'

maybe because of

$ which elan
/nix/store/ynxaiiw7pyrrm5has4wcipqy034dcpji-elan-1.4.5/bin/elan

@Mac Malone

[Mauricio Collares]

I'm seeing the same and have a PR at #8319, but I'm not sure if using "lake" from the PATH as in the PR is the best approach

[Mauricio Collares]

(The PR is not about disabling the hook, though. I agree it would be a good idea in case of overrides.)

[Mac Malone]

Ah, this is good to know! Issues like this are exactly the kind of thing I was hoping to discover by beta-testing this feature on Mathlib (as the next step is to implement a similar, but more general, approach in Lake).

[Mac Malone]

This seems like a communication probably between Lake and Elan. Lake assumes that Elan steps ELAN_HOME to the root of its installation and the its binaries are locating in $ELAN_HOME/bin. It sounds like this is not the case on Nix. I think @Sebastian Ullrich will need to weigh in here on how to properly find Elan on such systems.

[Mac Malone]

For now, as a stop-gap fix, my suggestion on @Mauricio Collares PR would be to just call Elan via elan directly (i.e., defaulting to one in PATH) rather than using Lake's detecting. Using the + option may work, but I have seen it break in the past under some circumstances.

[Joachim Breitner]

I agree that simply using the elan that's in the path is a good bet - all distro packaging would put the binary somewhere system wide, not just Nix's

[Mac Malone]

@Joachim Breitner As far as I understand, were the installer puts elan puts it is not the problem. Lake is not hard-coded to look for Elan in the home directory. The problem is that I assumed ELAN_HOME pointed to the root of Elan install (as it does on Windows). Apparently, ELAN_HOME is for something different. Fixing this detection will be important for future Lake features (e.g., lake install, local package cache, etc.). Maybe Lake should be guess and checking whether Lake is in <elan-root>/toolchains/<toolchain>/bin/lake and that elan is then located a <elan-root>/bin/elan, instead?

[Joachim Breitner]

I don't think that would work: why should elan the binary (in general) be installed in the directory that elan installs stuff into? The location of elan the binary is determined by how that program was installed (copied manually, package manager) - just like you expect lake to be in an elan-managed place, not a lake-managed place.

This is just a stop gap anyways, isn't it? because lake calling out to elan seems - to me - to be an odd inversion of control anyways as elan is (usually) the tool that installs lake.

Just using elan from the PATH doesn't work?

[Mac Malone]

Joachim Breitner said:

I don't think that would work: why should elan the binary (in general) be installed in the directory that elan installs stuff into?

While these can be theoretically separate, Elan also manages binaries of its own (e.g., lean, lake) that it are generally added to PATH. Personally, it makes more sense to me if these are all in the same directory (which can be added to PATH to get them all).

Joachim Breitner said:

This is just a stop gap anyways, isn't it? because lake calling out to elan seems - to me - to be an odd inversion of control anyways as elan is (usually) the tool that installs lake.

Lake calling Elan is not a stop gap at all. Lake will definitely need intimate knowledge of the Elan configuration to add and removes toolchain-wide packages (for a lake install a la cargo install). It will also need cooperation from Elan to manage global components (adding new shims for global packages which wish to install a toolchain-versioned executable to PATH). Admittedly, Cargo uses its own user-wide directory for this kind of stuff. However, in Cargo ecosystem, you can often build or install a crate from one Rust version and use it with another. Lean packages are generally locked to a toolchain (and need to be updated alongside them), so it makes more sense to store them under an Elan toolchain rather than beside it (and thus need to hack together synchronization with Elan).

Just using elan from the PATH doesn't work?

It is fine as a stop-gap. However, problems could arise if the elan in PATH is not the same as the elan which launched Lake (or at, the very least, if Lake cannot distinguish the two).

[Joachim Breitner]

Hmm, I don’t quite follow the first point. If I install elan from my distribution, it simply won’t be in ~/.elan/bin.

elan is already wrapping lake, and setting up an environment for it. So if lake calling back to elan is a supported use case, then elan should maybe set an environment variable ELAN_BINARY indicating how it wants to be called back? Such explicit coorporation between the tool might be more reliable than lake making assumptions about the dot-directories that elan manages.

[Mac Malone]

Joachim Breitner said:

So if lake calling back to elan is a supported use case, then elan should maybe set an environment variable ELAN_BINARY indicating how it wants to be called back? Such explicit coorporation between the tool might be more reliable than lake making assumptions about the dot-directories that elan manages.

Yes. I agree. I would bike shed and suggest ELAN as the environment variable (a la PYTHON). In fact, I had thought this was what I was already doing via using the ELAN_HOME that Elan sets. It was my understanding that elan was expected to be stored in the bin directory of ELAN_HOME (like lean is expected to be stored in bin directory of LEAN_SYSROOT), but I learned otherwise from this thread.