starting the port of a new file

Stream: mathlib4

[Johan Commelin]

From mathlib4/scripts/start_port.sh:

echo "usage: ./scripts/start_port.sh Mathlib/Foo/Bar/Baz.lean"

[Johan Commelin]

This will create a new branch named Foo.Bar.Baz with two commits:

1. the output of mathports Mathbin/Foo/Bar/Baz.lean
2. a commit that adds the new file to Mathlib.lean and replaces Mathbin by Mathlib in the import lines of the new file.

[Kevin Buzzard]

That's so cool that you keep the mathbin commit. I always check for mathbins as it gives me confidence that the commit claimed to be the first commit really is a commit with no edits at all to the mathlib3port file.

[Arien Malec]

Is this the preferred approach? Is it documented in the wiki?

[Eric Wieser]

Can we make it call the branch port/X.Y.Z instead?

[Eric Wieser]

One day we'll want to have non-port branches too!

[Johan Commelin]

Fair enough. I'll update the script.

[Johan Commelin]

@Arien Malec yes, I hope this will be adopted as the standard approach.

[Johan Commelin]

I'll document it in the wiki.

[Mario Carneiro]

well it's pretty weird to have branches named X.Y.Z otherwise

[Mario Carneiro]

they are usually named more like x_y_z

[Eric Wieser]

The next cool thing to build would be an update command that commits the latest mathport as a child of commit 1 (1a), then creates 2a as a child of 1 and 2 with the import fixes, then merges head

[Eric Wieser]

Mario, that doesn't work well for a_b.c vs a.b_c filenames

[Eric Wieser]

Git allows dots, so I don't think they're that weird. port/X/Y/Z would also be nice, as then the folder tree inside git matches the source tree (but this might be illegal for some branch names on windows!)

[Johan Commelin]

Eric Wieser said:

Can we make it call the branch port/X.Y.Z instead?

mathlib4#1170

[Mario Carneiro]

Eric Wieser said:

Mario, that doesn't work well for a_b.c vs a.b_c filenames

We don't have file names like that though?

[Mario Carneiro]

and also I don't understand how that is a conflict, those are different names

[Reid Barton]

I think Eric was assuming you were suggesting tr . _

[Mario Carneiro]

oh, no I meant to just use X.Y.Z and rely on the fact that most other branch names are named using a different convention to avoid conflicts

[Johan Commelin]

I've updated the wiki. (It assumes mathlib4#1170 will be merged at some point.)

[zbatt]

I'm having a bit of trouble with this. When I run ./scripts/start_port.sh Mathlib/Data/PNat/Prime.lean it seems to not work as I get back a file start_port_tmp.lean with contents 404: Not Found.

The output of running the command is

+ set -o pipefail
+ MATHLIB3PORT_BASE_URL=https://raw.githubusercontent.com/leanprover-community/mathlib3port/master
+ PORT_STATUS_YAML=https://raw.githubusercontent.com/wiki/leanprover-community/mathlib/mathlib4-port-status.md
+ TMP_FILE=start_port_tmp.lean
+ mathlib4_path=Mathlib/Data/PNat/Prime.lean
+++ echo Mathlib/Data/PNat/Prime.lean
+++ tr / .
++ basename Mathlib.Data.PNat.Prime.lean .lean
+ mathlib4_mod=Mathlib.Data.PNat.Prime
+ mathlib3port_url=https://raw.githubusercontent.com/leanprover-community/mathlib3port/master/Mathbin/Data/PNat/Prime.lean
+ curl --silent --show-error -o start_port_tmp.lean https://raw.githubusercontent.com/leanprover-community/mathlib3port/master/Mathbin/Data/PNat/Prime.lean
++ grep '^! .*source module '
++ sed 's/.*source module \(.*\)$/\1/'
+ mathlib3_module=

Any help would be really appreciated!

[zbatt]

I figured it out, there's an inconsistency in the naming schemes for PNat. In Mathlib4, its given as PNat, but in mathlib3port its given as Pnat which causes the curl to fail.

[Kevin Buzzard]

Oh nice catch!

[zbatt]

I feel like the naming inconsistency might make this port a bit delicate, so maybe not suitable for my first one haha. I'll leave it to the experts

[Arien Malec]

naming inconsistency is part of the joy of porting, along with autoimplicits, simp/rw inconsistencies -- just dive in!

[Reid Barton]

Is this Pnat vs PNat thing something we can/should inform mathport about?

[Johan Commelin]

I just created

