Zulip Chat Archive

Stream: general

Topic: Refresh mathlib in local branch


view this post on Zulip Adam Topaz (Oct 08 2020 at 12:50):

What is the preferred workflow for the following scenario?

I have a branch foo of mathlib on my local machine created with leanproject get -b mathlib:foo that has a few commits, e.g. github would say This branch is n commit ahead, m commits behind master. where both n and m are strictly positive integers. I would like to use some newly added code from the master branch in mathlib. I assume from the point of view of git this means I should merge master into foo. Is there some way to use leanproject to get the fresh olean files as well? Is there some leanproject command/flag that will merge master -> foo and get the oleans as well?

view this post on Zulip Gabriel Ebner (Oct 08 2020 at 12:52):

I think the current state of the art is:

git merge origin/master
git push
sleep 2h
leanproject up

view this post on Zulip Adam Topaz (Oct 08 2020 at 12:53):

Gabriel Ebner said:

sleep 2h

really?

view this post on Zulip Eric Wieser (Oct 08 2020 at 12:55):

I usually checkout master, get-cache, return to my branch, then merge

view this post on Zulip Gabriel Ebner (Oct 08 2020 at 12:55):

Yes, this waits for the github actions to finish and upload the oleans. At the moment this takes a bit over an hour.

view this post on Zulip Johan Commelin (Oct 08 2020 at 12:55):

git checkout master
leanproject up
git checkout -
git merge master

view this post on Zulip Eric Wieser (Oct 08 2020 at 12:56):

It would be great if get-cache let me pass a commit-ish to avoid the pointless checkout

view this post on Zulip Eric Wieser (Oct 08 2020 at 12:56):

Since AFAIK get-cache doesn't care about my local lean files anyway, all it does is ask git for the head commit

view this post on Zulip Gabriel Ebner (Oct 08 2020 at 12:56):

mathlib-tools#77

view this post on Zulip Adam Topaz (Oct 08 2020 at 12:57):

@Johan Commelin will git checkout - return to the original non-master branch foo or should I actually use git checkout foo?

view this post on Zulip Eric Wieser (Oct 08 2020 at 12:57):

As an extension, it would be cool if leanproject would automatically find all built parent commits of my branch and let me pick between their oleans

view this post on Zulip Bryan Gin-ge Chen (Oct 08 2020 at 13:06):

I think Patrick's been a bit busy recently, but PRs are definitely welcome.

view this post on Zulip Adam Topaz (Oct 08 2020 at 13:07):

So I tried @Johan Commelin 's suggestion, and leanproject up gives me the following error:

Failed to parse line: ' git config pull.rebase false # merge (the default strategy)'

view this post on Zulip Adam Topaz (Oct 08 2020 at 13:10):

Okay,

git checkout master
git pull
leanproject get-cache
git checkout foo
git merge master

seems to do the trick for me.

view this post on Zulip Eric Wieser (Oct 08 2020 at 13:12):

