Trouble Importing Mathlib

Stream: mathlib4

[Paul Wintz]

I'm trying to set up Mathlib but have been running into difficulties. In particular, for the file:

import Mathlib.Data.Real.Basic

#eval 1

I get the following error:

`c:\Users\pwintz\.elan\toolchains\leanprover--lean4---nightly\bin\lake.exe print-paths Init Mathlib.Data.Real.Basic Mathlib.Data.Complex.Exponential Mathlib.Algebra.Periodic` failed:

stderr:
info: Building Std.Linter.UnreachableTactic
info: Building Std.CodeAction.Basic
info: Building Std.Linter.UnnecessarySeqFocus
info: Building Std.Tactic.TryThis
info: Building Mathlib.Control.Basic
error: > LEAN_PATH=.\build\lib;.\lake-packages\mathlib\build\lib;.\lake-packages\Qq\build\lib;.\lake-packages\aesop\build\lib;.\lake-packages\std\build\lib PATH c:\Users\pwintz\.elan\toolchains\leanprover--lean4---nightly\bin\lean.exe -DwarningAsError=true -Dlinter.missingDocs=true .\lake-packages\std\.\.\Std\Linter\UnreachableTactic.lean -R .\lake-packages\std\.\. -o .\lake-packages\std\build\lib\Std\Linter\UnreachableTactic.olean -i .\lake-packages\std\build\lib\Std\Linter\UnreachableTactic.ilean -c .\lake-packages\std\build\ir\Std\Linter\UnreachableTactic.c
error: stdout:
.\lake-packages\std\.\.\Std\Linter\UnreachableTactic.lean:87:45: error: invalid {...} notation, expected type is not of the form (C ...)
  Linter
error: external command `c:\Users\pwintz\.elan\toolchains\leanprover--lean4---nightly\bin\lean.exe` exited with code 1
error: > LEAN_PATH=.\build\lib;.\lake-packages\mathlib\build\lib;.\lake-packages\Qq\build\lib;.\lake-packages\aesop\build\lib;.\lake-packages\std\build\lib PATH c:\Users\pwintz\.elan\toolchains\leanprover--lean4---nightly\bin\lean.exe -DwarningAsError=true -Dpp.unicode.fun=true .\lake-packages\mathlib\.\.\Mathlib\Control\Basic.lean -R .\lake-packages\mathlib\.\. -o .\lake-packages\mathlib\build\lib\Mathlib\Control\Basic.olean -i .\lake-packages\mathlib\build\lib\Mathlib\Control\Basic.ilean -c .\lake-packages\mathlib\build\ir\Mathlib\Control\Basic.c
error: stdout:
.\lake-packages\mathlib\.\.\Mathlib\Control\Basic.lean:272:6: error: expected '{' or strict indentation
.\lake-packages\mathlib\.\.\Mathlib\Control\Basic.lean:271:78: error: unsolved goals
α✝ β✝ γ✝ : Type u
m✝ : ?m.20171
m : Type u → Type v
h : Applicative m
inst✝ : CommApplicative m
α β γ : Type u
a : m α
b : m β
f : α → β → γ
⊢ (Seq.seq (f <$> a) fun x ↦ b) = (fun p ↦ f p.fst p.snd) <$> Seq.seq (Prod.mk <$> a) fun x ↦ b
error: external command `c:\Users\pwintz\.elan\toolchains\leanprover--lean4---nightly\bin\lean.exe` exited with code 1
error: > LEAN_PATH=.\build\lib;.\lake-packages\mathlib\build\lib;.\lake-packages\Qq\build\lib;.\lake-packages\aesop\build\lib;.\lake-packages\std\build\lib PATH c:\Users\pwintz\.elan\toolchains\leanprover--lean4---nightly\bin\lean.exe -DwarningAsError=true -Dlinter.missingDocs=true .\lake-packages\std\.\.\Std\Linter\UnnecessarySeqFocus.lean -R .\lake-packages\std\.\. -o .\lake-packages\std\build\lib\Std\Linter\UnnecessarySeqFocus.olean -i .\lake-packages\std\build\lib\Std\Linter\UnnecessarySeqFocus.ilean -c .\lake-packages\std\build\ir\Std\Linter\UnnecessarySeqFocus.c
error: stdout:
.\lake-packages\std\.\.\Std\Linter\UnnecessarySeqFocus.lean:63:6: error: unknown constant 'Parser.Tactic.Conv.«convNext__=>_»'
.\lake-packages\std\.\.\Std\Linter\UnnecessarySeqFocus.lean:151:47: error: invalid {...} notation, expected type is not of the form (C ...)
  Linter
