mathlib for a specific lean version

Stream: new members

[Florent Schaffhauser]

Mathlib currently uses lean4:v4.9.0-rc1. What is the way to configure a project created today to use lean4:v4.8.0 with a compatible mathlib dependency?

This is my current lakefile.lean:

import Lake
open Lake DSL

package «leanproject» where
  -- Settings applied to both builds and interactive editing
  leanOptions := #[
    ⟨`pp.unicode.fun, true⟩, -- pretty-prints `fun a ↦ b`
    ⟨`pp.proofs.withType, false⟩
  ]
  -- add any additional package configuration options here

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

[Markus Himmel]

mathlib has a v4.8.0 tag, so you can update the last line of your lakefile to "https://github.com/leanprover-community/mathlib4.git" @ "v4.8.0" and update your lean-toolchain file to contain leanprover/lean4:v4.8.0. After that, lake update should get you in a working state.

[Florent Schaffhauser]

Thanks, I did not know how to use tags :blush: