mathlib4 build error

Stream: new members

[Palalansoukî]

I tried to use mathlib4 in lean4 but I cannot use it with the following error. What should I do? When I run lake build I get a message including the following:

error: stdout:
./lake-packages/mathlib/././Mathlib/Algebra/Order/Monoid/NatCast.lean:55:19: error: failed to synthesize instance
  AddZeroClass ℕ
./lake-packages/mathlib/././Mathlib/Algebra/Order/Monoid/NatCast.lean:56:18: error: type mismatch
  add_le_add_left zero_le_one 1
has type
  1 + 0 ≤ @HAdd.hAdd ℕ ℕ ℕ (@instHAdd ℕ AddZeroClass.toAdd) 1 1 : Prop
but is expected to have type
  1 + 0 ≤ @HAdd.hAdd ℕ ℕ ℕ (@instHAdd ℕ instAddNat) 1 1 : Prop
./lake-packages/mathlib/././Mathlib/Algebra/Order/Monoid/NatCast.lean:56:34: error: failed to synthesize instance
  ZeroLEOneClass ℕ
./lake-packages/mathlib/././Mathlib/Algebra/Order/Monoid/NatCast.lean:56:18: error: failed to synthesize instance
  CovariantClass ℕ ℕ (fun x x_1 ↦ x + x_1) fun x x_1 ↦ x ≤ x_1
./lake-packages/mathlib/././Mathlib/Algebra/Order/Monoid/NatCast.lean:62:19: error: failed to synthesize instance
  AddZeroClass ℕ
./lake-packages/mathlib/././Mathlib/Algebra/Order/Monoid/NatCast.lean:63:18: error: type mismatch
  add_le_add_right zero_le_one 1
has type
  0 + 1 ≤ @HAdd.hAdd ℕ ℕ ℕ (@instHAdd ℕ AddZeroClass.toAdd) 1 1 : Prop
but is expected to have type
  0 + 1 ≤ @HAdd.hAdd ℕ ℕ ℕ (@instHAdd ℕ instAddNat) 1 1 : Prop
./lake-packages/mathlib/././Mathlib/Algebra/Order/Monoid/NatCast.lean:63:35: error: failed to synthesize instance
  ZeroLEOneClass ℕ
./lake-packages/mathlib/././Mathlib/Algebra/Order/Monoid/NatCast.lean:63:18: error: failed to synthesize instance
  CovariantClass ℕ ℕ (swap fun x x_1 ↦ x + x_1) fun x x_1 ↦ x ≤ x_1

Lean4 and mathlib4 are both the latest. (lean4: nightly-2023-02-04, mathlib4 revision: 25e6049. I tried several other revisions with the same result)

[Kevin Buzzard]

The latest mathlib4 doesn't use the latest lean4, that is probably your problem.

[Kevin Buzzard]

If you want to use mathlib, you should be on Lean version 4.0.0-nightly-2023-01-29, commit 38a0d1e3733e, Release, the version mathlib4 is using.

[Palalansoukî]

Thank you!

[Shreyas Srinivas]

Kevin Buzzard said:

The latest mathlib4 doesn't use the latest lean4, that is probably your problem.

This sounds like an issue for which there should be better solutions. Typically build tools (I have cabal and cargo in mind) have valid library ranges and vice versa. Incompatible versions throw errors.

[Eric Wieser]

Well, the version above did throw an error...

[Ruben Van de Velde]

Maybe a more explicit one

[Reid Barton]

I'm not actually sure how you would build mathlib4 with the wrong lean4 version without realizing it

[Reid Barton]

I guess maybe if you don't have elan installed?

[Shreyas Srinivas]

Akaho Akane said:

I tried to use mathlib4 in lean4 but I cannot use it with the following error. What should I do? When I run lake build I get a message including the following:

error: stdout:
./lake-packages/mathlib/././Mathlib/Algebra/Order/Monoid/NatCast.lean:55:19: error: failed to synthesize instance
  AddZeroClass ℕ
