Tell `lake build` to ignore a toolchain dependency?

Stream: lean4

[Rish Vaishnav]

My scenario is that I'm working with a custom lean toolchain that differs from some version X of Lean in a minor way that does not affect the generation of .olean files. I want to use this toolchain with a project that has been compiled for toolchain X, but when I change the lean-toolchain file and run lake build, this causes the entire project to rebuild (which is not ideal for mathlib4, for example).

So, my question is, is there a way to make lake ignore any changes to the toolchain, in the case that the user is confident that using the new toolchain doesn't require a rebuild?

[Mac Malone]

A feature for this use case was recently implemented in lean4#3609. However, this only works if the custom Lean toolchain is built with CHECK_OLEAN_VERSION=OFF (the default for development versions, but not Lean releases). As otherwsie, Lean itself will fail to load oleans from a different Lean version.

[Rish Vaishnav]

@Mac Malone That worked perfectly, and just in time, thanks so much! I have a couple follow-up questions:

1. I now have to use the lake binary that has been patched with your change, which is in stage1/bin. Is there a "correct" way to replace my current lake with this using Lean tooling? I guess I could always replace the binary in .elan/bin/lake, but that doesn't feel right.
2. When I do export LEAN_GITHASH=... and open a file importing mathlib in my editor, it seems that interactively, Lean is still trying to re-build all of the mathlib dependencies. Is this feature indeed limited to just lake build, or is there perhaps something wrong on my end?

[Mario Carneiro]

1. The way to switch between versions of lake is to use either toolchain overrides or +version. .elan/bin/lake is just a symlink to elan, you don't want to replace it. For example I have a toolchain called lean4 pointing to my development directory (i.e. path/to/lean4/build/release/stage1), set up via elan toolchain link lean4 <path>, so if I write lake +lean4 ... and it will run the development version of lake in the current directory.

[Mario Carneiro]

2. Most likely the issue is that the lean server is not using your patched version. If you use a toolchain override it will affect the server as well, but I think there is also a place you can specify this in the vscode settings

[Mac Malone]

Also, on (2), if you are using export rather than the VSCode setting for configuring server environment variables, you need to start VSCode from terminal after the export (which I imagine you are doing, but just wanted to make sure).

[Rish Vaishnav]

I seem to be having trouble with adding mathlib as a dependency in general. I've followed the instructions here, but with the attached example project when I do lake update && lake exe cache get! && lake build, it looks like it is still attempting to re-build all of mathlib. Do you notice anything wrong with it?
Laketest.tar.gz

[Rish Vaishnav]

