## Stream: general

### Topic: update-mathlib update

#### Patrick Massot (Feb 20 2020 at 18:24):

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 (Feb 20 2020 at 20:27):

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 (Feb 20 2020 at 20:29):

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

#### Sebastian Ullrich (Feb 20 2020 at 20:31):

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 (Feb 20 2020 at 20:32):

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 (Feb 20 2020 at 20:33):

Sebastian, my comment was specifically about the mathlib olean archives

#### Patrick Massot (Feb 20 2020 at 20:33):

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

#### Sebastian Ullrich (Feb 20 2020 at 20:39):

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 (Feb 20 2020 at 20:42):

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

#### Sebastian Ullrich (Feb 20 2020 at 20:47):

I parse HTML using regexes, of course

#### Mario Carneiro (Feb 20 2020 at 20:55):

Obligatory SE reference

#### Simon Hudon (Feb 20 2020 at 21:02):

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

Last updated: May 12 2021 at 23:13 UTC