update-mathlib update

Stream: general

[Patrick Massot]

Let me continue here the conversation from https://leanprover.zulipchat.com/#narrow/stream/113489-new-members/topic/Cannot.20start.20tutorials.2C.20nor.20import.20topology.2Ebasic.2C.20nor.2E.2E.2E/near/188584734 which should now be in the general stream. Question: why do we call the mathlib nightlies by there date (like nightly-2020-02-20) instead of using a git SHA? If we were using a SHA we could download them without needing the Git API (or webpage scrapping). Soon we'll want nightlies for every commit anyway.

[Simon Hudon]

If we were using a SHA we could download them without needing the Git API (or webpage scrapping)

Interesting. I didn't know that. There's no reason not to do it except that it makes downloading them manually harder

[Patrick Massot]

I mean: look at the url https://github.com/leanprover-community/mathlib-nightly/releases/download/nightly-2020-02-20/mathlib-olean-nightly-2020-02-20.tar.gz

[Patrick Massot]

This would be a perfectly guessable url if those dates were replaced by git SHA

[Sebastian Ullrich]

Originally I did want one release per day (for leanprover/lean-nightly), so using the date made perfect sense. If you want to move to one release per commit, then using the hash makes more sense of course.

[Patrick Massot]

I don't know how to proceed here. Any change in the nightly thing will break existing update-mathlib. So it doesn't make sense to do it too often. If Rob finds us a new hosting solution next week then we should wait.

[Patrick Massot]

Sebastian, my comment was specifically about the mathlib olean archives

[Patrick Massot]

There's nothing wrong with the Lean nightlies (especially those days...)

[Sebastian Ullrich]

Yeah, just wanted to answer your question as to why it was done so in the first place (which was then copied to other repos)

[Patrick Massot]

In elan, how do you avoid using the GitHub API?

[Sebastian Ullrich]

I parse HTML using regexes, of course

[Mario Carneiro]

Obligatory SE reference

[Kevin Buzzard]

now with added disputes

[Simon Hudon]

I thought Mario was linking to this CS adage:

Some people, when confronted with a problem, think "I know, I'll use regular expressions." Now they have two problems.