read tool-chain inside lakefile

Stream: lean4

[Jon Eugster]

I noticed, that one can do the following in the lakefile.lean:

import Lake
open Lake DSL

def getLeanToolchain : IO String := do
    let code ← IO.FS.readFile ⟨"lean-toolchain"⟩
    return code.replace "\n" "" |>.replace "leanprover/lean4:" ""

def leanVersion : String := match getLeanToolchain.run' () with
| none => ""
| some s => s

require mathlib from git
  "https://github.com/leanprover-community/mathlib4.git" @ leanVersion

With this, updating the lean-toolchain to the correct v4.x.0-version and calling lake update automatically fetches the correct mathlib version.

How wrong is this? Or is this fine? Is there maybe even an easier way to do this?

[Scott Morrison]

Note that I only create the v4.X.0 tags for Mathlib at the first commit where Mathlib moves to that version; it doesn't update after that.

[Scott Morrison]

I would say this is a horrible hack, that we will regret later, but is at least as good as the alternatives available right now. :-)

[Eric Wieser]

In Lean 3, we had leanproject --no-lean-upgrade, which effectively had this behavior. Is this something we want to restore?

[Jon Eugster]

Scott Morrison said:

Note that I only create the v4.X.0 tags for Mathlib at the first commit where Mathlib moves to that version; it doesn't update after that.

That's correct, and honestly I think that's convenient. I mainly use these tags because I want a slower updating pace that does not involve searching and copying commit-hashes. If you were to update the v4.X.0 tags automatically to the latest commit, I would just follow the frozen v4.(X-1).0 tag instead and wait another month.

[Mac Malone]

@Jon Eugster some code golf: you can use @ s!"v{Lean.versionString}" for the same result. :wink:

[Jon Eugster]

Mac Malone said:

Jon Eugster some code golf: you can use @ s!"v{Lean.versionString}" for the same result. :wink:

amazing, thx! Couldn't find that before.