Zulip Chat Archive

Stream: general

Topic: leanproject up?


Jeremy Avigad (May 09 2020 at 11:21):

I just typed leanproject up in a mathlib project and got a cryptic message 3-11-0, and now mathlib is totally gone. Did I do something wrong?

Jeremy Avigad (May 09 2020 at 11:24):

leanproject get-mathlib-cache at least got mathlib back.

Patrick Massot (May 09 2020 at 11:25):

Maybe there is some issue because Lean got upgraded yesterday

Patrick Massot (May 09 2020 at 11:25):

Is mathlib updated yet?

Patrick Massot (May 09 2020 at 11:26):

I can reproduce

Patrick Massot (May 09 2020 at 11:33):

The origin is clear: someone create a branch named lean-3-11-0, which doesn't match the usual naming scheme

Patrick Massot (May 09 2020 at 11:34):

But it also means the code in mathlib tools in not robust enough.

Patrick Massot (May 09 2020 at 11:36):

And using the usual naming scheme would have created a problem until this branch is actually compiling. I really need to fix this. But I need to go. I'll try to work on that really soon. Sorry about the inconvenience

Jeremy Avigad (May 09 2020 at 11:48):

No worries here -- the workaround was easy to find. Thanks for looking into it.

Johan Commelin (May 09 2020 at 12:14):

My apologies for creating a branch with a bad name :sweat: :face_palm:

Patrick Massot (May 09 2020 at 12:36):

Relying on those branch names was a bad idea anyway

Patrick Massot (May 09 2020 at 12:42):

Actually I'm sure what is the current workflow with mathlib branches. Can I safely assume that if I download mathlib's leanpkg.toml from git master, there will be a branch named after the lean version mentioned in the leanpkg.toml? @Gabriel Ebner

Gabriel Ebner (May 09 2020 at 12:45):

With a bit of delay, yes.

Patrick Massot (May 09 2020 at 12:50):

Thanks. The delay is bad because it means things are sometimes broken, but I guess this is hard to avoid when the project is moving so fast


Last updated: Dec 20 2023 at 11:08 UTC