leanproject up?

Stream: general

[Jeremy Avigad]

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]

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

[Patrick Massot]

Maybe there is some issue because Lean got upgraded yesterday

[Patrick Massot]

Is mathlib updated yet?

[Patrick Massot]

I can reproduce

[Patrick Massot]

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

[Patrick Massot]

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

[Patrick Massot]

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]

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

[Johan Commelin]

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

[Patrick Massot]

Relying on those branch names was a bad idea anyway

[Patrick Massot]

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]

With a bit of delay, yes.

[Patrick Massot]

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