leanproject debugging

Stream: general

[Kevin Buzzard]

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 ring/*; the 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.lean and ring.olean and 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]

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 ring.lean and ring/default.lean in algebra. But this complaint is currently on hold because perhaps you changed it on 0.0.9

[Patrick Massot]

Could you please try with 0.0.10? I would really like to help you here.

[Kevin Buzzard]

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]

After leanproject get-mathlib-cache I have both ring.lean and ring/basic.olean

[Kevin Buzzard]

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]

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]

This is definitely a bug.

[Kevin Buzzard]

Ok I'll file an issue

[Kevin Buzzard]

@Jalex Stark the issue is not what I would do -- it's what to tell an undergraduate to do.

[Jalex Stark]

Yes, I agree that my advice is too brittle to routinely give to undergrads.