getting mathlib running

Stream: mathlib4

[Kevin Buzzard]

I haven't thought about mathlib4 for a while but now my teaching for this term is quietening down I wanted to see the state of mathlib4; but I don't know how to get it running any more. I don't know what a lakefile is etc. I've pulled from origin and now I just seem to have orange bars. Can someone get me back up to speed? Maybe it would be good to have a brief description in the README about how to get this package running, or perhaps a link to the relevant docs in the lean 4 ecosystem, if such docs exist? Sorry for such a noob question. I don't even know how to compile oleans -- lean --make src doesn't seem to work any more (and might never have done with Lean 4, I don't remember what little I knew over the summer when I was writing Lean 4 code).

[Scott Morrison]

lake build should be all you need. I will write some README later today.

[Scott Morrison]

You may want to check your VSCode Lean4 extension is up to date as well, as it changed a bit when lake came along.

[Kevin Buzzard]

Oh many thanks for the prompt response! I'll see if I have lake

[Scott Morrison]

I suspect there is not a lot of hand-porting to be done at the moment; although I think feel free to do some for practice! Really tactics are what mathlib4 needs at the moment.

[Scott Morrison]

Unfortunately at the moment mathport takes a few hours to run, although it is close to up-to-date with mathlib4, and the build process has been simplified in the last few days. I'm hoping soon to have CI for mathport, and easily downloaded artifacts, so the barrier to looking at what it produces can be much lower. That said, what it produces is still full of errors. :-)

[Kevin Buzzard]

I get command 'lake' not found as I suspected I would -- where do I get this?

[David Renshaw]

I had to re-install elan to get it to work

[Kevin Buzzard]

As for the extension, VS Code seems to be telling me I have v0.0.41. Is this the right version? I don't know how to check. I don't know anything :-)

[Kevin Buzzard]

Aah great, elan update has given me lake

[Kevin Buzzard]

woohoo I'm up and running! Thanks Scott and David!

[Julian Berman]

Kevin Buzzard said:

As for the extension, VS Code seems to be telling me I have v0.0.41. Is this the right version? I don't know how to check. I don't know anything :-)

A decent lazy way to answer this is to check that the last version on the vscode lean releases page matches: https://github.com/leanprover/vscode-lean4/releases

