Zulip Chat Archive

Stream: general

Topic: update-mathlib update


view this post on Zulip 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.

view this post on Zulip 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

view this post on Zulip Patrick Massot (Feb 20 2020 at 20:29):

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

view this post on Zulip Patrick Massot (Feb 20 2020 at 20:29):

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

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip Patrick Massot (Feb 20 2020 at 20:33):

Sebastian, my comment was specifically about the mathlib olean archives

view this post on Zulip Patrick Massot (Feb 20 2020 at 20:33):

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

view this post on Zulip 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)

view this post on Zulip Patrick Massot (Feb 20 2020 at 20:42):

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

view this post on Zulip Sebastian Ullrich (Feb 20 2020 at 20:47):

I parse HTML using regexes, of course

view this post on Zulip Mario Carneiro (Feb 20 2020 at 20:55):

Obligatory SE reference

view this post on Zulip Kevin Buzzard (Feb 20 2020 at 20:57):

now with added disputes

view this post on Zulip Simon Hudon (Feb 20 2020 at 21:02):

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.


Last updated: May 12 2021 at 23:13 UTC