./lake-packages/mathlib/././Mathlib/Algebra/Order/Monoid/NatCast.lean:56:18: error: type mismatch
  add_le_add_left zero_le_one 1
has type
  1 + 0 ≤ @HAdd.hAdd ℕ ℕ ℕ (@instHAdd ℕ AddZeroClass.toAdd) 1 1 : Prop
but is expected to have type
  1 + 0 ≤ @HAdd.hAdd ℕ ℕ ℕ (@instHAdd ℕ instAddNat) 1 1 : Prop
./lake-packages/mathlib/././Mathlib/Algebra/Order/Monoid/NatCast.lean:56:34: error: failed to synthesize instance
  ZeroLEOneClass ℕ
./lake-packages/mathlib/././Mathlib/Algebra/Order/Monoid/NatCast.lean:56:18: error: failed to synthesize instance
  CovariantClass ℕ ℕ (fun x x_1 ↦ x + x_1) fun x x_1 ↦ x ≤ x_1
./lake-packages/mathlib/././Mathlib/Algebra/Order/Monoid/NatCast.lean:62:19: error: failed to synthesize instance
  AddZeroClass ℕ
./lake-packages/mathlib/././Mathlib/Algebra/Order/Monoid/NatCast.lean:63:18: error: type mismatch
  add_le_add_right zero_le_one 1
has type
  0 + 1 ≤ @HAdd.hAdd ℕ ℕ ℕ (@instHAdd ℕ AddZeroClass.toAdd) 1 1 : Prop
but is expected to have type
  0 + 1 ≤ @HAdd.hAdd ℕ ℕ ℕ (@instHAdd ℕ instAddNat) 1 1 : Prop
./lake-packages/mathlib/././Mathlib/Algebra/Order/Monoid/NatCast.lean:63:35: error: failed to synthesize instance
  ZeroLEOneClass ℕ
./lake-packages/mathlib/././Mathlib/Algebra/Order/Monoid/NatCast.lean:63:18: error: failed to synthesize instance
  CovariantClass ℕ ℕ (swap fun x x_1 ↦ x + x_1) fun x x_1 ↦ x ≤ x_1

Lean4 and mathlib4 are both the latest. (lean4: nightly-2023-02-04, mathlib4 revision: 25e6049. I tried several other revisions with the same result)

This error message does not immediately tell me I am using the wrong version of mathlib

[Shreyas Srinivas]

This version check sounds like a check that needs to happen before the compilation of these files even begins

[Reid Barton]

I don't agree. The package already knows what version of lean it is supposed to be compiled with, and elan will automatically use the correct version, even if the user doesn't have it installed yet.
Trying to use a different version of Lean--which might differ only in performance for instance--is not an error. This matters to package maintainers and, especially, those working on Lean itself.

[Reid Barton]

What we should try to prevent is users accidentally not using elan.

[Shreyas Srinivas]

Reid Barton said:

I don't agree. The package already knows what version of lean it is supposed to be compiled with, and elan will automatically use the correct version, even if the user doesn't have it installed yet.
Trying to use a different version of Lean--which might differ only in performance for instance--is not an error. This matters to package maintainers and, especially, those working on Lean itself.

I don't understand. Suppose I have a series of nightlies, say 1,2,3,4,5 and mathlib4 is currently on 3. Suppose I call lake new <project_name> math, are you saying lake will choose the correct toolchain? What happens if mathlib is manually added as a dependency in the lakefile with a require line

[Reid Barton]

I have no idea what lake will do in this situation, I'm just talking about building mathlib itself

[Shreyas Srinivas]

If this is purely about building mathlib, isn't lake build going to choose the toolchain in the lean-toolchain file, regardless of what elan is used to set as the default toolchain (outside the folder)?

[Reid Barton]

Well, you can use elan override to pick a different toolchain (for testing purposes say), but otherwise yes.