Zulip Chat Archive
Stream: general
Topic: Orange bar hell on fresh leanproject
Bolton Bailey (Jun 27 2022 at 16:07):
I'm seeing something a bit weird with a new leanproject I just made. Following the instructions under "Creating a Lean Project" it works fine. But if I change the topology.basic import to data.polynomial.basic, I get orange bar hell. Do I need to run something after leanproject new to get oleans for mathlib?
Kevin Buzzard (Jun 27 2022 at 16:09):
You shouldn't need to. What happens if you try lean --make src in the root directory of the project? And were there any errors when you ran leanproject new?
Bolton Bailey (Jun 27 2022 at 16:10):
No errors when I ran leanproject new. When I run lean --make src I start seeing it compile a bunch of mathlib files.
Alex J. Best (Jun 27 2022 at 16:12):
What about leanproject get-mathlib-cache? what is the output of that?
Kyle Miller (Jun 27 2022 at 16:13):
If you were unlucky and created your project in a recent 30-minute window, you got a version of mathlib that did not have complete oleans. Perhaps the simplest thing to try is to create a new project first, and then we can try more sophisticated debugging.
Bolton Bailey (Jun 27 2022 at 16:14):
Ok, I'll start from scratch again
Bolton Bailey (Jun 27 2022 at 16:16):
First thing that happens when I put import data.polynomial.basic in src/test.lean is "Could not resolve data.polynomia", which is weird itself, but restarting Lean makes that go away.
Bolton Bailey (Jun 27 2022 at 16:17):
Now I still get an orange bar on import data.polynomial.basic.
Bolton Bailey (Jun 27 2022 at 16:18):
Here's the leanproject new output
(base) 12:09:57 risc0-all-files #=# leanproject new lean-prototyping
> cd lean-prototyping
> git init -q
> git checkout -b lean-3.8.0
Switched to a new branch 'lean-3.8.0'
configuring lean-prototyping 0.1
Adding mathlib
mathlib: cloning https://github.com/leanprover-community/mathlib to _target/deps/mathlib
> git clone https://github.com/leanprover-community/mathlib _target/deps/mathlib
Cloning into '_target/deps/mathlib'...
remote: Enumerating objects: 307734, done.
remote: Counting objects: 100% (402/402), done.
remote: Compressing objects: 100% (276/276), done.
remote: Total 307734 (delta 206), reused 271 (delta 126), pack-reused 307332
Receiving objects: 100% (307734/307734), 161.86 MiB | 35.60 MiB/s, done.
Resolving deltas: 100% (246274/246274), done.
> git checkout --detach 8c836ac9dfa53d6acac4f2a693f2c718f013fe51 # in directory _target/deps/mathlib
HEAD is now at 8c836ac9df Merge branch 'master' of https://github.com/leanprover-community/mathlib
configuring lean-prototyping 0.1
mathlib: trying to update _target/deps/mathlib to revision 8c836ac9dfa53d6acac4f2a693f2c718f013fe51
> git checkout --detach 8c836ac9dfa53d6acac4f2a693f2c718f013fe51 # in directory _target/deps/mathlib
HEAD is now at 8c836ac9df Merge branch 'master' of https://github.com/leanprover-community/mathlib
Looking for lean-prototyping oleans for 8c836ac9df
locally...
Found local lean-prototyping oleans
Located matching cache
Applying cache
files extracted: 2498 [00:13, 187.86/s]
Bolton Bailey (Jun 27 2022 at 16:20):
Still an orange bar after 2 minutes. Trying leanproject get-mathilb-cache ...
Bolton Bailey (Jun 27 2022 at 16:21):
It finds the local cache, but still orange bars the import.
Julian Berman (Jun 27 2022 at 16:21):
Your Lean (or the one leanproject is choosing for you) is incredibly old -- 3.8.0. I'm pretty sure we've seen this before and making sure you're on some recent version of mathlibtools was the fix.
Julian Berman (Jun 27 2022 at 16:22):
What's leanproject --version?
Bolton Bailey (Jun 27 2022 at 16:22):
(base) 12:22:06 lean-prototyping #=# leanproject --version
leanproject, version 1.1.0
Kevin Buzzard (Jun 27 2022 at 16:22):
Julian Berman said:
Your Lean (or the one leanproject is choosing for you) is incredibly old --
3.8.0. I'm pretty sure we've seen this before and making sure you're on some recent version of mathlibtools was the fix.
I'm not sure that this is the correct diagnosis. IIRC leanproject prints out junk like this sometimes even when you're doing things right, and you don't end up on 3.8.0.
Kyle Miller (Jun 27 2022 at 16:23):
What does elan show say?
Bolton Bailey (Jun 27 2022 at 16:23):
(base) 12:22:12 lean-prototyping #=# elan show
installed toolchains
--------------------
stable (default)
leanprover-community-lean-3.20.0
leanprover-community-lean-3.21.0
leanprover-community-lean-3.23.0
leanprover-community-lean-3.26.0
leanprover-community-lean-3.27.0
leanprover-community-lean-3.28.0
leanprover-community-lean-3.30.0
leanprover-community-lean-3.31.0
leanprover-community-lean-3.32.1
leanprover-community-lean-3.33.0
leanprover-community-lean-3.34.0
leanprover-community-lean-3.35.0
leanprover-community-lean-3.35.1
leanprover-community-lean-3.8.0
leanprover-community/lean:3.30.0
leanprover-community/lean:3.35.1
leanprover-community/lean:3.37.0
leanprover-community/lean:3.38.0
leanprover-community/lean:3.39.0
leanprover-community/lean:3.39.1
leanprover-community/lean:3.39.2
leanprover-community/lean:3.40.0
leanprover-community/lean:3.41.0
leanprover-community/lean:3.42.0
leanprover-community/lean:3.42.1
leanprover-community/lean:3.43.0
active toolchain
----------------
leanprover-community/lean:3.43.0 (overridden by '/Users/boltonbailey/Desktop/risc0-all-files/lean-prototyping/leanpkg.toml')
Lean (version 3.43.0, commit bfce34363b0e, Release)
Kevin Buzzard (Jun 27 2022 at 16:24):
The "could not resolve data.polynomia" is also normal when you don't have the right oleans; it's the last error before the orange bars kick in and Lean doesn't clear the old error before it starts attempting to import data.polynomial.
Kevin Buzzard (Jun 27 2022 at 16:24):
I think the 3.8.0 thing is a red herring. What happens with leanproject get-mathlib-cache?
Bolton Bailey (Jun 27 2022 at 16:25):
I ran that before. It finds the local oleans, and when I restart, I still get orange bars.
Kevin Buzzard (Jun 27 2022 at 16:26):
$ leanproject new fishcake
> cd fishcake
> git init -q
> git checkout -b lean-3.41.0
Switched to a new branch 'lean-3.41.0'
configuring fishcake 0.1
Adding mathlib
...
Applying cache
files extracted: 2498 [00:04, 604.98/s]
$ cd fishcake/
/fishcake$ lean --version
Lean (version 3.43.0, commit bfce34363b0e, Release)
Note 3.41 v 3.43 and my set-up is fine.
Julian Berman (Jun 27 2022 at 16:26):
What's in /Users/boltonbailey/Desktop/risc0-all-files/lean-prototyping/leanpkg.toml
Julian Berman (Jun 27 2022 at 16:27):
I'm trying to find that old thread but IIRC another symptom was leanproject putting the old version in there too
Bolton Bailey (Jun 27 2022 at 16:27):
[package]
name = "lean-prototyping"
version = "0.1"
lean_version = "leanprover-community/lean:3.43.0"
path = "src"
[dependencies]
mathlib = {git = "https://github.com/leanprover-community/mathlib", rev = "8c836ac9dfa53d6acac4f2a693f2c718f013fe51"}
Julian Berman (Jun 27 2022 at 16:27):
OK then yeah I'm wrong but I also don't see that revision of mathlib... Ah never mind I do too, and it indeed wants 3.43.0. Hrm.
Kyle Miller (Jun 27 2022 at 16:30):
You shouldn't have revision 8c836ac9dfa53d6acac4f2a693f2c718f013fe51 -- this one was reverted
Julian Berman (Jun 27 2022 at 16:31):
Two other ideas until/unless someone has brighter ones is to either rm the olean cache for that commit, maybe it was partially corrupted and you're running into an issue reported elsewhere where the partial cache is still being reused, or otherwise a last resort is to open one of the olean files and see what it says at the start (it should say the version amongst some gibberish) just in case.
Julian Berman (Jun 27 2022 at 16:32):
Kyle Miller said:
You shouldn't have revision
8c836ac9dfa53d6acac4f2a693f2c718f013fe51-- this one was reverted
I see it no?
~/Development/mathlib is a git repository on master
⊙ g show 8c836ac9dfa53d6acac4f2a693f2c718f013fe51 julian@Airm
commit 8c836ac9dfa53d6acac4f2a693f2c718f013fe51 (origin/zmod.lift_injective_iff, origin/lean-3.43.0)
Merge: 8535ba9ea5 331df5a23a
Author: Heather Macbeth <25316162+hrmacbeth@users.noreply.github.com>
Date: Mon Jun 27 11:05:55 2022 -0400
Merge branch 'master' of https://github.com/leanprover-community/mathlib
It looks like it's https://github.com/leanprover-community/mathlib/commit/8c836ac9dfa53d6acac4f2a693f2c718f013fe51 -- or are you saying Bolton shouldn't be using it anyhow?
Kyle Miller (Jun 27 2022 at 16:32):
Try doing leanproject upgrade-mathlib and make sure that the rev becomes 05565f4d64c988f5ad3bc97eae5413229c34d01d
Kyle Miller (Jun 27 2022 at 16:33):
@Julian Berman Yes, I'm saying that commit should not be used. It's not in the master history anymore.
Bolton Bailey (Jun 27 2022 at 16:33):
(base) 12:33:09 lean-prototyping $ leanproject upgrade-mathl
ib
mathlib: trying to update _target/deps/mathlib to revision 8c836ac9dfa53d6acac4f2a693f2c718f013fe51
> git checkout --detach 8c836ac9dfa53d6acac4f2a693f2c718f013fe51 # in directory _target/deps/mathlib
HEAD is now at 8c836ac9df Merge branch 'master' of https://github.com/leanprover-community/mathlib
remote: Enumerating objects: 71, done.
remote: Counting objects: 100% (71/71), done.
remote: Compressing objects: 100% (33/33), done.
remote: Total 71 (delta 44), reused 56 (delta 38), pack-reused 0
Unpacking objects: 100% (71/71), 54.71 KiB | 636.00 KiB/s, done.
From https://github.com/leanprover-community/mathlib
7191e89632..57e7b8004e RD_condexp_mono -> origin/RD_condexp_mono
ccb29fa8bc..1e61bac1f1 RD_lp_order -> origin/RD_lp_order
ce83742c3a..400492c049 apurva/convex_cone_zero -> origin/apurva/convex_cone_zero
f4ee9f84db..ba43919145 jsm28/two_smul_angle_lemmas -> origin/jsm28/two_smul_angle_lemmas
* [new branch] limit_cardinal_refactor -> origin/limit_cardinal_refactor
331df5a23a..05565f4d64 master -> origin/master
05565f4d64..68e0160128 staging -> origin/staging
configuring lean-prototyping 0.1
mathlib: trying to update _target/deps/mathlib to revision 8c836ac9dfa53d6acac4f2a693f2c718f013fe51
> git checkout --detach 8c836ac9dfa53d6acac4f2a693f2c718f013fe51 # in directory _target/deps/mathlib
HEAD is now at 8c836ac9df Merge branch 'master' of https://github.com/leanprover-community/mathlib
Looking for lean-prototyping oleans for 8c836ac9df
locally...
Found local lean-prototyping oleans
Located matching cache
Applying cache
files extracted: 2498 [00:13, 179.07/s]
Kyle Miller (Jun 27 2022 at 16:35):
Also, apologies in advance if leanproject upgrade-mathlib doesn't work -- I don't know what it does in this situation.
Kyle Miller (Jun 27 2022 at 16:35):
Are you working in the freshly created project, or the one you started with at the beginning of the thread?
Bolton Bailey (Jun 27 2022 at 16:36):
Freshly created after you told me to do so.
Kevin Buzzard (Jun 27 2022 at 16:36):
Were the bad commits removed before or after? :-)
Kyle Miller (Jun 27 2022 at 16:36):
Before, I'm fairly sure.
Kyle Miller (Jun 27 2022 at 16:37):
It's very puzzling that you'd be on 8c836ac9dfa53d6acac4f2a693f2c718f013fe51 still, so maybe we turn if off and turn it on again for good measure... (i.e., create a fresh project)
Bolton Bailey (Jun 27 2022 at 16:39):
(base) 12:30:17 risc0-all-files #=# leanproject new yet-another-fresh-start
> cd yet-another-fresh-start
> git init -q
> git checkout -b lean-3.8.0
Switched to a new branch 'lean-3.8.0'
configuring yet-another-fresh-start 0.1
Adding mathlib
mathlib: cloning https://github.com/leanprover-community/mathlib to _target/deps/mathlib
> git clone https://github.com/leanprover-community/mathlib _target/deps/mathlib
Cloning into '_target/deps/mathlib'...
remote: Enumerating objects: 306972, done.
remote: Counting objects: 100% (660/660), done.
remote: Compressing objects: 100% (335/335), done.
remote: Total 306972 (delta 420), reused 522 (delta 325), pack-reused 306312
Receiving objects: 100% (306972/306972), 161.70 MiB | 14.33 MiB/s, done.
Resolving deltas: 100% (245617/245617), done.
> git checkout --detach 8c836ac9dfa53d6acac4f2a693f2c718f013fe51 # in directory _target/deps/mathlib
HEAD is now at 8c836ac9df Merge branch 'master' of https://github.com/leanprover-community/mathlib
configuring yet-another-fresh-start 0.1
mathlib: trying to update _target/deps/mathlib to revision 8c836ac9dfa53d6acac4f2a693f2c718f013fe51
> git checkout --detach 8c836ac9dfa53d6acac4f2a693f2c718f013fe51 # in directory _target/deps/mathlib
HEAD is now at 8c836ac9df Merge branch 'master' of https://github.com/leanprover-community/mathlib
Looking for yet-another-fresh-start oleans for 8c836ac9df
locally...
Found local yet-another-fresh-start oleans
Located matching cache
Applying cache
files extracted: 2498 [00:15, 165.14/s]
(base) 12:38:56 risc0-all-files #=#
Bolton Bailey (Jun 27 2022 at 16:39):
Still 8c836ac9dfa53d6acac4f2a693f2c718f013fe51
Kyle Miller (Jun 27 2022 at 16:42):
Hmm, I'm getting that too
Kevin Buzzard (Jun 27 2022 at 16:43):
Yes, I can also reproduce (together with orange bar hell). So right now leanproject new is broken.
Kyle Miller (Jun 27 2022 at 17:01):
I've reproduced it without leanproject.
$ mkdir foo
$ cd foo
$ leanpkg init foo
# now edit the leanpkg.toml file to use lean_version = "leanprover-community/lean:3.43.0"
$ leanpkg configure
$ leanpkg add leanprover-community/mathlib
Then if you look at the leanpkg.toml it has rev = "8c836ac9dfa53d6acac4f2a693f2c718f013fe51".
If I leave it at lean:3.42.1 (the default for me), then it has rev = "c81c6c91781f12ac7005367a4477dcb2f6be638f", which is a commit from 12 days ago. I guess leanpkg knows what version of mathlib to use for each version of lean somehow?
Reid Barton (Jun 27 2022 at 17:05):
It's because the lean-3.43.0 branch is still on that commit
Kevin Buzzard (Jun 27 2022 at 17:06):
gaargh I thought it would be something like that but I checked tags not branches.
Last updated: Dec 20 2023 at 11:08 UTC