Starting a project with Mathlib4 dependency fails...

Stream: mathlib4

[Arien Malec]

I'm trying to create an #mwe project, and went through the following process:

arienmalec@Ariens-MBP-2 lean % lake new mwe
arienmalec@Ariens-MBP-2 lean % cd mwe
arienmalec@Ariens-MBP-2 mwe % cat lakefile.lean
import Lake
open Lake DSL

package «mwe» {
  -- add package configuration options here
}

lean_lib «Mwe» {
  -- add library configuration options here
}

@[default_target]
lean_exe «mwe» {
  root := `Main
}

require mathlib from git "https://github.com/leanprover-community/mathlib4" @ "master"
arienmalec@Ariens-MBP-2 mwe % lake update
-- Cut but all good
arienmalec@Ariens-MBP-2 mwe % lake build
Building Mwe
Compiling Mwe
Building Main
Compiling Main
Linking mwe
arienmalec@Ariens-MBP-2 mwe % lake exe cache get
-- cut but all good
arienmalec@Ariens-MBP-2 mwe % cat Mwe.lean
import Mathlib.Data.Sum.Basic

def hello := "world"%
arienmalec@Ariens-MBP-2 mwe % lake build
-- ...
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 DYLD_LIBRARY_PATH=/Users/arienmalec/.elan/toolchains/leanprover--lean4---nightly-2022-12-03/lib:././lake-packages/mathlib/build/lib /Users/arienmalec/.elan/toolchains/leanprover--lean4---nightly-2022-12-03/bin/lean -DwarningAsError=true ././lake-packages/mathlib/././Mathlib/Data/KVMap.lean -R ././lake-packages/mathlib/./. -o ././lake-packages/mathlib/build/lib/Mathlib/Data/KVMap.olean -i ././lake-packages/mathlib/build/lib/Mathlib/Data/KVMap.ilean -c ././lake-packages/mathlib/build/ir/Mathlib/Data/KVMap.c
error: stdout:
././lake-packages/mathlib/././Mathlib/Data/KVMap.lean:17:31: error: expected token
error: external command `/Users/arienmalec/.elan/toolchains/leanprover--lean4---nightly-2022-12-03/bin/lean` 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 DYLD_LIBRARY_PATH=/Users/arienmalec/.elan/toolchains/leanprover--lean4---nightly-2022-12-03/lib:././lake-packages/mathlib/build/lib /Users/arienmalec/.elan/toolchains/leanprover--lean4---nightly-2022-12-03/bin/lean -DwarningAsError=true ././lake-packages/mathlib/././Mathlib/Tactic/Relation/Rfl.lean -R ././lake-packages/mathlib/./. -o ././lake-packages/mathlib/build/lib/Mathlib/Tactic/Relation/Rfl.olean -i ././lake-packages/mathlib/build/lib/Mathlib/Tactic/Relation/Rfl.ilean -c ././lake-packages/mathlib/build/ir/Mathlib/Tactic/Relation/Rfl.c
error: stdout:
././lake-packages/mathlib/././Mathlib/Tactic/Relation/Rfl.lean:23:31: error: expected token
././lake-packages/mathlib/././Mathlib/Tactic/Relation/Rfl.lean:30:25: error: expected token
error: external command `/Users/arienmalec/.elan/toolchains/leanprover--lean4---nightly-2022-12-03/bin/lean` 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 DYLD_LIBRARY_PATH=/Users/arienmalec/.elan/toolchains/leanprover--lean4---nightly-2022-12-03/lib:././lake-packages/mathlib/build/lib /Users/arienmalec/.elan/toolchains/leanprover--lean4---nightly-2022-12-03/bin/lean -DwarningAsError=true ././lake-packages/mathlib/././Mathlib/Lean/Meta.lean -R ././lake-packages/mathlib/./. -o ././lake-packages/mathlib/build/lib/Mathlib/Lean/Meta.olean -i ././lake-packages/mathlib/build/lib/Mathlib/Lean/Meta.ilean -c ././lake-packages/mathlib/build/ir/Mathlib/Lean/Meta.c
error: stdout:
././lake-packages/mathlib/././Mathlib/Lean/Meta.lean:36:21: error: expected token
error: external command `/Users/arienmalec/.elan/toolchains/leanprover--lean4---nightly-2022-12-03/bin/lean` 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 DYLD_LIBRARY_PATH=/Users/arienmalec/.elan/toolchains/leanprover--lean4---nightly-2022-12-03/lib:././lake-packages/mathlib/build/lib /Users/arienmalec/.elan/toolchains/leanprover--lean4---nightly-2022-12-03/bin/lean -DwarningAsError=true ././lake-packages/mathlib/././Mathlib/Tactic/LeftRight.lean -R ././lake-packages/mathlib/./. -o ././lake-packages/mathlib/build/lib/Mathlib/Tactic/LeftRight.olean -i ././lake-packages/mathlib/build/lib/Mathlib/Tactic/LeftRight.ilean -c ././lake-packages/mathlib/build/ir/Mathlib/Tactic/LeftRight.c
error: stdout:
././lake-packages/mathlib/././Mathlib/Tactic/LeftRight.lean:15:13: error: expected token
-- lots more like this...
---

My elan is up to date, yadda yadda.

[Kevin Buzzard]

Did lake new mwe give you a lakefile with a mathlib dependency? It doesn't do that for me (I was trying to repro). Or did I misunderstand?

[Arien Malec]

I inserted the dependency

[Arien Malec]

Sorry- deleted the editing steps

[Siddhartha Gadgil]

Do the lean-toolchains match?

[Arien Malec]

Match what, I guess? lake is using the toolchain specified in lean-toolchain

[Arien Malec]

Which is a day behind the toolchain for Mathlib4?

[Gabriel Ebner]

A day behind is a day too much. :smile: Just copy the lean-toolchain file from mathlib.

[Gabriel Ebner]

cp lake-packages/mathlib/lean-toolchain .

[Arien Malec]

If I update the toolchain, I still get errors... How is lake supposed to work with mathlib4? My experience in lean 3 is that leanproject JustWorks...

[Kevin Buzzard]

Leanproject was specifically designed to work with mathlib. Lake was not specifically designed to work with mathlib4

[Arien Malec]

And I suspect at some point that's going to be an issue, but discovering in another thread that making mathlib4 work as a client isn't a priority at the moment. As noted I was trying to create an Mwe scratchpad so I can isolate issues, etc.

[Arthur Paulino]

Arien Malec said:

And I suspect at some point that's going to be an issue, but discovering in another thread that making mathlib4 work as a client isn't a priority at the moment. As noted I was trying to create an Mwe scratchpad so I can isolate issues, etc.

Hmm, not exactly. Making lake exe cache work on projects that import Mathlib isn't a priority. But using Mathlib, or any other Lake project, as a dependency shouldn't be an issue (as long as there isn't any version mismatch)

[Arthur Paulino]

@Arien Malec this is how you make your Lake project depend on Mathlib:
https://github.com/siddhartha-gadgil/LeanAide/blob/b6fb470c3997ea1ac1669969383691a976fc8b5d/lakefile.lean#L71-L72. You need to be careful to use a mathlib rev that matches your lean-toolchain

[Arien Malec]

Let me do this again ground up and see how far I can get.

[Arien Malec]

Fascinating -- same issues.

arienmalec@Ariens-MBP-2 lean % rm -rf mwe
arienmalec@Ariens-MBP-2 lean % lake new mwe
arienmalec@Ariens-MBP-2 lean % code mwe
arienmalec@Ariens-MBP-2 lean % cd mwe
arienmalec@Ariens-MBP-2 mwe % cat lean-toolchain
leanprover/lean4:nightly-2023-01-04
arienmalec@Ariens-MBP-2 mwe % cat lakefile.lean
import Lake
open Lake DSL

package «mwe» {
  -- add package configuration options here
}

lean_lib «Mwe» {
  -- add library configuration options here
}

@[default_target]
lean_exe «mwe» {
  root := `Main
}

