Topic: leanproject debugging
Kevin Buzzard (Aug 10 2020 at 14:03):
I think I use
leanproject in a very different way to Patrick and I've always found it difficult to explain to him the problems I'm having. I use leanproject to manage multi-user projects with mathlib as a dependency, and when someone in my team bumps mathlib there can be problems for the other people. @Patrick Massot you will probably tell me that if I see this error when I am using leanproject then I've done something wrong:
/home/buzzard/lean-projects/group-theory-game/_target/deps/mathlib/src/algebra/field.lean:1:0: error: ambiguous import, it can be '/home/buzzard/lean-projects/group-theory-game/_target/deps/mathlib/src/algebra/ring/default.lean' or '/home/buzzard/lean-projects/group-theory-game/_target/deps/mathlib/src/algebra/ring.lean'
But I claim that I have done nothing wrong. What has happened here is that there has been a bump of mathlib recently which seems to have deleted
ring.lean and replaced it with
default.lean trick is to ensure that code doesn't break when mathlib is updated. But it breaks for me anyway because someone else changed the toml, so my understanding is that I cannot at this point use
leanproject up because this will change the toml again and I don't want to do this; I am not in the mood for bumping, mathlib has just been bumped in this project a few days ago and my co-author has it compiling with lean. Currently in
_target/deps/mathlib/src/algebra I have
ring/basic.lean and my toml says that my version of mathlib should have no file called ring.lean. How can I make leanproject get rid of it?
Patrick I don't think you see this situation because you are typically either working on mathlib (where
leanproject up is essentially always the right thing to do because you're tracking a branch) or working on a single-user project which has mathlib as a dependency. All this stuff is being ignored by git and we have some branches which are working with one version of mathlib and some with a different version, because only master got bumped, and I think the system cannot handle this. But my problem is that user1 bumped mathlib and now user2 has a broken local installation through no fault of their own because
leanproject get-mathlib-cache does not seem to remove out of date lean files.
I think I want a command which simply deletes _target and re-installs mathlib + oleans from the version in the toml. This seems to me to be a failsafe workaround.
Deleting oleans doesn't fix it
Kevin Buzzard (Aug 10 2020 at 17:08):
OK so I just checked this with guinea pig user3. user1 had bumped mathlib in master on github and user3 has not
yet updated. If they do
git pull and then
leanproject get-mathlib-cache on leanproject v0.0.8 and then they have both
algebra. But this complaint is currently on hold because perhaps you changed it on 0.0.9
Patrick Massot (Aug 10 2020 at 18:23):
Could you please try with 0.0.10? I would really like to help you here.
Kevin Buzzard (Aug 10 2020 at 19:46):
Here is a question which we can try with 0.0.10. I have a repo and different branches are on different mathlib commits. For one branch algebra/ring.lean exists, and for another one
algebra/ring/basic.lean exists. Here is what I thought was a reasonable usage of leanproject (I'm using 0.0.10):
$ leanproject get ImperialCollegeLondon/group-theory-game ... Looking for local mathlib oleans Found local mathlib oleans $ cd group-theory-game $ lean --make src/group/definitions.lean ## works fine. Note that master mathlib dependency is after the ring change. $ git checkout Sylow_theorems ## branch from before the recent ring -> ring/basic mathlib change $ leanproject get-mathlib-cache Looking for local mathlib oleans Found local mathlib oleans $ lean --make src/group/definitions.lean /home/buzzard/temp/group-theory-game/_target/deps/mathlib/src/algebra/field.lean:1:0: error: ambiguous import, it can be '/home/buzzard/temp/group-theory-game/_target/deps/mathlib/src/algebra/ring/default.lean' or '/home/buzzard/temp/group-theory-game/_target/deps/mathlib/src/algebra/ring.lean' ...
Kevin Buzzard (Aug 10 2020 at 19:50):
leanproject get-mathlib-cache I have both
Kevin Buzzard (Aug 10 2020 at 19:54):
I would just tell my users to reclone with
leanproject get, which of course works, but some of them have branches which they haven't pushed
Jalex Stark (Aug 10 2020 at 20:02):
the thing i would do is commit and push (maybe to a separate branch), and then nuke, re-clone, and delete extra files / sort out merge conflicts by hand. This tactic is maybe more error-prone than you would like, but it was enough to get out of the messes i made for myself while refactoring data/polynomial.
Patrick Massot (Aug 10 2020 at 20:20):
This is definitely a bug.
Kevin Buzzard (Aug 10 2020 at 22:02):
Ok I'll file an issue
Kevin Buzzard (Aug 10 2020 at 22:13):
@Jalex Stark the issue is not what I would do -- it's what to tell an undergraduate to do.
Jalex Stark (Aug 10 2020 at 22:14):
Yes, I agree that my advice is too brittle to routinely give to undergrads.
Last updated: May 12 2021 at 05:19 UTC