How to install mathlib4

Stream: mathlib4

[Martin Gilchrist]

Hi - apologies for asking a very simple question. I have Visual Studio Code and lean4 installed on a Windows box. Now I want to create a new project so that I can use mathlib4 (specifically for some ring theory work). How do I do this? I have googled around, but cannot find easy-to-follow instructions. Thanks for any help, Martin

[Mac]

The README of Lake (Lean 4's package manager) may be of help to you: https://github.com/leanprover/lake/blob/v3.0.1/README.md (edit: changed link to stable v3.0.1 )

[Alexander Bentkamp]

I've also had some issues with setting up mathlib4. @Ramon Fernandez Mir came up with this setup that works for me:

lakefile.lean:

import Lake

open Lake DSL System

def rebuildDependency (depDir : FilePath) : OpaqueTarget :=
  (Target.opaqueSync : BuildM BuildTrace → _) $ do
    proc { cmd := "lake", args := #["build"], cwd := some <| depDir }
    pure BuildTrace.nil

package MyProject (pkgDir) {
  defaultFacet := PackageFacet.oleans
  dependencies := #[{
    name := "mathlib3port",
    src := Source.git
      "https://github.com/leanprover-community/mathlib3port.git"
      "20ff80c8529718040f00c68bf0a7d72cddc634a0",
  }]
  extraDepTarget := let depsDir := pkgDir / "lean_packages"
    Target.collectOpaqueList [
      rebuildDependency (depsDir / "lean3port"),
      rebuildDependency (depsDir / "mathlib"),
      rebuildDependency (depsDir / "mathlib3port")
    ]
}

lean-toolchain:

leanprover/lean4:nightly-2022-05-10

[Alexander Bentkamp]

However, if you just want to try out Lean, I'd recommend to use Lean 3. Or is there a specific reason you want to use Lean 4?

[Kevin Buzzard]

Ring theory in Lean 3: a ton of MSc level commutative algebra. Ring theory in Lean 4: the definition plus epsilon. So it very much depends on what this "ring theory work" is.

[Kevin Buzzard]

Of course, when the port happens then all the good stuff will be in Lean 4 too. But this hasn't happened yet.

[Alexander Bentkamp]

Oh, I assumed we are talking about mathbin, i.e., the port of the mathlib3 binaries into Lean4. That's what the setup above is for.

[Alexander Bentkamp]

If we're really talking about mathlib 4 only, then indeed there is no way to do anything serious related to ring theory.

[Alexander Bentkamp]

But even with mathbin it'll be hard because of the missing tactics and some other flaws of mathbin.

[Martin Gilchrist]

Hi, and thanks for the various suggestions above. I've tried two things, neither of which have worked, so I'll report them here in the hopes that someone can suggest how to make progress, and/or provide feedback!

Attempt 1. I created a project using lake. It's in a directory D:\temp\rings\rings. In the lower rings directory, I edited the lakefile.lean as suggested on https://github.com/leanprover/lake/blob/v3.0.1/README.md (I've attached this as firstlakefile.lean). When I open the rings project in VS Code, then the Output window displays the following:
Lean (version 4.0.0-nightly-2022-06-09, commit d0499ebf4d92, Release)
elan 1.4.1 (6a7f30d8e 2022-04-15)
[Error - 8:55:50 PM] Request textDocument/documentSymbol failed.
Message: Server process for file:///d%3A/temp/rings/rings/Rings.lean crashed, likely due to a stack overflow in user code.
Code: -32603
[Error - 8:55:50 PM] Request textDocument/foldingRange failed.
Message: Server process for file:///d%3A/temp/rings/rings/Rings.lean crashed, likely due to a stack overflow in user code.
Code: -32603
[Error - 8:55:50 PM] Request textDocument/semanticTokens/range failed.
Message: Server process for file:///d%3A/temp/rings/rings/Rings.lean crashed, likely due to a stack overflow in user code.
Code: -32603
[Error - 8:55:50 PM] Request textDocument/semanticTokens/full failed.
Message: Server process for file:///d%3A/temp/rings/rings/Rings.lean crashed, likely due to a stack overflow in user code.
Code: -32603

Attempt 2 involved editing the lakefile.lean along the lines suggested by Alexander Bentkamp (attached secondlakefile.lean) and restarting VS Code again. This gives pretty much the same output too.

So any suggestions appreciated, and I'd be happy to provide more information if need be. Thanks, Martin

secondlakefile.lean firstlakefile.lean

[Alexander Bentkamp]

Hm, I can't reproduce that. Does Lean4 work for you without mathlib? And what is in the file Rings.lean?

[Stuart Geipel]

Hey guys, I am trying to install mathlib4 as well and running into different issues. I followed the same lake REAMDE (on an Apple M1) and got a different result:

% lake build
info: mathlib: trying to update ./lean_packages/mathlib to revision master
./lean_packages/mathlib/./lakefile.lean:8:0: error: expected 'abbrev', 'axiom', 'class', 'constant', 'def', 'example', 'inductive', 'instance', 'structure' or 'theorem'
error: package configuration `./lean_packages/mathlib/./lakefile.lean` has errors

If I clone mathlib4 directly and then lake build, it appears to fully build without incident.

[Henrik Böving]

Lake recently did a breaking change in its configuration format so old lakes will not understand new lake formats. If you look into the lean-toolchain file of mathlib and your lake project you will most likely see that mathlib is using a much newer release than you are in your project that depends on mathlib

You should basically update your lean-toolchain version to that of mathlib and it will work @Stuart Geipel

[Stuart Geipel]

Okay, thank you, I will try that!

[Stuart Geipel]

It worked! My solution in case someone needs it:

1. elan update to update lean, lake to the latest nightly
2. Inside my project, do lake init <package name>, e.g. my package name is fractran
3. Set lakefile.lean to this:

import Lake
open Lake DSL

package fractran

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

@[defaultTarget]
lean_exe fractran {
  root := `Main
}

4. Add import Mathlib to your file of interest
5. Run lean build in the directory a couple times, let VS code spin a little bit/restart a couple times while it builds all of mathlib4 (not sure what exactly happens here)
6. It works

[Gabriel Ebner]

You should always set the correct Lean version in the lean-toolchain file. If you have mathlib4 as a dependency, you can just do cp lean_packages/mathlib/lean-toolchain . to get the right one.

[Andreas K.]

Stuart Geipel schrieb:

It worked! My solution in case someone needs it:

1. elan update to update lean, lake to the latest nightly
2. Inside my project, do lake init <package name>, e.g. my package name is fractran
3. Set lakefile.lean to this:

import Lake
open Lake DSL

package fractran

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

@[defaultTarget]
lean_exe fractran {
  root := `Main
}

4. Add import Mathlib to your file of interest
5. Run lean build in the directory a couple times, let VS code spin a little bit/restart a couple times while it builds all of mathlib4 (not sure what exactly happens here)
6. It works

Sorry did you mean lake build? lean build doesn't work for me.
Also, while the download worked with your code, I still get "unknown package 'mathlib'"

[Alex J. Best]

This thread is over a year old, please check out https://leanprover-community.github.io/install/project.html#working-on-an-existing-project instead

[Alex J. Best]

Or better yet https://leanprover-community.github.io/install/project.html#creating-a-lean-project it sounds like

[Patrick Massot]

@Marc Huisinga and @David Thrane Christiansen how far are we from getting rid of those installation pages on the community website? I see that https://lean-lang.org/lean4/doc/quickstart.html hasn't been updated.