Might have a go at a PR once my open one (https://github.com/leanprover-community/mathlib-tools/pull/79) goes through, since that will make development easier for me

view this post on Zulip Adam Topaz (Oct 08 2020 at 13:14):

The last line from leanproject -h is this

upgrade-mathlib    Upgrade mathlib (as a dependency or as the main...

What does as the main... mean?

view this post on Zulip Johan Commelin (Oct 08 2020 at 13:17):

@Adam Topaz git checkout - changes to the previous branch (like cd -)

view this post on Zulip Damiano Testa (Oct 08 2020 at 13:34):

I was going to post this in new-members but since this thread appears similar, at least to my git-newbie eyes, I thought of posting here!

I just pulled mathlib to my branch and when I ran leanproject get-cache and obtained the following error:

$ leanproject get-cache
Looking for local mathlib oleans
Looking for remote mathlib oleans
Trying to download https://oleanstorage.azureedge.net/mathlib/6e7e77761f15a95cd3569af1e76f0e56592851d4.tar.xz to /home/damiano/.mathlib/6e7e77761f15a95cd3569af1e76f0e56592851d4.tar.xz
Trying to download https://oleanstorage.azureedge.net/mathlib/6e7e77761f15a95cd3569af1e76f0e56592851d4.tar.gz to /home/damiano/.mathlib/6e7e77761f15a95cd3569af1e76f0e56592851d4.tar.gz
Trying to download https://oleanstorage.azureedge.net/mathlib/6e7e77761f15a95cd3569af1e76f0e56592851d4.tar.bz2 to /home/damiano/.mathlib/6e7e77761f15a95cd3569af1e76f0e56592851d4.tar.bz2
Looking for GitHub mathlib oleans
Info: No github section found in 'git config', we will use GitHub with no authentication
403 {"message": "API rate limit exceeded for 45.86.225.93. (But here's the good news: Authenticated requests get a higher rate limit. Check out the documentation for more details.)", "documentation_url": "https://developer.github.com/v3/#rate-limiting"}

Did I do something that I was not supposed to do? How do I get the cache?

Thank you!

view this post on Zulip Bryan Gin-ge Chen (Oct 08 2020 at 13:36):

The commit 6e7e776 doesn't exist on the mathlib repo, so it hasn't been built by CI. Maybe you need to push your branch?

view this post on Zulip Eric Wieser (Oct 08 2020 at 13:37):

What's the trailing error message about there? Are the oleans on both azure and github?

view this post on Zulip Damiano Testa (Oct 08 2020 at 13:38):

Bryan Gin-ge Chen said:

The commit 6e7e776 doesn't exist on the mathlib repo, so it hasn't been built by CI. Maybe you need to push your branch?

I wanted to pull to my local branch the changes in #4527. I am starting to realize that maybe I cannot do this, unless the PR has been merged?

view this post on Zulip Gabriel Ebner (Oct 08 2020 at 13:38):

Eric Wieser said:

What's the trailing error message about there? Are the oleans on both azure and github?

A long, long time ago we used to publish oleans as github releases

view this post on Zulip Eric Wieser (Oct 08 2020 at 13:39):

Is that code still there so that users can get oleans for those old releases?

view this post on Zulip Bryan Gin-ge Chen (Oct 08 2020 at 13:40):

I think Rob copied all those oleans to azure, so we could probably remove that code.

view this post on Zulip Bryan Gin-ge Chen (Oct 08 2020 at 13:42):

Ah, there's already a PR: https://github.com/leanprover-community/mathlib-tools/pull/76

view this post on Zulip Damiano Testa (Oct 08 2020 at 13:42):

[I am quite lost: is the discussion about trailing error messages, azure and github relating to API rate limit exceeded? Sorry if it isn't, but I am really confused...]

view this post on Zulip Eric Wieser (Oct 08 2020 at 13:44):

Yes - I asked that because the reason you had to ask your first question is because the error message doesn't say "This isn't (yet) in the cache", despite that being what's happening.

view this post on Zulip Damiano Testa (Oct 08 2020 at 13:44):

Ah, ok, thanks for the explanation!!

view this post on Zulip Bryan Gin-ge Chen (Oct 08 2020 at 13:45):

Damiano Testa said:

I wanted to pull to my local branch the changes in #4527. I am starting to realize that maybe I cannot do this, unless the PR has been merged?

You can pull those changes with git fetch origin; git merge origin/erase_lead2 (assuming the community mathlib repo is called origin in your local repo). However, there won't be oleans for the resulting merge commit unless you either run leanproject build or push a new branch to the mathlib repo and then wait for CI to finish.

view this post on Zulip Damiano Testa (Oct 08 2020 at 13:45):

Ok, thanks for the explanation @Bryan Gin-ge Chen !

view this post on Zulip Bryan Gin-ge Chen (Oct 08 2020 at 13:50):

By the way, for getting more comfortable with git, I recommend having a look at chapters 1-3 (and maybe 7) of https://git-scm.com/book/en/v2. At least for me it really helped me build up a mental model of what I was doing with all these strange commands.

view this post on Zulip Damiano Testa (Oct 08 2020 at 13:53):

Thank you for the reference manual! I will look at it, since I feel that the discussion here should help me, but every time I pull or push something, I then have to go to my own private folder, well away from Git's reach to recover a file that I lost...

view this post on Zulip Johan Commelin (Oct 08 2020 at 14:00):

@Damiano Testa Do you know "You might have invented spectral sequences"?

Here is "You might have invented git": https://news.ycombinator.com/item?id=1342902

view this post on Zulip Damiano Testa (Oct 08 2020 at 14:01):

I will look at this as well: I do feel that I have no idea what is happening every time I type git ...!

view this post on Zulip Eric Wieser (Oct 08 2020 at 14:05):

I found that providing coworkers with a git gui was a great way to have them go from "I type magic on the command line" to "I understand how git works now"

view this post on Zulip Johan Commelin (Oct 08 2020 at 14:14):

@Damiano Testa You should also remember that

Git gets easier once you understand branches are homeomorphic endofunctors mapping submanifolds of a Hilbert space

view this post on Zulip Damiano Testa (Oct 08 2020 at 14:15):

Johan Commelin said:

Damiano Testa You should also remember that

Git gets easier once you understand branches are homeomorphic endofunctors mapping submanifolds of a Hilbert space

In my current state, I am not even completely sure whether this is a joke or not... Ahaha

view this post on Zulip Johan Commelin (Oct 08 2020 at 14:39):

@Damiano Testa Don't worry, it's a joke

view this post on Zulip Damiano Testa (Oct 08 2020 at 14:40):

That's a relief! I was hoping that this was the case, but did not have the confidence to fully believe it!

view this post on Zulip Yury G. Kudryashov (Oct 08 2020 at 21:52):

Was it inspired by something like this Haskell joke?

view this post on Zulip Reid Barton (Oct 08 2020 at 21:57):

Related blog post: https://web.archive.org/web/20101221025743/http://tartley.com/?p=1267

view this post on Zulip Adam Topaz (Oct 08 2020 at 22:12):

I'm surprised this blog post didn't make some sort of GIT pun (as in https://en.wikipedia.org/wiki/Geometric_invariant_theory )


Last updated: May 13 2021 at 05:21 UTC