require mathlib from git
  "https://github.com/leanprover-community/mathlib4.git"@"a4f3950661f788086a461619be71ebf68636d7ac"%                                                            arienmalec@Ariens-MBP-2 mwe % lake update
cloning https://github.com/leanprover-community/mathlib4.git to ./lake-packages/mathlib
cloning https://github.com/xubaiw/CMark.lean to ././lake-packages/CMark
cloning https://github.com/leanprover/lake to ././lake-packages/lake
cloning https://github.com/leanprover/doc-gen4 to ././lake-packages/doc-gen4
cloning https://github.com/mhuisi/lean4-cli to ././lake-packages/Cli
cloning https://github.com/gebner/quote4 to ././lake-packages/Qq
cloning https://github.com/JLimperg/aesop to ././lake-packages/aesop
cloning https://github.com/hargonix/LeanInk to ././lake-packages/leanInk
cloning https://github.com/xubaiw/Unicode.lean to ././lake-packages/Unicode
cloning https://github.com/leanprover/std4 to ././lake-packages/std
arienmalec@Ariens-MBP-2 mwe % lake exe cache get
info: Building Cache.IO
info: Building Cache.Hashing
info: Compiling Cache.IO
info: Compiling Cache.Hashing
info: Building Cache.Requests
info: Compiling Cache.Requests
info: Building Cache.Main
info: Compiling Cache.Main
info: Linking cache
Attempting to download 804 file(s)
Decompressing 803 file(s)
arienmalec@Ariens-MBP-2 mwe % cat Mwe.lean
import Mathlib.Data.Sum.Basic
arienmalec@Ariens-MBP-2 mwe % lake build
# <deleted lines>
Compiling Mathlib.Data.Sum.Basic
Building Mwe
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 DYLD_LIBRARY_PATH=/Users/arienmalec/.elan/toolchains/leanprover--lean4---nightly-2023-01-04/lib:./build/lib /Users/arienmalec/.elan/toolchains/leanprover--lean4---nightly-2023-01-04/bin/lean ./././Mwe.lean -R ././. -o ./build/lib/Mwe.olean -i ./build/lib/Mwe.ilean -c ./build/ir/Mwe.c
error: stdout:
./././Mwe.lean:1:0: error: object file './build/lib/Mathlib/Data/Sum/Basic.olean' of module Mathlib.Data.Sum.Basic does not exist
error: external command `/Users/arienmalec/.elan/toolchains/leanprover--lean4---nightly-2023-01-04/bin/lean` exited with code 1