error: external command `c:\Users\pwintz\.elan\toolchains\leanprover--lean4---nightly\bin\lean.exe` exited with code 1
error: > LEAN_PATH=.\build\lib;.\lake-packages\mathlib\build\lib;.\lake-packages\Qq\build\lib;.\lake-packages\aesop\build\lib;.\lake-packages\std\build\lib PATH c:\Users\pwintz\.elan\toolchains\leanprover--lean4---nightly\bin\lean.exe -DwarningAsError=true -Dlinter.missingDocs=true .\lake-packages\std\.\.\Std\Tactic\TryThis.lean -R .\lake-packages\std\.\. -o .\lake-packages\std\build\lib\Std\Tactic\TryThis.olean -i .\lake-packages\std\build\lib\Std\Tactic\TryThis.ilean -c .\lake-packages\std\build\ir\Std\Tactic\TryThis.c
error: stdout:
.\lake-packages\std\.\.\Std\Tactic\TryThis.lean:51:2: error: unknown attribute [code_action_provider]
error: external command `c:\Users\pwintz\.elan\toolchains\leanprover--lean4---nightly\bin\lean.exe` exited with code 1
error: > LEAN_PATH=.\build\lib;.\lake-packages\mathlib\build\lib;.\lake-packages\Qq\build\lib;.\lake-packages\aesop\build\lib;.\lake-packages\std\build\lib PATH c:\Users\pwintz\.elan\toolchains\leanprover--lean4---nightly\bin\lean.exe -DwarningAsError=true -Dlinter.missingDocs=true .\lake-packages\std\.\.\Std\CodeAction\Basic.lean -R .\lake-packages\std\.\. -o .\lake-packages\std\build\lib\Std\CodeAction\Basic.olean -i .\lake-packages\std\build\lib\Std\CodeAction\Basic.ilean -c .\lake-packages\std\build\ir\Std\CodeAction\Basic.c
error: stdout:
.\lake-packages\std\.\.\Std\CodeAction\Basic.lean:29:2: error: unknown attribute [code_action_provider]
.\lake-packages\std\.\.\Std\CodeAction\Basic.lean:166:2: error: unknown attribute [code_action_provider]
.\lake-packages\std\.\.\Std\CodeAction\Basic.lean:213:2: error: unknown attribute [code_action_provider]
error: external command `c:\Users\pwintz\.elan\toolchains\leanprover--lean4---nightly\bin\lean.exe` exited with code 1

My lakefile.lean is as follows:

 import Lake
open Lake DSL

package «learn-lean» {
  -- add any package configuration options here
}

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

@[default_target]
lean_lib «LearnLean» {
  -- add any library configuration options here
}

Any ideas for how to fix this?

[Paul Wintz]

Also, if this is not the right forum to get this type of help, please let me know. I'm new here :)

[Sebastian Ullrich]

@Paul Wintz Did you follow the steps at https://github.com/leanprover-community/mathlib4#using-mathlib4-as-a-dependency? It sounds like your lean-toolchain file does not match mathlib4's

[Paul Wintz]

@Sebastian Ullrich, I'm not sure if I followed thos steps the first time, so I've started over, to make sure. When I run elan run leanprover/lean4:nightly-2023-02-04 lake new lean-test math the output is

$ elan run leanprover/lean4:nightly-2023-02-04 lake new lean-test math
error: toolchain 'leanprover/lean4:nightly-2023-02-04' is not installed

Do I need to build mathlib4as described here before I run elan run leanprover/lean4:nightly-2023-02-04 lake new lean-test math?

[Moritz Doll]

probably elan toolchain install leanprover/lean4:nightly-2023-02-04 solves your problem. but what you really want to do is check whether the contents of lean-toolchain in your project match with the current version of mathlib4 (and run lake update to make sure you have the current version of mathlib4 in your project)

[Scott Morrison]

I think

lake +leanprover/lean4:nightly-2023-02-04 new lean-test math

is the right command. This seems to successfully install the relevant version of lean if it is not available (unlike elan run).

[Scott Morrison]

(That said, this is a very old toolchain, and definitely not the one in mathlib4's current lean-toolchain, which is what you should be using.)

[Sebastian Ullrich]

Oops yes, the elan run issue was noticed before, but we didn't adjust the readme. !4#4724

[Sebastian Ullrich]

Scott Morrison said:

(That said, this is a very old toolchain, and definitely not the one in mathlib4's current lean-toolchain, which is what you should be using.)

It's a fine toolchain for setting up the project. This is the most robust solution we have right now.

[David Sprayberry]

Sebastian Ullrich said:

Paul Wintz Did you follow the steps at https://github.com/leanprover-community/mathlib4#using-mathlib4-as-a-dependency? It sounds like your lean-toolchain file does not match mathlib4's

Does it have to be exactly the same?
My lean project's toolchain is "leanprover/lean4:v4.0.0-rc4"
whereas mathlib's is "leanprover/lean4:v4.0.0".
I tried elan toolchain install leanprover/lean4:v4.0.0 and it gave output
leanprover/lean4:v4.0.0 unchanged - Lean (version 4.0.0, commit ec941735c80d, Release)

[Sebastian Ullrich]

It does, please follow the steps as written