What's your workflow to review Mathlib PR's

Stream: mathlib4

[metakuntyyy]

So question for reviewers that are looking for golfs. How do you review PR's? Do you check the branch out and try golfing ideas? Or do you copy paste the declaration that you want to golf?

Because my current workflow of copy-pasting seems cumbersome. I didn't yet find a good, frictionless workflow.

[Thomas Murrills]

gh pr checkout 12345 followed by lake exe cache get (or the equivalent VS code extension command—"get cache for current imports" is also useful if you don't want the whole cache) is my go-to for interacting with the declarations in a PR, golfing or not. :)

[Kevin Buzzard]

In my opinion the best golfs are those that either (a) greatly decrease compilation time without sacrificing readability or (b) decrease the number of times lemmas are called explicitly (replacing calls to lemmas with calls to tactics). If you're getting into golfing then please don't just assume that because you've shaved 5 characters of a proof that this represents progress! Making a proof a bit shorter because rfl happens to work two lines from the end but takes 10 seconds to compile is definitely a step backwards, for example :-)

[metakuntyyy]

Does anyone have a different workflow that they use or are most/all of you using gh-cli to checkout foreign branches? I'm not really using gh-cli and instead use git-ssh to push/pull. Before the fork based workflow one could just check out the branch directly.

[David Renshaw]

You don't need gh-cli to pull from PR branches. I do

git fetch origin pull/12345/head:pr12345

[metakuntyyy]

@David Renshaw Do I even need to pull? Wouldn't a detached checkout origin/pull/12345 work as well?

[David Renshaw]

I think the PR refs don't get fetched by default.

[metakuntyyy]

I guess I have to add a second origin to the main repo right?

git remote -v
origin  https://github.com/metakunt/mathlib4.git (fetch)
origin  https://github.com/metakunt/mathlib4.git (push)

I get this

git fetch origin pull/32811/head:test
fatal: couldn't find remote ref pull/32811/head

[Johan Commelin]

Yup, add a remote that points to the main repo. I call that remote upstream on my machines.

[metakuntyyy]

Ah, yeah it works, although I was a bit more unoriginal with my name orig.

I tried checking it out, it works but unfortunately I couldn't figure out how to do a detached checkout.

[metakuntyyy]

Nvm it is git switch FETCH_HEAD after the fetch.

[Snir Broshi]

metakuntyyy said:

Does anyone have a different workflow that they use or are most/all of you using gh-cli to checkout foreign branches?

I'm doing the same awkward copy-paste you mentioned, though I'll for big PRs I'd use gh-cli.
The GitHub CLI is useful to have regardless, I'm using it to keep track of PRs using gh api graphql, e.g.

echo '{"query":"{ search(type: ISSUE, first: 100, query: \"repo:leanprover-community/mathlib4 is:pr author:@me\") { nodes { ... on PullRequest { number state title } } } }"}' | gh api graphql --input -

[metakuntyyy]

Very nice.

I tried the git fetch orig... and it worked, but lake exe cache get tries to pull from my repository instead of the authors. Do I have to configure that as well, because rebuilding takes a lot of time?

[Kevin Buzzard]

lake exe cache get definitely works out of the box with gh.

[metakuntyyy]

I see, I'll try it tomorrow.

[Artie Khovanov]

Is there any tutorial on this workflow available? nws if not, I can read this thread carefully and try to understand what to do

[Etienne Marion]

Part 2 here: https://leanprover-community.github.io/contribute/git.html

[Snir Broshi]

Artie Khovanov said:

Is there any tutorial on this workflow available? nws if not, I can read this thread carefully and try to understand what to do

Press the Code button on the top-right of a PR, copy the command, and run it on your local clone of Mathlib
image.png

after it finishes, run lake exe cache get, and you're done

[Snir Broshi]

and here's the link to install the GitHub CLI if you don't have it: https://cli.github.com/

[Snir Broshi]

(I prefer installing with winget install -e --id GitHub.cli on Windows and brew install gh on macOS, depends on whether you like package managers)