require math lib from git

Stream: lean4

[Dean Young]

Does anyone know how to tweak this so that I don't get "unknown identifier 'ℝ'"

import Lake
open Lake DSL
require mathlib from git
  "https://github.com/leanprover-community/mathlib4.git"

#check ℝ

[Reid Barton]

Do you really want to use mathlib in the lakefile? Or just in your project?

[Dean Young]

here is my lakefile:

import Lake
open Lake DSL

package CategoryTheory

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

package introduction {
  -- add package configuration options here
}


lean_lib Introduction {
  -- add library configuration options here
}

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

No I just want it in the project... but somehow I still get unknown identifier ℝ.

[Reid Barton]

You need to import something.

[Dean Young]

What's the necessary import for ℝ? Any time I import Mathlib I get a bunch of errors "Main.lean:3:0: error: unknown package 'Mathlib'".

[Dean Young]

I thought this "require math lib from git" would fix it but it didn't.

[Martin Dvořák]

import Mathlib.Data.Real.Basic

[Martin Dvořák]

This is the import you need to write in the file that uses ℝ not in the lakefile itself.

[Dean Young]

The file no longer compiles after I include the import import Mathlib.Data.Real.Basic . I get tons of error messages like this one:

error: unknown constant 'sorryAx'

Main.lean:275:103: error: expected token

and this is the first error:

Main.lean:2:0: error: unknown package 'Mathlib'

I've been having this trouble for months and can't use Mathlib.

[Dean Young]

I also tried this:

cd; cd /Users/elliotyoung/Documents/CategoryTheory/CategoryTheory;  lake build +Mathlib.Data.Real.Basic CategoryTheory

[Dean Young]

and got this:

error: ./lakefile.lean:17:2: error: unknown attribute [defaultTarget]
error: ./lakefile.lean: package configuration has errors

[Eric Wieser]

What does lake --version give?

[Dean Young]

Lake version 4.0.0 (Lean version 4.0.0, commit 7dbfaf9b751917a7fe020485bf57f41fdddcaafa)

[Kyle Miller]

Is it supposed to be defaultTarget or default_target?

[Kyle Miller]

https://github.com/leanprover/lake suggests the second

[Dean Young]

changing it gives this:

error: ./lakefile.lean:12:2: error: unknown attribute [default_target]
error: ./lakefile.lean: package configuration has errors

[Dean Young]

I did change the default target but it gives me

error: ./lakefile.lean:15:2: error: unknown attribute [default_target]
error: ./lakefile.lean: package configuration has errors

[Dean Young]

so maybe it still doesn't see the default_target in the lake file, which is now this:

import Lake
open Lake DSL

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

package categories {
  -- add package configuration options here
}

lean_lib Categories {
  -- add library configuration options here
}

@[default_target]
lean_exe categories {
  root := `Main
}

[Kyle Miller]

Oh, wait, your lake is pretty old. This is mine:

Lake version 4.1.0-pre (Lean version 4.0.0-nightly-2023-04-11)

[Dean Young]

how do you update again?

[Dean Young]

it won't self update on my Mac I think...

[Eric Wieser]

Yeah, that commit, https://github.com/leanprover/lean4/commit/7dbfaf9b751917a7fe020485bf57f41fdddcaafa, is from August

[Eric Wieser]

I would recommend you just uninstall everything related to Lean4 and start over, those old versions are likely only going to make things more confusing

[Eric Wieser]

Kind Bubble said:

I've been having this trouble for months and can't use Mathlib.

You would likely have ended up with a resolution much sooner if you kept the discussion to a single thread rather than creating lots of separate ones about what is ultimately the same problem

[Dean Young]

Well, I did reinstall everything but I still have been getting these sorts of error: unknown constant 'sorryAx'. Is there a more manual way to import math lib?

[Dean Young]

error: dependency mathlib of whiteheadTheorem not in manifest, use `lake update` to update```

[Dean Young]

updating lake gives error: ./lake-packages/mathlib/lakefile.lean:29:2: error: 'weakLeanArgs' is not a field of structure 'Lake.LeanLibConfig' error: ./lake-packages/mathlib/lakefile.lean:52:2: error: 'weakLeanArgs' is not a field of structure 'Lake.LeanLibConfig' error: ./lake-packages/mathlib/lakefile.lean: package configuration has errors

[Kevin Buzzard]

If nothing works then why not just delete mathlib and reinstall?

[Dean Young]

Lake version 4.1.0-pre (Lean version 4.0.0-nightly-2023-06-01)... I'm going to try that.

[Dean Young]

Here's a clue:

leanproject new f

gives

error: toolchain 'leanprover/lean4:nightly' does not have the binary `/Users/elliotyoung/.elan/toolchains/leanprover--lean4---nightly/bin/leanpkg`
Command '['leanpkg', 'new', 'f']' returned non-zero exit status 1.

[Eric Wieser]

Why are you using leanproject? What instructions did you read that told you to use it?

[Adam Topaz]

leanproject is a tool for lean3.

[Ruben Van de Velde]

I wonder if we can make it error if you try to use it with lean 4

[Dean Young]

Ok I got it to work, and those bicategories I'm excited about too.

[Eric Wieser]

Ruben Van de Velde said:

I wonder if we can make it error if you try to use it with lean 4

Wish granted

[Ruben Van de Velde]

While you're granting wishes, error with a comprehensible message?