Refresh mathlib in local branch

Stream: general

[Adam Topaz]

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?

[Gabriel Ebner]

I think the current state of the art is:

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

[Adam Topaz]

Gabriel Ebner said:

sleep 2h

really?

[Eric Wieser]

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

[Gabriel Ebner]

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

[Johan Commelin]

git checkout master
leanproject up
git checkout -
git merge master

[Eric Wieser]

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

[Eric Wieser]

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

[Gabriel Ebner]

mathlib-tools#77

[Adam Topaz]

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

[Eric Wieser]

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

[Bryan Gin-ge Chen]

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

[Adam Topaz]

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)'

[Adam Topaz]

Okay,

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

seems to do the trick for me.

[Eric Wieser]

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

[Adam Topaz]

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?

[Johan Commelin]

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

[Damiano Testa]

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!

[Bryan Gin-ge Chen]

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?

[Eric Wieser]

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

[Damiano Testa]

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?

[Gabriel Ebner]

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

[Eric Wieser]

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

[Bryan Gin-ge Chen]

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

[Bryan Gin-ge Chen]

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

[Damiano Testa]

[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...]

[Eric Wieser]

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.

[Damiano Testa]

Ah, ok, thanks for the explanation!!

[Bryan Gin-ge Chen]

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.

[Damiano Testa]

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

[Bryan Gin-ge Chen]

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.

[Damiano Testa]

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...

[Johan Commelin]

@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

[Damiano Testa]

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

[Eric Wieser]

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"

[Johan Commelin]

@Damiano Testa You should also remember that

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

[Damiano Testa]

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

[Johan Commelin]

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

[Damiano Testa]

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

[Yury G. Kudryashov]

Was it inspired by something like this Haskell joke?

[Reid Barton]

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

[Adam Topaz]

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