chore: start_port.sh makes empty commit with nice PR title #1345

This should give you a nice PR title, when you open a PR.

[Eric Wieser]

mathlib4#1345

[Eric Wieser]

I don't think this helps?

[Eric Wieser]

Doesn't github just use the branch name for the PR title if there is more than one commit?

[Johan Commelin]

Nope, it takes the title of the first commit, in that case. I'm pretty sure about that.

[Johan Commelin]

Or is that something that hub does on my end?

[Eric Wieser]

That sounds like something hub does; or github changed this behavior within the last two days; I've not seen this happen before

[Anne Baanen]

The web interface indeed tries to parse the branch name, which I find very frustrating :(

[Eric Wieser]

For example: https://github.com/leanprover-community/mathlib/compare/eric-wieser/bad-pr-title?expand=1

[Johan Commelin]

Aah, I didn't realize it was hub doing that. Ok. Maybe let's drop the PR in that case.

[Yaël Dillies]

It helps if you open PRs from within VScode

[Eric Wieser]

Oh, you can set the title in a URL!

[Eric Wieser]

https://github.com/leanprover-community/mathlib/compare/eric-wieser/bad-pr-title?expand=1&title=this+is+ok

[Eric Wieser]

So maybe the script can just emit a url to click at the end to open the PR?

[Johan Commelin]

Ooh! That sounds like a good idea!

[Eric Wieser]

(don't forget to query-string-quote the title! Python's urllib.parse.quote_plus would do it)

[Johan Commelin]

script is in bash

[Johan Commelin]

chore: start_port.sh can print a URL to open PR with useful title mathlib4#1346

[Johan Commelin]

Should the script also do a git push?

[Eric Wieser]

I think it's fine to do the git push, as long as it:

• Does it silently, so that github doesn't insert it's own url with a bad link
• Catches errors and turns them into an error message like "someone else has already ported this file"

[Johan Commelin]

I don't know how to do that off the top of my head.

[Eric Wieser]

git push --quiet is the first. Maybe a better approach for the last is to first check if origin/$mathport_branch already exists

[Eric Rodriguez]

Have people tried the gh tool? gh pr new is a really good way to create a PR, in my experience.

[Johan Commelin]

gh pr create is perfect. It also uses the first commit message to create a PR title.

[Johan Commelin]

@Eric Wieser What do you think of doing both (i) an empty commit with a nice title at the start of the PR, and (ii) print a URL to open a PR with a nice title

[Johan Commelin]

That way we can support both a gh and non-gh workflow.

[Eric Wieser]

I don't think the empty commit does any harm if it helps with some workflows

[Johan Commelin]

I updated the PR

[Johan Commelin]

I suggest that the pushing etc be done in another PR.

[Arien Malec]

FWIW, my workflow is to first see if the port is possible for me to make meaningful progress on before I push. If I walk into a file and when I compile after fixing Mathlib I see a see of red that I have no idea how to fix, and I can't make progress on cleanup, I delete the branch and walk slowly away.

[Johan Commelin]

In mathlib4#1667 I add two tiny features to the start_port script:

• fix Smul and Pnat to SMul and PNat in import statements
• move by to the end of the previous line, when it fits

[Johan Commelin]

The second one might need some second touch ups due to later changes to the file, but I still hope it will take care of 90% of the by issues.

[Johan Commelin]

In semi-related news: mathport will now add #align statements for to_additiveized decls

[Eric Rodriguez]

Johan Commelin said:

In mathlib4#1667 I add two tiny features to the start_port script:

• fix Smul and Pnat to SMul and PNat in import statements
• move by to the end of the previous line, when it fits

fwiw, this causes the same issue for mac because awk doesn't line up on both operating systems - i think the workaround is similar, just worth noting

[Johan Commelin]

Good point.

[Arien Malec]

The workaround being "install gnu awk via brew"?

[Eric Rodriguez]

yes, and add the correct thing to your .zshrc

[Arien Malec]

I've taken to adding to /etc/paths

[Arien Malec]

Added instructions to the porting guide wiki.

[Eric Rodriguez]

Arien Malec said:

Added instructions to the porting guide wiki.

where exactly, sorry? can't find ti

[Arien Malec]

Last bullet of 3.

[Arien Malec]

Note that on OS X, the OS installed version of sed and awk do not work with the start_port.sh script. The fix is to install the GNU versions (e.g. via brew install gawk gsed) and ensure they, rather than the OS versions, are the default for sed and awk (e.g. by following the path instructions provided by brew)