Oh, I noticed that the output of cat .lake/packages/*/lean-toolchain lean-toolchain gives me a few different toolchains (though mathlib, std and the project's toolchains are in sync). Could that be why?

[Ruben Van de Velde]

No, if yours and mathlib's are in sync, that should be enough

[Ruben Van de Velde]

Try removing the .lake folder in your project and lake exe cache get again

[Rish Vaishnav]

Hmm, unfortunately that didn't work for me either... I don't know if the start of my build trace would be informative at all:

[1/15] Building Laketest.Basic
[1131/1166] Building Laketest
[4287/4293] Compiling Laketest.Basic
[4287/4294] Compiling Laketest
[4287/4295] Compiling Mathlib.Init.Data.Nat.Notation
[4287/4295] Compiling Mathlib.Mathport.Rename
[4287/4814] Compiling Std.CodeAction.Basic
[4287/4814] Compiling Std.Tactic.Init
[4287/4814] Compiling Mathlib.Lean.EnvExtension
[4287/4814] Compiling Std.Lean.Meta.Basic
[4287/4814] Compiling Std.Tactic.OpenPrivate
[4287/4814] Compiling Std.CodeAction.Deprecated
[4287/4814] Compiling Std.CodeAction.Attr
[4287/4814] Compiling Std.Lean.Position
[4287/4814] Compiling Std.Data.Nat.Lemmas
[4287/4814] Compiling Mathlib.Lean.Meta.Simp
[4287/4814] Compiling Std.Data.Nat.Basic
[4287/5081] Compiling Mathlib.Util.MemoFix
[4287/5092] Compiling Std.Tactic.Alias
[4287/5240] Compiling Mathlib.Lean.Expr.ReplaceRec
[4287/5240] Compiling Std.Tactic.Relation.Rfl
[4287/5240] Compiling Std.Data.Int.Order
[4289/5876] Compiling Std.Util.LibraryNote
[4289/5876] Compiling Std.Tactic.Lint.Basic
[4290/6604] Compiling Std.Tactic.Lint
[4291/8385] Compiling Mathlib.Lean.Meta
[4292/8463] Compiling Std.Data.List.Basic
[4293/8577] Compiling Std.Tactic.Lint.Misc
[4294/8577] Compiling Mathlib.Lean.Elab.Tactic.Basic
[4295/8577] Compiling Mathlib.Tactic.Relation.Trans

[Ruben Van de Velde]

8577 dependencies? That's very odd

[Ruben Van de Velde]

What does your lake-manifest.json look like?

[Rish Vaishnav]

Here it is:

{"version": 7,
 "packagesDir": ".lake/packages",
 "packages":
 [{"url": "https://github.com/leanprover/std4",
   "type": "git",
   "subDir": null,
   "rev": "ff9850c4726f6b9fb8d8e96980c3fcb2900be8bd",
   "name": "std",
   "manifestFile": "lake-manifest.json",
   "inputRev": "main",
   "inherited": true,
   "configFile": "lakefile.lean"},
  {"url": "https://github.com/leanprover-community/quote4",
   "type": "git",
   "subDir": null,
   "rev": "fd760831487e6835944e7eeed505522c9dd47563",
   "name": "Qq",
   "manifestFile": "lake-manifest.json",
   "inputRev": "master",
   "inherited": true,
   "configFile": "lakefile.lean"},
  {"url": "https://github.com/leanprover-community/aesop",
   "type": "git",
   "subDir": null,
   "rev": "056ca0fa8f5585539d0b940f532d9750c3a2270f",
   "name": "aesop",
   "manifestFile": "lake-manifest.json",
   "inputRev": "master",
   "inherited": true,
   "configFile": "lakefile.lean"},
  {"url": "https://github.com/leanprover-community/ProofWidgets4",
   "type": "git",
   "subDir": null,
   "rev": "fb65c476595a453a9b8ffc4a1cea2db3a89b9cd8",
   "name": "proofwidgets",
   "manifestFile": "lake-manifest.json",
   "inputRev": "v0.0.30",
   "inherited": true,
   "configFile": "lakefile.lean"},
  {"url": "https://github.com/leanprover/lean4-cli",
   "type": "git",
   "subDir": null,
   "rev": "a751d21d4b68c999accb6fc5d960538af26ad5ec",
   "name": "Cli",
   "manifestFile": "lake-manifest.json",
   "inputRev": "main",
   "inherited": true,
   "configFile": "lakefile.lean"},
  {"url": "https://github.com/leanprover-community/import-graph.git",
   "type": "git",
   "subDir": null,
   "rev": "64d082eeaad1a8e6bbb7c23b7a16b85a1715a02f",
   "name": "importGraph",
   "manifestFile": "lake-manifest.json",
   "inputRev": "main",
   "inherited": true,
   "configFile": "lakefile.lean"},
  {"url": "https://github.com/leanprover-community/mathlib4",
   "type": "git",
   "subDir": null,
   "rev": "fa48894a5d2780c6593a224003a660ca039e3e8f",
   "name": "mathlib",
   "manifestFile": "lake-manifest.json",
   "inputRev": "v4.7.0-rc1",
   "inherited": false,
   "configFile": "lakefile.lean"}],
 "name": "Laketest",
 "lakeDir": ".lake"}

[Ruben Van de Velde]

I'm stumped

[Mauricio Collares]

That's expected behaviour. Compiling steps (which generate native .o files and not oleans) are not cached, just Building ones. You're getting them because your target is a lean_exe. On the bright side, Compiling the whole of mathlib should be fast since it is mostly theorems. Most projects using mathlib as a dependency have no lean_exe targets, just lean_lib ones, and therefore you don't see that often.

[Ruben Van de Velde]

Ugh, I can never remember which is which

[Mauricio Collares]

I'm not saying this is desired behaviour, though. Being able to use mathlib's theorems without Compiling everything would be nice.

[Rish Vaishnav]

Alright, I guess I will accept it then, fortunately it does finish compiling everything within a reasonable amount of time.

However, I guess that making use of this new feature with a project that has a mathlib dependency means that you'll break the practice of keeping your project toolchain the same as that of your mathlib dependency (if you want to take advantage of pre-compiled olean files). @Mac Malone I noticed that this led to the following issues:

1. When I run lake update, it overrides my lean-toolchain file with that of the mathlib dependency.
2. If I then reset the lean-toolchain file to the custom toolchain, I can no longer run lake exe cache get, it results in the error:

Dependency Mathlib uses a different lean-toolchain
  Project uses rish987/lean4:lean2dk-v1
  Mathlib uses leanprover/lean4:v4.7.0-rc2

The cache will not work unless your project's toolchain matches Mathlib's toolchain
This can be achieved by copying the contents of the file `.lake/packages/mathlib/lean-toolchain`
into the `lean-toolchain` file at the root directory of your project

I think I would expect both of these to not happen if did an export LEAN_GITHASH=[hash of v4.7.0-rc2] first (though I understand this is a separate feature request to what was handled in lean4#3609).

[Mac Malone]

@Rish Vaishnav Ideally. you should not be changing the lean-toolchain file for mathlib-dependent projects. Mathlib relies on the toolchain matching itself for things like cache to work (as you observed). Instead, you should use elan override to override the package toolchain with your custom one.

[Mac Malone]

If you need to use a different toolchain for your dependent package (e.g., a PR toolchain) but want to still use mathlib's cache, that would be a feature request for Mathlib. IIRC, I believe it could work (the cache could download the files for mathlib's toolchain and just let Lake handle whether to rebuild). It would probably need a flag on Cache itself, though, b/c it still wants to present that error for the standard use case.

[Rish Vaishnav]

Alright, I'm actually quite happy with using elan override(along with setting LEAN_GITHASH). I won't insist on any new feature in Mathlib (for now), since my problem seems to be very specific. Thank you so much for the help!

[Kim Morrison]

@Rish Vaishnav, your alternative is to create a branch of Mathlib that uses your desired toolchain, and then refer directly that that in your lakefile.lean.

[Kim Morrison]

As soon as you push a branch to Mathlib, CI will start generating oleans that cache can use.

[Rish Vaishnav]

Oh cool, I think I will be taking advantage of that in the CI for my project repo. This LEAN_GITHASH trick should still be very useful for me as I iterate locally on my custom lean4 toolchain.