restart port

Stream: mathlib4

[Yury G. Kudryashov]

Recently, I made too many changes to topology.order while porting. First, don't make this mistake. Second, here is how I recovered from it.

• Backport changes to mathlib, wait for the PR to be merged and mathlib3port to be regenerated (I've slightly sped up the process by manually starting the actions 1 2).
• Merge master into port/*.
• Edit start_port.sh to remove the safety check about porting being already started and use another branch name (port/tmp/* in my case).
• Run the modified script.
• Checkout port/*
• Run git reset --mixed port/tmp/branch
• Revert modification to the line with SHA sum.
• Review the diff and accept/reject modifications one by one (I use Emacs magit, probably VSCode has similar functionality).
• Forse-push to Github, delete temporary branch.

[Kevin Buzzard]

How about we ban making this mistake?

[Johan Commelin]

@Yury G. Kudryashov would you mind sharing that script?

[Yury G. Kudryashov]

It's just start-port with safety check commented out

[Yury G. Kudryashov]

--- scripts/start_port.sh   2023-02-11 01:04:25.260456356 -0600
+++ scripts/restart_port.sh 2023-01-31 03:27:40.885389231 -0600
@@ -8,7 +8,7 @@
 fi

 if [ ! $1 ] ; then
-    echo "usage: ./scripts/start_port.sh Mathlib/Foo/Bar/Baz.lean"
+    echo "usage: ./scripts/restart_port.sh Mathlib/Foo/Bar/Baz.lean"
     exit 1
 fi

@@ -27,7 +27,6 @@
 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=$1
@@ -39,20 +38,11 @@

 mathlib3_module=$(grep '^! .*source module ' <"$TMP_FILE" | sed 's/.*source module \(.*\)$/\1/')

-if curl --silent --show-error --fail "$PORT_STATUS_YAML" | grep -F "$mathlib3_module: " | grep "mathlib4#" ; then
-    set +x
-    echo "WARNING: The file is already in the process of being ported."
-    echo "(See line above for PR number.)"
-    rm "$TMP_FILE"
-    exit 1
-fi
-
 mkdir -p $(dirname "$mathlib4_path")
 mv "$TMP_FILE" "$mathlib4_path"

-git fetch
 mathlib4_mod_tail=${mathlib4_mod#Mathlib.}
-branch_name=port/${mathlib4_mod_tail}
+branch_name=port/tmp/${mathlib4_mod_tail}
 git checkout --no-track -b "$branch_name" origin/master

 # Empty commit with nice title. Used by gh and hub to suggest PR title.
@@ -79,8 +69,3 @@
    -m 'fix certain import statements' \
    -m 'move "by" to end of line' \
    -m 'add import to Mathlib.lean'
-
-set +x
-
-echo "After pushing, you can open a PR at:"
-echo "https://github.com/leanprover-community/mathlib4/compare/$branch_name?expand=1&title=feat:+port+$mathlib4_mod_tail&labels=mathlib-port"

[Yury G. Kudryashov]

This create a new port/tmp/something branch. I switch to the old branch, rebase it on master, then git reset --soft port/tmp/something, and discard/stage diff chunks one by one using Emacs magit

[Notification Bot]

4 messages were moved here from #mathlib4 > Algebra.Algebra.Basic by Yury G. Kudryashov.

[Johan Commelin]

Thanks

[Johan Commelin]

Created a PR with this script: https://github.com/leanprover-community/mathlib4/pull/2249

[Eric Wieser]

I pushed a change to that PR to allow us to reuse the same script behind a --restart flag