search

leanprover-community / mathlib3

Lean 3's obsolete mathematical components library: please use mathlib4
https://leanprover-community.github.io/lean3
Apache License 2.0
1.66k stars 299 forks source link

following docs/elan.md "Scenario 1" instructions gives you an old mathlib #365

Closed rwbarton closed 5 years ago

rwbarton commented 5 years ago

As indicated in the title, if you follow the instructions at https://github.com/leanprover/mathlib/blob/master/docs/elan.md under "Scenario 1: Start a new package", replacing nightly-2018-04-06 by 3.4.1 according to master mathlib's current leanpkg.toml file, the result is that you get a checkout of the lean-3.4.1 branch of mathlib, which has not been updated since June 20. I described the situation in more detail on Zulip. This is potentially confusing to new users and even to me. I can easily diagnose what happened and how to fix it, but for the sake of new users we should make it impossible to end up in this situation in the first place.

I infer from elan.md (and also dimly recall) that there was a time when mathlib master built against a nightly version of Lean. As that is no longer the case, can we simply delete the lean-3.4.1 branch of mathlib? Then leanpkg should automatically choose the master branch, which is the desired behavior, right?

kbuzzard commented 5 years ago

I pushed for that branch to exist for the simple reason that I wanted to see for myself (and for my summer students) the possible advantages of having a stable version of everything. In theory this sounds like a way of injecting some sort of sanity into the situation, but in practice I did not find too many advantages, so would not be fighting to keep the 3.4.1 branch.

kbuzzard commented 5 years ago

Just to note here that Mario updated (sorry I don't know the proper git word) the 3.4.1 branch so it is now currently even with mathlib master. I do accept responsibility for some of this chaos; I really pushed Mario for a stable branch, for a good reason (mathlib was changing fast and I really wanted all my students to be on the same page at all times). At the time I did not realise the complex consequences which this decision would have. Perhaps we could have done it another way and the consequences for other people outside my group of students would not have been so weird.

When Lean 4 hits we might well need a 3.4.1 branch, when managing the transition, but this is probably not the thread to worry about this issue.

jcommelin commented 5 years ago

I think the problems described in this issue have been solved by the 3.4.2 branch etc... @rwbarton Shall we close this?

semorrison commented 5 years ago

I agree this is fixed.