[Arien Malec]

It has no problem building -- the issue seems to be in linking?

[Arthur Paulino]

I'm about to go AFK, but try to host that project on github so other people can clone it and help you. Also, the stream #lean4 is a better place to solve these general Lean 4/Lake issues

[Arien Malec]

It fails only with lake exe cache get -- will post the repo to GH.

[Arien Malec]

https://github.com/arienmalec/mwe

[Kevin Buzzard]

To make a mwe scratchpad I just use a scratch directory in mathlib4 BTW. I edit some file in .git (info/exclude maybe?) to make it not show up in VS Code git integration.

[Siddhartha Gadgil]

Arien Malec said:

It fails only with lake exe cache get -- will post the repo to GH.

I too have a repository which fails with lake exe cache get and so does @Raghuram (he mentioned this to me). For repos depending on mathlib4 lake exe cache get is not yet reliable.

[Jineon Baek]

Yet another report that lake exe cache get didn't work. Toolchain was leanprover/lean4:nightly-2023-04-20

[Marcin Tomaszewski]

i have mathlib4 in D:\mathlib4 downloaded and compiled, now i created D:\lean4mathlib4 and used command: lake new lean4mathlib4 math
how can I attach D:\mathlib4 to the lakefile instead of github?
lakefile is:
import Lake
...
require mathlib from git
"https://github.com/leanprover-community/mathlib4.git"

[Shreyas Srinivas]

Jineon Baek said:

Yet another report that lake exe cache get didn't work. Toolchain was leanprover/lean4:nightly-2023-04-20

Did you follow these steps: https://github.com/leanprover-community/mathlib4#using-mathlib4-as-a-dependency
?

[Shreyas Srinivas]

Step 2 is important

[Shreyas Srinivas]

I have never had to do step 6. I don't know why it was added. I didn't write it originally.

[Shreyas Srinivas]

It happens automatically

[Shreyas Srinivas]

Jineon Baek said:

Yet another report that lake exe cache get didn't work. Toolchain was leanprover/lean4:nightly-2023-04-20

Also, do the lake exe cache get! step before opening the project in vscode. Because opening an unbuilt project starts a build of mathlib4 whose oleans conflict with the cache downloaded oleans

[Jon Eugster]

Shreyas Srinivas said:

I have never had to do step 6. I don't know why it was added. I didn't write it originally.

I think step 6 (check that lean-toolchains agree) is important when calling lake update on an existing project, whereas lake new xy math does this automatically correctly.