(It does, so you're good!)

[Julian Berman]

mathlib4 doesn't build on latest Lean4 at the minute correct? I know its lean-toolchain file lists an earlier version, so that's me being lazy, but just to be sure, I get:

> LEAN_PATH=./build/lib /opt/homebrew/Cellar/lean@4/HEAD-d5e05f3/bin/lean -R ./. -o ./build/lib/Mathlib/Tactic/Cache.olean ././Mathlib/Tactic/Cache.lean
error: external command /opt/homebrew/Cellar/lean@4/HEAD-d5e05f3/bin/lean exited with status 1
error: build failed
././Mathlib/Tactic/Cache.lean:72:16: error: type mismatch
  IO.asTask
    (EIO.toIO'
      (let metaCtx :=
        { config :=
            { foApprox := false, ctxApprox := false, quasiPatternApprox := false, constApprox := false,
              isDefEqStuckEx := false, transparency := TransparencyMode.default, zetaNonDep := true, trackZeta := false,
              unificationHints := true, proofIrrelevance := true, assignSyntheticOpaque := false,
              ignoreLevelMVarDepth := true, offsetCnstrs := true },
          lctx :=
            { fvarIdToDecl :=
                { root := Std.PersistentHashMap.Node.entries Std.PersistentHashMap.mkEmptyEntriesArray, size := 0 },
              decls :=
                { root := Std.PersistentArrayNode.node (Array.mkEmpty (USize.toNat Std.PersistentArray.branching)),
                  tail := Array.mkEmpty (USize.toNat Std.PersistentArray.branching), size := 0,
                  shift := Std.PersistentArray.initShift, tailOff := 0 } },
          localInstances := #[], defEqCtx? := none, synthPendingDepth := 0 };
      let metaState :=
        { mctx :=
            { depth := 0, mvarCounter := 0,
              lDepth :=
                { root := Std.PersistentHashMap.Node.entries Std.PersistentHashMap.mkEmptyEntriesArray, size := 0 },
              decls :=
                { root := Std.PersistentHashMap.Node.entries Std.PersistentHashMap.mkEmptyEntriesArray, size := 0 },
              userNames :=
                { root := Std.PersistentHashMap.Node.entries Std.PersistentHashMap.mkEmptyEntriesArray, size := 0 },
              lAssignment :=
                { root := Std.PersistentHashMap.Node.entries Std.PersistentHashMap.mkEmptyEntriesArray, size := 0 },
              eAssignment :=
                { root := Std.PersistentHashMap.Node.entries Std.PersistentHashMap.mkEmptyEntriesArray, size := 0 },
              dAssignment :=
                { root := Std.PersistentHashMap.Node.entries Std.PersistentHashMap.mkEmptyEntriesArray, size := 0 } },
          cache :=
            { inferType :=
                { root := Std.PersistentHashMap.Node.entries Std.PersistentHashMap.mkEmptyEntriesArray, size := 0 },
              funInfo :=
                { root := Std.PersistentHashMap.Node.entries Std.PersistentHashMap.mkEmptyEntriesArray, size := 0 },
              synthInstance :=
                { root := Std.PersistentHashMap.Node.entries Std.PersistentHashMap.mkEmptyEntriesArray, size := 0 },
              whnfDefault :=
                { root := Std.PersistentHashMap.Node.entries Std.PersistentHashMap.mkEmptyEntriesArray, size := 0 },
              whnfAll :=
                { root := Std.PersistentHashMap.Node.entries Std.PersistentHashMap.mkEmptyEntriesArray, size := 0 },
              defEqDefault :=
                { root := Std.PersistentHashMap.Node.entries Std.PersistentHashMap.mkEmptyEntriesArray, size := 0 },
              defEqAll :=
                { root := Std.PersistentHashMap.Node.entries Std.PersistentHashMap.mkEmptyEntriesArray, size := 0 } },
          zetaFVarIds := ∅,
          postponed :=
            { root := Std.PersistentArrayNode.node (Array.mkEmpty (USize.toNat Std.PersistentArray.branching)),
              tail := Array.mkEmpty (USize.toNat Std.PersistentArray.branching), size := 0,
              shift := Std.PersistentArray.initShift, tailOff := 0 } };
      let coreCtx :=
        { options := options, currRecDepth := 0, maxRecDepth := 1000, ref := Syntax.missing,
          currNamespace := Name.anonymous, openDecls := [], initHeartbeats := 0,
          maxHeartbeats := Core.getMaxHeartbeats options };
      let coreState :=
        { env := env, nextMacroScope := firstFrontendMacroScope + 1, ngen := { namePrefix := `_uniq, idx := 1 },
          traceState :=
            { enabled := true,
              traces :=
                { root := Std.PersistentArrayNode.node (Array.mkEmpty (USize.toNat Std.PersistentArray.branching)),
                  tail := Array.mkEmpty (USize.toNat Std.PersistentArray.branching), size := 0,
                  shift := Std.PersistentArray.initShift, tailOff := 0 } } };
      do
        let a ←
          StateRefT'.run
              (StateRefT'.run (init (?m.788 metaCtx metaState coreCtx coreState))
                (?m.789 metaCtx metaState coreCtx coreState) (?m.790 metaCtx metaState coreCtx coreState))
              (?m.791 metaCtx metaState coreCtx coreState)
        pure a.fst.fst))
    Task.Priority.default
has type
  BaseIO (Task (Except IO.Error (Except Exception α))) : Type
but is expected to have type
  m (Task (Except IO.Error (Except Exception α))) : Type

on latest lean4 HEAD?

[Julian Berman]

OK never mind, me being less lazy and compiling that version confirms it works fine there, ok.

[Scott Morrison]

Feel free to send a PR updating mathlib4 to new versions of Lean 4, whenever you do this!

[Julian Berman]

I was a few things deep on the yak stack but happy to do so otherwise in general, good to hear it's welcome.