Feedback on scripts/migrate_to_fork.py

Stream: mathlib4

[Chris Birkbeck]

So, I'm trying this out, but just got this error, have I done something wrong? I was just saying yes to all the instructions the script gave :

Found leanprover-community/mathlib4 as remote 'origin'
Rename 'origin' to 'upstream'? [Y/n]: y
⚠ ⚠️  Changing remote names will reset upstream tracking for all branches.
   This is much faster than renaming, but means other local branches will need
   their upstream reset manually later.
   ✅ Don't worry: This script will automatically fix the upstream for your
   current branch after the remote changes.
✓ Replaced remote with 'upstream'
Current origin: https://github.com/leanprover-community/mathlib4.git
Replace existing 'origin' with your fork? [Y/n]: y
✗ Command failed: git remote remove origin
✗ Error: error: No such remote: 'origin'

[Jeremy Tan]

What is going on?

[Jeremy Tan]

I'm still getting the same error even after syncing on my fork

[Jeremy Tan]

What do I need to fix

[Matthew Ballard]

It sounds like you already have a branch on your fork. Did you use the migration script to create the fork?

[Jeremy Tan]

I used the migration script to both create my fork and migrate the PR #25770 for the branch h-recursors – that was OK. Now I'm trying to migrate deprime-algtop-cattheory and I'm getting the above error @Matthew Ballard

[Matthew Ballard]

Do you have changes in the branch on the remote leanprover-community/mathlib4 repo compared to your local clone?

[Jeremy Tan]

On my local copy of leanprover-community/mathlib4 I merged master, and then I ran the migration script there

[Jeremy Tan]

@Matthew Ballard – the repo is the central repository I have always been using, I have pulled my forked repo at Documents/Computing/mathlib4

parclytaxel@parclytaxel-winterthur:~/Documents/Computing/Repos/mathlib4$ git checkout deprime-algtop-cattheory
Switched to branch 'deprime-algtop-cattheory'
parclytaxel@parclytaxel-winterthur:~/Documents/Computing/Repos/mathlib4$ scripts/migrate_to_fork.py
🔄 Mathlib4 Fork Migration Script
This script will help you migrate from direct write access to using forks.


=== Step 1: Checking GitHub CLI installation and authentication ===
✓ GitHub CLI is installed
✓ GitHub CLI is authenticated
✓ GitHub CLI token has required scopes

=== Step 2: Identifying GitHub username ===
✓ GitHub username: Parcly-Taxel

=== Step 3: Checking for fork of mathlib4 ===
✓ SSH access to GitHub is available - will use SSH URLs
✓ Fork exists: Parcly-Taxel/mathlib4
Synchronizing fork's master branch...
✓ Fork synchronized with upstream

=== Step 4: Setting up git remotes ===
✓ Upstream remote already configured correctly
✓ Origin remote (fork) already configured correctly

Current branch: deprime-algtop-cattheory

=== Step 5: Pushing branch 'deprime-algtop-cattheory' to fork ===
✗ Command failed: git push -u origin deprime-algtop-cattheory
✗ Error: To github.com:Parcly-Taxel/mathlib4.git
 ! [rejected]                deprime-algtop-cattheory -> deprime-algtop-cattheory (non-fast-forward)
error: failed to push some refs to 'github.com:Parcly-Taxel/mathlib4.git'
hint: Updates were rejected because the tip of your current branch is behind
hint: its remote counterpart. If you want to integrate the remote changes,
hint: use 'git pull' before pushing again.
hint: See the 'Note about fast-forwards' in 'git push --help' for details.

[Joscha Mennicken]

@Jeremy Tan As far as I can tell, the branch deprime-algtop-cattheory on your fork is pointing to the exact same commit as deprime-algtop-cattheory in the main mathlib4 repo, namely b8c95be. Maybe the branch in your local repository is out of sync from both remotes? In that case, you could either reset it to either of the remotes or force-push it to both before trying the script again.

[Matthew Ballard]

Ok. I am guessing attempting to push your changes to the branch on leanprover-community/mathlib4 will reproduce the error

[Jeremy Tan]

Joscha Mennicken said:

Jeremy Tan As far as I can tell, the branch deprime-algtop-cattheory on your fork is pointing to the exact same commit as deprime-algtop-cattheory in the main mathlib4 repo, namely b8c95be. Maybe the branch in your local repository is out of sync from both remotes? In that case, you could either reset it to either of the remotes or force-push it to both before trying the script again.

I don't get it

[Jeremy Tan]

What commands do I run

[Sebastian Ullrich]

Try git pull? That may be a missing step in the script

[Matthew Ballard]

I think you should follow the hint and git pull and follow the instructions.

[Matthew Ballard]

Let me know how it goes.

[Jeremy Tan]

git pull (on the central mathlib4) produces this error

There is no tracking information for the current branch.
Please specify which branch you want to merge with.
See git-pull(1) for details.

    git pull <remote> <branch>

If you wish to set tracking information for this branch you can do so with:

    git branch --set-upstream-to=<remote>/<branch> deprime-algtop-cattheory

[Robin Carlier]

Emily Riehl said:

Robin Carlier's answer to my question above makes me realize I don't understand the migration script. Where and when do I run it?

Should I create a fork first before running it, or run it first? If I have multiple open PRs, do I run this multiple times (after checking out each branch separately) or do I just run this once? Is the script creating separate forks for each one or moving them all to branches of a single new fork? What else do I need to know?

The script is in scripts/migrate_to_fork.py.

I think the script can create the fork for you, but I created my fork before running the script and it works just fine.
You do have to run it once for every PR, but once you have a created fork, it will not create a new one, and instead create and push branches on your existing fork.
For each PR you want to migrate, you need to
1) checkout the branch you want to migrate, using either git switch <branch-name> or gh pr checkout <PR-number>
2) merge master (if PR depends on other PRs, first migrate them, then merge these instead of master)
3) run the script
and that’s it :D

[Matthew Ballard]

Francesco N. Chotuck said:

I ran the scrip and my PR migrated but it's missing the topic label, and I also got this error:

Hmm. I will fix this one manually. #25759

[Joscha Mennicken]

Jeremy Tan said:

git pull (on the central mathlib4) produces this error

There is no tracking information for the current branch.
Please specify which branch you want to merge with.
See git-pull(1) for details.

    git pull <remote> <branch>

If you wish to set tracking information for this branch you can do so with:

    git branch --set-upstream-to=<remote>/<branch> deprime-algtop-cattheory

In your case, git pull origin <branch>

[Robin Carlier]

Also, the script has the gh CLI as a hard dependency. that might be good to know.

[Jeremy Tan]

Ran the script after git pull origin ... and it worked – #25774

[Jeremy Tan]

I will be keeping track of my migrated PRs and branches at #PR reviews > Jeremy Tan's open PRs @ 💬

[Kim Morrison]

Robin Carlier said:

Some things I noticed with the migration script:

• draft PRs are reopened as non-draft PRs when migrated.

#25777

[Kim Morrison]

Chris Birkbeck said:

So, I'm trying this out, but just got this error, have I done something wrong? I was just saying yes to all the instructions the script gave :

Found leanprover-community/mathlib4 as remote 'origin'
Rename 'origin' to 'upstream'? [Y/n]: y
⚠ ⚠️  Changing remote names will reset upstream tracking for all branches.
   This is much faster than renaming, but means other local branches will need
   their upstream reset manually later.
   ✅ Don't worry: This script will automatically fix the upstream for your
   current branch after the remote changes.
✓ Replaced remote with 'upstream'
Current origin: https://github.com/leanprover-community/mathlib4.git
Replace existing 'origin' with your fork? [Y/n]: y
✗ Command failed: git remote remove origin
✗ Error: error: No such remote: 'origin'

I think this issue should be fixed by #25789, but I wouldn't mind a second human checking the logic here...

[Jeremy Tan]

OK, I should have migrated all my 8 active PRs to my fork of mathlib4. (I have taken this opportunity to delete all my stale PRs I no longer have an interest in)

[Jeremy Tan]

@Kim Morrison the migrated PRs all look fine, no?

[Chris Birkbeck]

Kim Morrison [said]
I think this issue should be fixed by #25789, but I wouldn't mind a second human checking the logic here...

So I tried this and still no luck, it did get further, but now has some other error. I left a comment on the PR with the description.

[Vlad Tsyrklevich]

Just some feedback: I was hitting the error pasted below ("error checking for existing pull request: no remote for" for anyone using Zulip search) when I first used the migration script. I checked gh --version, it was 2.66.0 from this January. Surprisingly, updating gh fixed this error and the script succeeded.

vlad@Vlads-MacBook-Air:~/Development/mathlib4 (vlad.tsyrklevich/cg4-istree) python scripts/migrate_to_fork.py
:counterclockwise: Mathlib4 Fork Migration Script
This script will help you migrate from direct write access to using forks.

=== Step 1: Checking GitHub CLI installation and authentication ===
✓ GitHub CLI is installed
✓ GitHub CLI is authenticated
✓ GitHub CLI token has required scopes

=== Step 2: Identifying GitHub username ===
✓ GitHub username: vlad902

=== Step 3: Checking for fork of mathlib4 ===
✓ SSH access to GitHub is available - will use SSH URLs
✓ Fork exists: vlad902/mathlib4
Synchronizing fork's master branch...
✓ Fork synchronized with upstream

=== Step 4: Setting up git remotes ===
✓ Upstream remote already configured correctly
✓ Origin remote (fork) already configured correctly

Current branch: vlad.tsyrklevich/cg4-istree
✓ Branch 'vlad.tsyrklevich/cg4-istree' is already configured to push to your fork
:check: Branch 'vlad.tsyrklevich/cg4-istree' is already configured to push to your fork - skipping migration

=== Step 6: Checking for existing PR ===
✓ Found existing open PR from main repo: #25630 - feat(SimpleGraph): Weaker condition for paths in acyclic graphs
URL: https://github.com/leanprover-community/mathlib4/pull/25630
Create new PR from fork and close the old one? [Y/n]: y

=== Step 7: Creating new PR from fork ===
Using title from old PR: feat(SimpleGraph): Weaker condition for paths in acyclic graphs
Fetching complete PR details...
✓ Found 1 labels to copy: t-combinatorics
✗ Command failed: gh pr create --repo leanprover-community/mathlib4 --head vlad902:vlad.tsyrklevich/cg4-istree --title feat(SimpleGraph): Weaker condition for paths in acyclic graphs --body IsAcyclic.isPath_iff_chain' defines a weaker condition for proving that a walk is a path, in particular it shows that rather than proving that all vertices in the support of a walk are distinct, one must only show that consecutive edges are distinct (e.g. every other vertex must be distinct.) This leads to a simple corollary that trails are also paths in acyclic graphs.

---

This PR continues the work from #25630.

*Original PR: https://github.com/leanprover-community/mathlib4/pull/25630*
✗ Error: error checking for existing pull request: no remote for "vlad902:vlad.tsyrklevich/cg4-istree@{push}" found in "upstream, origin"

some excerpts from .git/config that may be relevant

...
[branch "vlad.tsyrklevich/cg4-istree"]
vscode-merge-base = origin/master
remote = origin
merge = refs/heads/vlad.tsyrklevich/cg4-istree
rebase = true
...
[remote "upstream"]
url = git@github.com:leanprover-community/mathlib4.git
fetch = +refs/heads/:refs/remotes/upstream/
[remote "origin"]
url = git@github.com:vlad902/mathlib4.git
fetch = +refs/heads/:refs/remotes/origin/

[Notification Bot]

A message was moved here from #mathlib4 > all future PRs should be made from forks by Eric Wieser.

[Nailin Guan]

I have a a problem that might be a bit silly: when trying to run scripts/migrate_to_fork.py
it show some errors

🔄 Mathlib4 Fork Migration Script
This script will help you migrate from direct write access to using forks.


=== Step 1: Checking GitHub CLI installation and authentication ===
✓ GitHub CLI is installed
Exception in thread Thread-3 (_readerthread):
Traceback (most recent call last):
  File "C:\Users\35718\AppData\Local\Programs\Python\Python313\Lib\threading.py", line 1041, in _bootstrap_inner
    self.run()
    ~~~~~~~~^^
  File "C:\Users\35718\AppData\Local\Programs\Python\Python313\Lib\threading.py", line 992, in run
    self._target(*self._args, **self._kwargs)
    ~~~~~~~~~~~~^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
  File "C:\Users\35718\AppData\Local\Programs\Python\Python313\Lib\subprocess.py", line 1609, in _readerthread
    buffer.append(fh.read())
                  ~~~~~~~^^
UnicodeDecodeError: 'gbk' codec can't decode byte 0x93 in position 15: illegal multibyte sequence
✓ GitHub CLI is authenticated
Exception in thread Thread-5 (_readerthread):
Traceback (most recent call last):
  File "C:\Users\35718\AppData\Local\Programs\Python\Python313\Lib\threading.py", line 1041, in _bootstrap_inner
    self.run()
    ~~~~~~~~^^
  File "C:\Users\35718\AppData\Local\Programs\Python\Python313\Lib\threading.py", line 992, in run
    self._target(*self._args, **self._kwargs)
    ~~~~~~~~~~~~^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
  File "C:\Users\35718\AppData\Local\Programs\Python\Python313\Lib\subprocess.py", line 1609, in _readerthread
    buffer.append(fh.read())
                  ~~~~~~~^^
UnicodeDecodeError: 'gbk' codec can't decode byte 0x93 in position 15: illegal multibyte sequence
✗ GitHub CLI token lacks required 'repo' scope.
Please re-authenticate with required scopes:
  gh auth login --scopes 'repo,workflow'

I run gh auth login --scopes 'repo,workflow but it still show the last error. Can anyone help? Thanks

[Joscha Mennicken]

Could you apply this diff to the script and try running it again? It adds an encoding="utf8"on line 80.

diff --git a/scripts/migrate_to_fork.py b/scripts/migrate_to_fork.py
index e550f15aaf..106daeb989 100755
--- a/scripts/migrate_to_fork.py
+++ b/scripts/migrate_to_fork.py
@@ -77,7 +77,7 @@ def print_error(message: str) -> None:
 def run_command(cmd: List[str], capture_output: bool = True, check: bool = True) -> subprocess.CompletedProcess:
     """Run a command and return the result."""
     try:
-        result = subprocess.run(cmd, capture_output=capture_output, text=True, check=check)
+        result = subprocess.run(cmd, capture_output=capture_output, text=True, encoding="utf8", check=check)
         return result
     except subprocess.CalledProcessError as e:
         if not check:

[Joscha Mennicken]

My suspicion (based on the subprocess docs) is that subprocess.run uses the system encoding because neither encoding nor universal_newlines is set, but gh always outputs utf-8.

[David Loeffler]

I have tried to use the migration script on my PR #25529 and it keeps crashing at Step 4:

=== Step 4: Setting up git remotes ===
Found leanprover-community/mathlib4 as remote 'origin'
Rename 'origin' to 'upstream'? [Y/n]: Y
⚠ ⚠️  Changing remote names will reset upstream tracking for all branches.
   This is much faster than renaming, but means other local branches will need
   their upstream reset manually later.
   ✅ Don't worry: This script will automatically fix the upstream for your
   current branch after the remote changes.
✗ Command failed: git remote remove origin
✗ Error: error: could not delete references: cannot lock ref 'refs/remotes/origin/AffineLocalToPretop': Unable to create '/Users/davidloeffler/lean/mathlib4/.git/refs/remotes/origin/AffineLocalToPretop.lock': File exists.

Another git process seems to be running in this repository, e.g.
an editor opened by 'git commit'. Please make sure all processes
are terminated then try again. If it still fails, a git process
may have crashed in this repository earlier:
remove the file manually to continue.

Removing the file named in the error message doesn't help, and there are no other git processes running. Answering no rather than yes to the last prompt doesn't help, it still gives the same error.

[Robin Carlier]

Do you have VSCode open at the same time? I don’t know very well the inner working of VS code but it might be spawning git processes?

[David Loeffler]

I do not have VSCode open at the same time.

[Robin Carlier]

Perhaps you can try setting up the remotes manually and then re-run the script?
git remote -v to list your remotes, and confirm that the rename is not already done, then if not git remote rename origin upstream (if origin points to leanprover-community/mathilb4) and then git remote add origin <your-fork>

[Robin Carlier]

This process should only be done once and not everytime for every migration so it should be fine doing it manually once and for all.

[David Loeffler]

I did that manually. But how do I create a new PR from the branch in my personal fork (to replace the existing non-fork PR)? GitHub isn't giving me the option, because (unsurprisingly) there are no new commits in "my fork / my branch" which aren't in "master repo / my branch". How do I get it to compare "my fork / my branch" against "master repo / master", not against the old PR branch in master?

[Joscha Mennicken]

One option is to go to mathlib4's pull requests page, click "New pull request", click "compare across forks", and select your fork/branch as the source. You should also be able to do this in your own fork's PR page, though in my case it already let me choose the target repo, and mathlib was already correctly filled in as target.

[David Loeffler]

Thanks, that worked! I am still puzzled why the official migration script did not work though; I have quite a few PR's in the works, and it will be very annoying if I have to re-create them all by hand.

[Robin Carlier]

is the script still crashing even after setting up the remotes manually?

[David Loeffler]

Yes.

[Robin Carlier]

Do you have other files with .lock extensions in .git/refs/... ? Is it always the same file/command that fails when you re-run the script? I’m trying to understand what happens but I have to admit I’m a bit clueless here.

[David Loeffler]

The file it's protesting about does not exist in the first place. There are no files with .lock extensions in that directory.

[Robin Carlier]

I’m sorry, I’m out of ideas about what is causing this :/
The fact that git complains about the file despite you not seeing it could mean that it’s a lock created by a previous invocation of git/gh within the script, but reading through the script I see no situation in which concurent gits could be running.

[Joscha Mennicken]

It could maybe be caused by weird file systems, for example file syncing or mounting over a network?

David Loeffler said:

The file it's protesting about does not exist in the first place. There are no files with .lock extensions in that directory.

Earlier, you said "Removing the file named in the error message doesn't help" - so there was a lock file at some point, but now it no longer appears?

[David Loeffler]

I ran rm -f (as specifically advised by the script itself). This removes the file if it exists, and silently does nothing otherwise.

[David Loeffler]

Moreover, I am not working on a "weird file system", unless a nearly-new MacBook Pro with its default configuration qualifies as weird.

[Bryan Gin-ge Chen]

I wonder if it has something to do with case-(in)sensitivity? I know very little about git and just found a few similar-looking error messages via google, e.g. https://github.com/newren/git-filter-repo/issues/325

Apologies if this is completely off-base.

[Robin Carlier]

Bryan, it seems mathlib4 has a branch AffineLocalToPretop, and a branch AffineLocalToPreTop, so you might, in fact, be completely spot on.
Looks like it was in fact a weird file system :D

[Robin Carlier]

Minor nitpick point: how feasible would it be for the zulip-emoji bot to use an emoji different from when the PR is migrated? maybe some kind of arrow emoj?

[Michael Rothgang]

Should be doable by

• creating a new label moved-to-fork
• making the script label the migrated PR with that label
• making the emoji bot react with an arrow to PRs labelled thusly

[Michael Rothgang]

I could do (1) and (3), but am less sure how to do (2).

[Michael Rothgang]

(And will only have time for this on Tuesday or Wednesday.)

[Robin Carlier]

I think 1 and 2 are desirable regardless of the emoji bot, at least to filter "actually closed" PRs from the ones that were just moved.

[Damiano Testa]

It might be easier in terms of available automation to

• add a migrated-to-fork label in the migration script;
• repurpose one of the "label-listening" github action to recognize migrated-to-fork and also add a migration emoji.

[Damiano Testa]

(Michael, if you want to try this out, feel free to do so: I probably won't have time during the weekend.)

[Joscha Mennicken]

Michael Rothgang said:

I could do (1) and (3), but am less sure how to do (2).

I think you'd want to add the label to the list directly after this line.

[Damiano Testa]

Michael, re-reading your message, I realise that what I wrote is exactly what you wrote: I had misinterpreted your proposal, but I fully support it! :slight_smile:

[Michael Stoll]

I'm trying to use the scipt to move my only open PR to a fork. I get a similar error as @Nailin Guan did (after merging origin/master into the relevant branch):

~/lean4/mathlib4$ ./scripts/migrate_to_fork.py
🔄 Mathlib4 Fork Migration Script
This script will help you migrate from direct write access to using forks.


=== Step 1: Checking GitHub CLI installation and authentication ===
✓ GitHub CLI is installed
✓ GitHub CLI is authenticated
✗ GitHub CLI token lacks required scopes.
Required scopes: repo, workflow
Please re-authenticate with required scopes:
  gh auth login --scopes 'repo,workflow'

Then I did gh auth login --scopes 'repo,workflow' as suggested, which seemed to succeed. But then running the script again still gives the same error.

The version of gh on my machine is

~/lean4/mathlib4$ gh --version
gh version 2.23.0 (2023-02-27 Debian 2.23.0+dfsg1-1)
https://github.com/cli/cli/releases/tag/v2.23.0

which does not look too recent, but sudo apt install gh tells me that the currently installed version is the newest one.

I followed the instructions that were given to @David Loeffler yesterday to migrate my PR manually (#24752 --> #25856), and it's unlikely that I'll want to migrate more, but it would still be nice to fix this problem in case other people run into it.

[Joscha Mennicken]

That is a pretty old gh version. For reference, this is my version:

gh version 2.74.0 (2025-05-30)
https://github.com/cli/cli/releases/tag/v2.74.0

What is the output of gh auth status for you?

[Michael Stoll]

$ gh auth status
github.com
  ✓ Logged in to github.com as MichaelStollBayreuth (/home/mstoll/.config/gh/hosts.yml)
  ✓ Git operations for github.com configured to use ssh protocol.
  ✓ Token: gho_************************************
  ✓ Token scopes: admin:public_key, gist, read:org, repo, workflow

...which should be OK? It contains repo and workflow...

[Joscha Mennicken]

Yes, I don't see how the current version of the script can produce the error above based on this output.

[Jz Pan]

Robin Carlier said:

Bryan, it seems mathlib4 has a branch AffineLocalToPretop, and a branch AffineLocalToPreTop, so you might, in fact, be completely spot on.
Looks like it was in fact a weird file system :D

I don't think this has something to do with case sensitivity of file system. There are branches whose name contain ', which is forbidden in Windows file system. But they can still be checked out normally (you need to type git checkout "branch_name'").

[Robin Carlier]

Jz Pan said:

Robin Carlier said:

Bryan, it seems mathlib4 has a branch AffineLocalToPretop, and a branch AffineLocalToPreTop, so you might, in fact, be completely spot on.
Looks like it was in fact a weird file system :D

I don't think this has something to do with case sensitivity of file system. There are branches whose name contain ', which is forbidden in Windows file system. But they can still be checked out normally (you need to type git checkout "branch_name'").

Well, the error is identical to the one described in Bryan's link, happening precisely on a branch (or rather to the lock file of a branch) that has a "duplicate" with a name differing by case only, on an OS that has a case insensitive file system, seems like a lot for a coincidence to me.

[Robin Carlier]

But I agree that there is something confusing in that this doesn't seem to happen to everyone one with a case insensitive file system...

[Bryan Gin-ge Chen]

Supposing the issue that David is seeing is the same as in the link, what should we do to fix it? I'm a little out of my depth here but I can try to do some research if someone has some pointers.

[Eric Wieser]

Jz Pan said:

There are branches whose name contain ', which is forbidden in Windows file system

This is false, ' is legal in filenames on my windows system, and so presumably on NTFS in general

[Robin Carlier]

Apparently there's a git option that makes things better in such file systems
Perhaps locally adding this config to the script, then restoring the original value?

[Robin Carlier]

(of course, locally adding it only if file system is case insensitive... This might be hard to detect from the script side.)

[Joscha Mennicken]

I've opened #25857 as an attempt to fix the two auth scope related issues mentioned in this thread.

[Robin Carlier]

Bryan Gin-ge Chen said:

Supposing the issue that David is seeing is the same as in the link, what should we do to fix it? I'm a little out of my depth here but I can try to do some research if someone has some pointers.

Running

❯ git branch -r | grep upstream | uniq -di
  upstream/AffineLocalToPreTop

says that in fact this is the only branch with dupe name up to case.
The branch has identical commits with its duplicate AFAICT.
Perhaps the solution is as simple as to delete this branch on the main repo? Since anyway no more branches should/will be created soon that’s a "solution"?

[Bryan Gin-ge Chen]

Robin Carlier said:

Apparently there's a git option that makes things better in such file systems
Perhaps locally adding this config to the script, then restoring the original value?

To be clear, the suggestion is to have the script set git config core.ignorecase true on case-insensitive file systems (possibly temporarily)? I'm on macOS as well with a case insensitive APFS drive, but git config --get core.ignorecase returns true.

[Eric Wieser]

I think that's about filenames not about branch names

[Bryan Gin-ge Chen]

Robin Carlier said:

Running

❯ git branch -r | grep upstream | uniq -di
  upstream/AffineLocalToPreTop

says that in fact this is the only branch with dupe name up to case.
The branch has identical commits with its duplicate AFAICT.
Perhaps the solution is as simple as to delete this branch on the main repo? Since anyway no more branches should/will be created soon that’s a "solution"?

Ah, maybe we should do that too. In any case it's confusing if there are branches whose names differ only in case, so maybe we should prevent this somehow. (Though I guess it's less pressing now that there should be fewer branches created in the main repo.)

[David Loeffler]

I think a cull of dead git branches is way overdue in any case.

[Yaël Dillies]

This is quite dangerous, as removing branches is when you could actually lose information. And dead branches are useful sometimes: Not so long ago I fished up a branch from three years ago by @Alex J. Best

[Bryan Gin-ge Chen]

We had several threads about cleaning up stale branches a few years ago #mathlib4 > Stale branches. Of course WIP branches, even if very stale, should not be deleted. In any case, since we don't have a policy for deleting other people's branches, it's up to contributors do clean up after themselves (though that will be harder as we lock down write access).

[Eric Wieser]

An easy answer is to make a mathlib4-backup repo into which we copy all branches, and then delete all branches that remain from the main repo

[Eric Wieser]

The branch# linkifier may as well go to that backup, since it won't work for forks anyway

[Eric Wieser]

(in the fork workflow I think we should just prefer draft PRs)

[Robin Carlier]

Bryan Gin-ge Chen said:

Robin Carlier said:

Apparently there's a git option that makes things better in such file systems
Perhaps locally adding this config to the script, then restoring the original value?

To be clear, the suggestion is to have the script set git config core.ignorecase true on case-insensitive file systems (possibly temporarily)? I'm on macOS as well with a case insensitive APFS drive, but git config --get core.ignorecase returns true.

Yes that was the suggestion, (either true or false, depending on what would be needed), but since in your case it’s already on I’m not sure that’s the right solution.

[Bryan Gin-ge Chen]

Well, I've never seen that error either, so I guess the question is what the setting is on @David Loeffler's machine.

[Robin Carlier]

In the case of AffineLocalToPretop, I think the choice is clear: the branches have same content, and apparently creates weird bugs for some people, so should be safe to delete independently of a future more massive branch culling.

[Bryan Gin-ge Chen]

So AffineLocalToPreTop had a (closed) PR associated with it in #14266 and AffineLocalToPretop did not, so I've deleted the latter just now. cc: @Dagur Asgeirsson

[Michael Rothgang]

Damiano Testa said:

Michael, re-reading your message, I realise that what I wrote is exactly what you wrote: I had misinterpreted your proposal, but I fully support it! :slight_smile:

I made a PR doing so. Two questions

• which emoji would be useful? :right: could be one version, :next_track: another. If it's unintuitive, it's not as helpful, so I'm interested in your opinion!
• should the migration script label the old, the new PR or both? (The location above is for labelling the new. Intuitively, I would've labelled the old PR instead.)

I'm running out of time now and can return to this by Wednesday.

[Michael Rothgang]

I see Kim just pushed my PR to completion: thank you for doing this!

[David Loeffler]

Bryan Gin-ge Chen said:

Well, I've never seen that error either, so I guess the question is what the setting is on David Loeffler's machine.

FWIW, on my machine git config --get core.ignorecase returns true. I will re-test the migrate script later today and find out if deleting one of the two nearly-identically-named branches solves the problem.

[Robin Carlier]

you might want to git fetch upstream (syncing remote branches with the upstream ones) and also perhaps deleting the bad branch AffineLocalToPretop on your local fork if it made it there as well (git branch -r | grep origin | uniq -Di to check if it’s here) before trying to re-migrate.

[David Loeffler]

uniq -Di doesn't work on Mac, but I did git fetch --prune and checked by hand that the AffineLocalToPretop branch is gone.

[David Loeffler]

It fails again :sad:

=== Step 4: Setting up git remotes ===
Found leanprover-community/mathlib4 as remote 'origin'
Rename 'origin' to 'upstream'? [Y/n]: Y
⚠ ⚠️  Changing remote names will reset upstream tracking for all branches.
   This is much faster than renaming, but means other local branches will need
   their upstream reset manually later.
   ✅ Don't worry: This script will automatically fix the upstream for your
   current branch after the remote changes.
✗ Command failed: git remote remove origin
✗ Error: error: could not delete references: cannot lock ref 'refs/remotes/origin/NoncommTensorProduct': Unable to create '/Users/davidloeffler/lean/mathlib4_master/.git/refs/remotes/origin/NoncommTensorProduct.lock': File exists.

Another git process seems to be running in this repository, e.g.
an editor opened by 'git commit'. Please make sure all processes
are terminated then try again. If it still fails, a git process
may have crashed in this repository earlier:
remove the file manually to continue.

[David Loeffler]

Looks like this is the same issue actually: there is a branch NoncommTensorProduct and another branch NonCommTensorProduct.

[David Loeffler]

@Junyan Xu these branches are both yours I think, is either of them still live?

[Robin Carlier]

:thinking: and here I thought AffineLocalToPretop was the only one... I’ll try running a better command than uniq -Di to see if there are more and report back
Well at least this pinpoints the issue.

[David Loeffler]

I guess the issue is that since the default sorting is case-sensitive, and lots of branch names start with Non, the branches NonCommTensorProduct and NoncommTensorProduct aren't adjacent in the sort order. If you do git branch -r | grep origin | sort -f | uniq -di, it returns precisely one hit and it's NonCommTensorProduct.

[Robin Carlier]

Right, uniq reports adjacent unique lines. I should have RTFM.

[David Loeffler]

So what are we going to do about these two near-identical branches? One is much older than the other; but the older one has a (draft) PR attached to it, while the newer one doesn't, and the newer one only contains 1 commit. We could re-name the newer branch (the lowercase-c one) to NoncommTensorProduct2 or something?

[David Loeffler]

OK, I renamed the NoncommTensorProduct branch and I can confirm that the migrate script does now work for me (see #25894, which is a migrate of my open PR #25078). Some feedback:

• There is a mystery eror message in step 7:

=== Step 7: Creating new PR from fork ===
Using title from old PR: feat(NumberTheory/ModularForms): GL(2, R) action preserves holomorphy
Fetching complete PR details...
⚠ Could not fetch full PR details: string indices must be integers
✓ New PR created: https://github.com/leanprover-community/mathlib4/pull/25894
Fetching comments from original PR...
✓ Added comments summary from original PR

• It's great that the script now copies over comments. However, although it claims it's trying to filter out bot comments, this doesn't seem to work optimally: it copies over the output of Damiano's PR-summary bot (which is not needed, since the PR-summary bot immediately posts to the new PR as well); and it copies over posts from the merge-conflict bot, which is presumably unnecessary for the same reason.
• More seriously, open review comments on github (pointing to a particular line or lines in the PR code) don't seem to get copied across, which is a real loss IMHO.

[David Loeffler]

• The PR title gets copied across, but the PR description doesn't; it gets replaced with an auto-generated one. It would be better to copy over the existing description, and append the info about migration.
• Related to above: I have learned to strenuously avoid including link-ified references to other PR's in the part of the PR description above the divider (the bit that gets copied into the eventual commit message when the PR is merged), because otherwise GitHub posts a notification to the PR thread every time anyone, anywhere, pulls the updated mathlib into any downstream project – spam galore for years afterwards. The migration script, as currently written, will trigger this.

[Robin Carlier]

David Loeffler said:

• The PR title gets copied across, but the PR description doesn't; it gets replaced with an auto-generated one. It would be better to copy over the existing description, and append the info about migration.

This one is a definite (recently introduced?) bug. When migrating my PRs thursday the descriptions were copied correctly, e.g #25744.

[David Loeffler]

Robin Carlier said:

David Loeffler said:

• The PR title gets copied across, but the PR description doesn't; it gets replaced with an auto-generated one. It would be better to copy over the existing description, and append the info about migration.

This one is a definite (recently introduced?) bug. When migrating my PRs thursday the descriptions were copied correctly, e.g #25744.

Interesting. It definitely didn't with #25894, I had to copy it across by hand.

[Eric Wieser]

David Loeffler said:

• because otherwise GitHub posts a notification to the PR thread every time anyone, anywhere, pulls the updated mathlib into any downstream projec

This only happens when people misuse git rebase downstream, but unfortunately this is quite common.

[David Loeffler]

Here's a proposal for modifying the migration script (based on some extremely helpful comments from @Shreyas Srinivas in another thread). The migration script creates a personal fork of Mathlib if you don't already have one, but it copies across all branches, and the mathlib repo has an immense number of branches (> 6000), the majority of which are not relevant to anyone except their creator.

Perhaps the migrate script should offer the choice of whether or not to copy non-master branches, possibly defaulting to not copying them?

[Bolton Bailey]

I am trying to run the script but it is not working. I am getting the following output:

> uv run scripts/migrate_to_fork.py
🔄 Mathlib4 Fork Migration Script
This script will help you migrate from direct write access to using forks.


=== Step 1: Checking GitHub CLI installation and authentication ===
✓ GitHub CLI is installed
✓ GitHub CLI is authenticated
✓ GitHub CLI token has required scopes

=== Step 2: Identifying GitHub username ===
✓ GitHub username: BoltonBailey

=== Step 3: Checking for fork of mathlib4 ===
✓ SSH access to GitHub is available - will use SSH URLs
✓ Fork exists: BoltonBailey/mathlib4
Synchronizing fork's master branch...
✓ Fork synchronized with upstream

=== Step 4: Setting up git remotes ===
Found leanprover-community/mathlib4 as remote 'origin'
Rename 'origin' to 'upstream'? [Y/n]: Y
⚠ ⚠️  Changing remote names will reset upstream tracking for all branches.
   This is much faster than renaming, but means other local branches will need
   their upstream reset manually later.
   ✅ Don't worry: This script will automatically fix the upstream for your
   current branch after the remote changes.
✗ Command failed: git remote remove origin
✗ Error: error: could not delete references: cannot lock ref 'refs/remotes/origin/AffineLocalToPretop': Unable to create '/Users/boltonbailey/Desktop/mathlibcontribution/mathlib4/.git/refs/remotes/origin/AffineLocalToPretop.lock': File exists.

Another git process seems to be running in this repository, e.g.
an editor opened by 'git commit'. Please make sure all processes
are terminated then try again. If it still fails, a git process
may have crashed in this repository earlier:
remove the file manually to continue.

But when I look for this file it mentions, it's not there:

> ls /Users/boltonbailey/Desktop/mathlibcontribution/mathlib4/.git/refs/remotes/origin/
ACL          ACL-J        ACLFN        ACLMIdFF     AIM          BoltonBailey HEAD         master

[David Loeffler]

If you do git fetch --prune and run it again, does it work?

[Bolton Bailey]

Yes, that resolves the error, thanks!

[David Loeffler]

(This deletes the local tracking branches corresponding to branches that were deleted or renamed on master. The script has issues with case-sensitivity of branch names, which have been solved by the somewhat brutal expedient of deleting or renaming one out of each of the two pairs of branches whose names differed only in capitalization.)

[David Loeffler]

I'm happy I can now help others out of the mess I myself previously ran into :-)

[Joscha Mennicken]

David Loeffler said:

Perhaps the migrate script should offer the choice of whether or not to copy non-master branches, possibly defaulting to not copying them?

I think the default in the GitHub UI is to only copy the master branch when forking a repo (at least it was for me a few days ago. Maybe it remembered my preferences from a previous fork?).

[David Loeffler]

The migrate script automatically makes a fork for you if you haven't already done it manually. Letting it run (with default settings) is how I got a fork with 6000 branches in it, iirc.

[Bolton Bailey]

Ok now it is telling me to checkout my other branches and migrate those too but I can't find them anymore?

[Bolton Bailey]

Do I need to run some kind of fetch operation? (Update: yes, running git fetch upstream seemed to work.)

[Bolton Bailey]

Another note: I am getting a warning

=== Step 7: Creating new PR from fork ===
Using title from old PR: feat: add simp lemmas for trig functions on `π * 2⁻¹`
Fetching complete PR details...
⚠ Could not fetch full PR details: string indices must be integers, not 'str'
✓ New PR created: https://github.com/leanprover-community/mathlib4/pull/25912
Fetching comments from original PR...
✓ Added comments summary from original PR

This doesn't seem to cause a concrete problem, but perhaps it's of interest to the people who wrote the script?

[Joscha Mennicken]

I agree that it makes sense for the fork created by the script to only include master. To do this, the argument --default-branch-only needs to be added to this command.

[David Loeffler]

David Loeffler said:

If you do git fetch --prune and run it again, does it work?

I made a PR #25913 to add this line to the migrate script.

[Bolton Bailey]

I notice that only one of the branches I migrated just now was given the migrated-from-branch tag, is something going wrong?

[Joscha Mennicken]

Maybe you executed different versions of the script in each branch (older versions did not add the tag), or maybe the script is broken in some scenarios. The former could happen if you did not merge master into each branch before migrating it.

[Eric Wieser]

Bolton Bailey said:

I notice that only one of the branches I migrated just now was given the migrated-from-branch tag, is something going wrong?

I applied it manually

[Joscha Mennicken]

In that case, maybe your master itself was outdated? You can update it by running git switch master followed by git pull upstream master.

[Bolton Bailey]

I merged upstream master from an hour ago each time

[David Loeffler]

I just migrated a couple more PR's and it seems that neither the PR description, nor the labels on the existing PR, are getting copied across (edit: and the bot-comments filter isn't filtering out most of the bot comments).

[Michael Rothgang]

Reading this thread, the filtering of comments to migrate (great addition btw!) should be tweaked in two ways: it should allow comments from FR-vdash-bot (who is a human), and it should remove comments from github-actions (the summary comment).

[David Loeffler]

Another bot to be filtered out is leanprover-community-bot-assistant (the username under which merge-conflict warnings are posted)

[Kim Morrison]

I'm not going to hard code an exception for FR-vdash-bot. They should change their github username. :-)

[Kim Morrison]

Could someone please collate a list of usernames of bots that need to be filtered out? It's no longer the weekend, so I need to get my actual work done instead of working on the migration script. :-)

[Michael Rothgang]

Kim Morrison said:

I'm not going to hard code an exception for FR-vdash-bot. They should change their github username. :-)

I politely disagree with the first part: this seems very unexpected behaviour of the script, especially since it fails silently.

[Michael Rothgang]

That said: I can take a look at this bug tomorrow afternoon and probably suggest a fix.

[Kim Morrison]

Hard to disagree with my statement that I'm not going to do it, but I look forward to you doing, thank you @Michael Rothgang!

[Johan Commelin]

chore: minor tweaks to migration script #26003

fixes some small things, including the issue that the old PR number shouldn't end up in the commit message of the new PR.

[Wrenna Robson]

A small comment: I had previously named my branches "linesthatinterlace/BRANCHNAME". However after migration I can't really rename them because that kills the migrated PR, which I want to retain. It isn't the end of the world but it would be cool if there was something for this in the script?

[Johan Commelin]

@Wrenna Robson Could you please explain the problem in a bit more detail?

[Wrenna Robson]

Ah, apologies.

So consider #26007. This was previous a PR from the branch linesthatinterlace/finiteperm. Now it is a PR from the branch on my fork linesthatinterlace:linesthatinterlace/finiteperm. What I would have really wanted was to rename the branch on my fork to finiteperm, so that the PR was from linesthatinterlace:finiteperm.

[Wrenna Robson]

Now that the migrated PR is created, I cannot rename the branch on my fork, because really that is the same as deleting the branch and creating a new one, so while GitHub can rename the branch fine, it results in killing the migrated PR and me needing to make one from scratch.

[Johan Commelin]

Aha, I see. Do I understand correctly that this does not mean things are broken, but just that you find the name long and redundant?

[Wrenna Robson]

Yes, correct - it's a "nice to have" rather than a breaking problem.

[Wrenna Robson]

Overall I found it very straightforward (possibly because I am using the script after a few days of bug-testing, as I was away!)

[Johan Commelin]

Understood. In that case, I'm inclined to just leave this as is. It's a one time thing. With new PRs you can pick the name you want.

[Wrenna Robson]

Aye, indeed :)

[Wrenna Robson]

But I thought feedback would be useful even if the conclusion is WONT_FIX.

[Wrenna Robson]

I have added the "migrated-from-branch" label manually to my PRs - was this the correct thing to do?

[Antoine Chambert-Loir]

I just tried my first migration. I accepted that origin be renamed as upstream in Step 4, but then the automatic command git push -u origin ACL/groebnerdoc provided by Step 4 didn't work. I tried with upstream instead of origin, and that worked — apparently. What did I miss?

=== Step 4: Setting up git remotes ===
Found leanprover-community/mathlib4 as remote 'origin'
Rename 'origin' to 'upstream'? [Y/n]:
⚠ :warning: Changing remote names will reset upstream tracking for all branches.
This is much faster than renaming, but means other local branches will need
their upstream reset manually later.
:check: Don't worry: This script will automatically fix the upstream for your
current branch after the remote changes.
✓ Replaced remote with 'upstream'
✓ Added origin remote pointing to your fork

Current branch: ACL/groebnerdoc

=== Step 5: Pushing branch 'ACL/groebnerdoc' to fork ===
✗ Command failed: git push -u origin ACL/groebnerdoc
✗ Error: ERROR: Repository not found.
fatal: Could not read from remote repository.

Please make sure you have the correct access rights
and the repository exists.

(7:09) pro-acl > git push -u upstream ACL/groebnerdoc
(seems to work)

[Joscha Mennicken]

What does git remote -v say in your repo?

[Antoine Chambert-Loir]

(7:15) pro-acl > git remote -v
origin git@github.com:AntoineChambert-Loir/mathlib4.git (fetch)
origin git@github.com:AntoineChambert-Loir/mathlib4.git (push)
upstream git@github.com:leanprover-community/mathlib4.git (fetch)
upstream git@github.com:leanprover-community/mathlib4.git (push)

[Joscha Mennicken]

That looks correct, but your fork https://github.com/AntoineChambert-Loir/mathlib4 doesn't seem to exist (at least not publicly).

[Markus Himmel]

Your fork of mathlib4 is called ZModnUnits instead of mathlib4: https://github.com/AntoineChambert-Loir/ZModnUnits I don't know why that is, but you can rename it in the web interface:
image.png

[Antoine Chambert-Loir]

There is something I don't understand here, sorry if my questions are absurd.
I made one fork to create this PR ZModnUnits. But now I am willing to migrate other PR and I am using scripts/migrate_to_fork.py. Should I have one single mathlib4 fork, and create branches from them?
Then, I need probably to rename my initial fork, but create a branch within in, and start new branches from that fork? If that even makes sense, I'll probably need some help.

[Yaël Dillies]

Yes, you only need one fork for all your PRs

[Yaël Dillies]

You can create several PRs from your fork, one PR per branch on the fork

[Antoine Chambert-Loir]

OK, thank you. So now I probably need to 1. rename my fork, 2. set it as a branch, 3. create new branches. But I have no idea about how to implement 2.

[Shreyas Srinivas]

Step 2 is not a real thing

[Shreyas Srinivas]

Once you have a fork

[Shreyas Srinivas]

It is a separate repository

[Shreyas Srinivas]

On which you can create your own branches

[Shreyas Srinivas]

Same as you have been doing in mathlib so far

[Antoine Chambert-Loir]

I managed to do something. That crashed my first PR on that branch and I lost the comments that had been kindly given by @Thomas Browning and @Junyan Xu .

[Shreyas Srinivas]

Do you have your mathlib4 PR number at hand?

[Antoine Chambert-Loir]

The new one is #26020, and the previous one is #25879 (it was in some Zulip message).

[Shreyas Srinivas]

Basically you can create a reference to the old PR with a note in the new PR

[Antoine Chambert-Loir]

Thank you! It had just been closed, not destroyed. Sorry for that mess.

[Shreyas Srinivas]

I have done it for you.

[Shreyas Srinivas]

You will see a link in #25879 to #26020

[Shreyas Srinivas]

Now you won’t lose access to those comments from the new PR

[Shreyas Srinivas]

This was suggested as one of the alternatives to the migration script in Kevin’s announcement as well

[Michael Rothgang]

I just had it migrate #25094: the new PR looks mostly fine --- but some comments are missing (and the labels also). While running, the log contains the line ⚠ Could not fetch full PR details: string indices must be integers, not 'str'. Any ideas why?

[Michael Rothgang]

Michael Rothgang said:

That said: I can take a look at this bug tomorrow afternoon and probably suggest a fix.

#26081

[Bhavik Mehta]

I'm getting the following error on running the script:

=== Step 1: Checking GitHub CLI installation and authentication ===
✓ GitHub CLI is installed
✓ GitHub CLI is authenticated
✓ GitHub CLI token has required scopes

=== Step 2: Identifying GitHub username ===
✗ Failed to get GitHub username: Expecting value: line 1 column 1 (char 0)

[Joscha Mennicken]

What does gh api user show when you run it?

[Bhavik Mehta]

It prints out some json with my github username and other account information

[Bhavik Mehta]

It's not completely clear to me that it's safe to share the whole thing, so I'll show the first two lines:

$ gh api user
{
  "login": "b-mehta",

[Joscha Mennicken]

The error sounded like the script saw an empty output instead of JSON, so I wanted to check whether the gh output was reasonable, but it seems like it is.

[Bhavik Mehta]

I hard-coded my username into the script, but now I'm getting another error:

✗ Command failed: git fetch --all --prune
✗ Error: error: could not delete references: cannot lock ref

[Bhavik Mehta]

Is there a description somewhere of what this script actually does? It's looking like it's easier to just run the steps myself instead of trying to understand what it's attempting to do

[Joscha Mennicken]

The readme at https://github.com/leanprover-community/mathlib4/tree/master/scripts describes what the script tries to do, but not all individual steps.

[Joscha Mennicken]

I think the script does roughly the following:

1. Set up your local repo so the remote upstream points to mathlib and origin points to your own fork (creating a fork in the process if necessary)
2. Push your branch to your own fork (git push -u origin branchname)
3. Create a new PR with the original title and description, amended with info about where the PR came from (taking care to create a draft PR if the original PR was also one)
4. Copy over labels and add the migrated-from-branch label
5. Post the non-bot comments of the original PR as a single new comment
6. Close the old PR and add a comment pointing to the migrated PR

[Bhavik Mehta]

After about 45 minutes of debugging the first issue, in part privately with Joscha, we managed to find the root cause, but after (many hours more) for the second, I still can't get the script to work. Is there any better option than manually migrating here?

[Kim Morrison]

@Bhavik Mehta, can you try doing it from a fresh clone?

[Bhavik Mehta]

I will try this when I have some free time, thanks for the suggestion!

[Mario Carneiro]

I notice an authorship issue: #25287 is a PR authored by me and co-authored by Emily, and it was migrated by Emily to #25784, which is now authored and co-authored by Emily (but the first commit still has me as author). Will this cause issues for bors? Does the co-authored-by field need to be edited by the script to account for this?

[Matthew Ballard]

I think the answer to this is yes

[Yaël Dillies]

Yes and no: Having the first commit of a PR be authored by someone else than the author on that PR has always been confusing to bors. Unless you change the first commit for Emily to be the author of the commit, or reopen the PR for you to be the author of the PR, bors will mishmatch your identities: something like author name Emily Riehl, author email address digama@gmail.com

[Yaël Dillies]

I would advise:

1. You add an empty commit with author Emily at the start of the branch
2. You remove all Co-authored-by mention. bors can figure out you co-authored the PR so long as you've authored one of the last 25 commits on the branch. If that's unlikely to be the case by the time the PR is merged, add a Co-authored-by with your name

[Matthew Ballard]

I think there are problems beyond the usual bors issues but memory is hazy

[Yunge Yu]

Hi,

I'm trying to migrate this PR: https://github.com/leanprover-community/mathlib4/pull/25224

The script created this new PR https://github.com/leanprover-community/mathlib4/pull/26263, but stopped partway through with the following error.

✗ Command failed: gh pr edit 25224 --repo leanprover-community/mathlib4 --add-label migrated-to-fork
✗ Error: GraphQL: xcloudyunx does not have the correct permissions to execute `AddLabelsToLabelable` (addLabelsToLabelable)

What should I do in this situation?

[Bryan Gin-ge Chen]

Looks like the links in your message don't work, so here are some working ones:

• original PR: #25224
• migrated PR: #26263

I took a look at your PRs, and I re-added the easy tag by hand. Did you see the comment by @Oliver Nash? Please implement his suggestion and then we can merge your PR.

[Bryan Gin-ge Chen]

Side note: the script should probably be allowed to continue if adding labels fails; does someone want to look into this?

[Yunge Yu]

The changes have been made in #26263

[Bolton Bailey]

I have been trying to use the repository after migrating and I have been getting a bunch of git errors. Google told me to run git fsck and it reported an error

> git fsck
Checking object directories: 100% (256/256), done.
Checking objects: 100% (896671/896671), done.
error: refs/remotes/origin/BoltonBailey/finsupp-option 2: invalid sha1 pointer 0000000000000000000000000000000000000000

Is this a problem with the migration script or have I done something else wrong

[Bolton Bailey]

Is the issue perhaps that I cloned the leanprover community mathlib when I should have cloned my own fork?

[Joscha Mennicken]

It seems to me like somehow your local repository was corrupted; your fork seems to be unaffected. If you have no unpushed changes, cloning the repo freshly following the git guide should solve the problem.

You could also try the following steps if you don't want to redownload mathlib, they might fix the error directly:

1. Remove the file .git/refs/remotes/origin/BoltonBailey/finsupp-option
2. Run git fetch --all --prune

[Bolton Bailey]

Redownloading via the git guide helped, thank you!

[A.]

I wonder if some clever person could immediately spot what's gone wrong here? I've had a quick look through this thread and I can't see that anyone has reported the error before.

ali@Alistairs-MacBook-Pro mathlib % python3 scripts/migrate_to_fork.py
🔄 Mathlib4 Fork Migration Script
This script will help you migrate from direct write access to using forks.


=== Step 1: Checking GitHub CLI installation and authentication ===
✓ GitHub CLI is installed
✓ GitHub CLI is authenticated
✓ GitHub CLI token has required scopes

=== Step 2: Identifying GitHub username ===
✓ GitHub username: agjftucker

=== Step 3: Checking for fork of mathlib4 ===
⚠ SSH access to GitHub not available - will use HTTPS URLs
✓ Fork exists: agjftucker/mathlib4
Synchronizing fork's master branch...
✓ Fork synchronized with upstream

=== Step 4: Setting up git remotes ===
✓ Upstream remote already configured correctly
✓ Origin remote (fork) already configured correctly

Current branch: agjftucker/implicit

=== Step 5: Pushing branch 'agjftucker/implicit' to fork ===
✗ Command failed: git push -u origin agjftucker/implicit
✗ Error: error: RPC failed; HTTP 400 curl 22 The requested URL returned error: 400
send-pack: unexpected disconnect while reading sideband packet
fatal: the remote end hung up unexpectedly
Everything up-to-date

[A.]

I have fixed my SSH but I still get the same error at Step 5 :sad:

[Joscha Mennicken]

What error message to do you get if you run the command (git push -u origin agjftucker/implicit) manually while on the agjftucker/implicit branch?

[Joscha Mennicken]

Also, what does your git remote -v say?

[A.]

Thanks! This is what I get

ali@Alistairs-MacBook-Pro mathlib % git push -u origin agjftucker/implicit
Enumerating objects: 11389, done.
Counting objects: 100% (11389/11389), done.
Delta compression using up to 8 threads
Compressing objects: 100% (7600/7600), done.
error: RPC failed; HTTP 400 curl 22 The requested URL returned error: 400
send-pack: unexpected disconnect while reading sideband packet
Writing objects: 100% (7902/7902), 13.81 MiB | 10.57 MiB/s, done.
Total 7902 (delta 2778), reused 1641 (delta 179), pack-reused 0
fatal: the remote end hung up unexpectedly
Everything up-to-date
ali@Alistairs-MacBook-Pro mathlib % git remote -v
origin  https://github.com/agjftucker/mathlib4.git (fetch)
origin  https://github.com/agjftucker/mathlib4.git (push)
upstream    https://github.com/leanprover-community/mathlib4.git (fetch)
upstream    https://github.com/leanprover-community/mathlib4.git (push)

[Joscha Mennicken]

You're still trying to push over HTTPS, not SSH. Since the error seems HTTP specific, I suspect using SSH will circumvent it. You can use git remote set-url origin git@github.com:agjftucker/mathlib4.git to switch the origin remote to use SSH, and then try the push again.

[A.]

Thank you very much for your help. I would never have guessed that was the solution. I have run the script and it sort of worked but all the comment history has been lost :sad:. I guess the whole PR process just has to begin again.

[A.]

There was another error in Step 7 but the script ran to completion.

=== Step 7: Creating new PR from fork ===
Using title from old PR: feat(Analysis/Calculus/Implicit): define HasStrictDerivAt.implicitFunOfBivariate
Fetching complete PR details...
⚠ Could not fetch full PR details: string indices must be integers, not 'str'
✓ New PR created: https://github.com/leanprover-community/mathlib4/pull/26985
Fetching comments from original PR...
No comments found on original PR (or only bot comments)

[A.]

Also I now have a thousand merge conflicts according to GitHub that don't show up locally.

[Joscha Mennicken]

Those were probably caused by this commit, which is not present in your old PR.

[A.]

The instructions here say to

• Merge a recent version of master into your PR branch, if the script is not available at scripts/migrate_to_fork.py

[A.]

I guess it's best to do everything manually.

[Eric Wieser]

(deleted)

[Yunge Yu]

Bryan Gin-ge Chen said:

Side note: the script should probably be allowed to continue if adding labels fails; does someone want to look into this?

I want to mention that I got the exact same error again when migrating another PR just now.

The original PR is #25248
The migrated PR is #27226

[Aaron Liu]

I ran into a weird situation here

aaronliu@Haitao-MacBook-Pro-2021 mathlib4 % git remote -v
Vtec234 https://github.com/vtec234/mathlib4 (fetch)
Vtec234 https://github.com/vtec234/mathlib4 (push)
adamtopaz       https://github.com/adamtopaz/mathlib4 (fetch)
adamtopaz       https://github.com/adamtopaz/mathlib4 (push)
linesthatinterlace      https://github.com/linesthatinterlace/mathlib4 (fetch)
linesthatinterlace      https://github.com/linesthatinterlace/mathlib4 (push)
mathlib4-nightly-testing        https://github.com/leanprover-community/mathlib4-nightly-testing.git (fetch)
mathlib4-nightly-testing        https://github.com/leanprover-community/mathlib4-nightly-testing.git (push)
origin  https://github.com/plp127/mathlib4.git (fetch)
origin  https://github.com/plp127/mathlib4.git (push)
upstream        https://github.com/leanprover-community/mathlib4.git (fetch)
upstream        https://github.com/leanprover-community/mathlib4.git (push)
aaronliu@Haitao-MacBook-Pro-2021 mathlib4 % python3 scripts/migrate_to_fork.py
🔄 Mathlib4 Fork Migration Script
This script will help you migrate from direct write access to using forks.


=== Step 1: Checking GitHub CLI installation and authentication ===
✓ GitHub CLI is installed
✓ GitHub CLI is authenticated
✓ GitHub CLI token has required scopes

=== Step 2: Identifying GitHub username ===
✓ GitHub username: plp127

=== Step 3: Checking for fork of mathlib4 ===
⚠ SSH access to GitHub not available - will use HTTPS URLs
✓ Fork exists: plp127/mathlib4
Synchronizing fork's master branch...
✓ Fork synchronized with upstream

=== Step 4: Setting up git remotes ===
Found leanprover-community/mathlib4 as remote 'mathlib4-nightly-testing'
Rename 'mathlib4-nightly-testing' to 'upstream'? [Y/n]:

[Aaron Liu]

it thinks the nightly testing is my upstream (it's not)

[Aaron Liu]

I don't know if this will cause other issues so I've decided to cancel it for now

[Joscha Mennicken]

The broken/lazy code is here: https://github.com/leanprover-community/mathlib4/blob/27e7ed0c1a2df81fedf8760888857e7bb8ae9bf6/scripts/migrate_to_fork.py#L342C9-L342C51

Instead of checking whether the URL actually points to the remote, it only does a substring match and since https://github.com/leanprover-community/mathlib4-nightly-testing.git contains the substring leanprover-community/mathlib4, it thinks it points to mathlib.

[Bryan Gin-ge Chen]

OK, if no one beats me to it, I'll try and fix this issue (and the one about labels) later this week. (I'd also be happy to review / merge PRs addressing problems in the script).

[Bryan Gin-ge Chen]

#27646 should hopefully be a reasonable fix for the bad upstream detection logic.

[Bryan Gin-ge Chen]

Yunge Yu said:

Bryan Gin-ge Chen said:

Side note: the script should probably be allowed to continue if adding labels fails; does someone want to look into this?

I want to mention that I got the exact same error again when migrating another PR just now.

The original PR is #25248
The migrated PR is #27226

I'm checking the script now and it looks like it already has a fallback which posts a comment if adding labels fails. Could you (or someone else without write access) try and reproduce this? Basically I want to understand better what causes the script to terminate partway through instead of continuing on in a case like this.

[Rudy Peterson]

I also get the error for attempting to add the label:

python scripts/migrate_to_fork.py
🔄 Mathlib4 Fork Migration Script
This script will help you migrate from direct write access to using forks.


=== Step 1: Checking GitHub CLI installation and authentication ===
✓ GitHub CLI is installed
✓ GitHub CLI is authenticated
✓ GitHub CLI token has required scopes

=== Step 2: Identifying GitHub username ===
✓ GitHub username: rudynicolop

=== Step 3: Checking for fork of mathlib4 ===
✓ SSH access to GitHub is available - will use SSH URLs
✓ Fork exists: rudynicolop/mathlib4
Synchronizing fork's master branch...
✓ Fork synchronized with upstream

=== Step 4: Setting up git remotes ===
✓ Upstream remote already configured correctly
✓ Origin remote (fork) already configured correctly

Current branch: list-splits
✓ Branch 'list-splits' is already configured to push to your fork
✅ Branch 'list-splits' is already configured to push to your fork - skipping migration

=== Step 6: Checking for existing PR ===
✓ Found existing open PR from main repo: #24395 - feat(Data/List): list splitting definitions and lemmas
URL: https://github.com/leanprover-community/mathlib4/pull/24395
Create new PR from fork and close the old one? [Y/n]: Y

=== Step 7: Creating new PR from fork ===
Using title from old PR: feat(Data/List): list splitting definitions and lemmas
Fetching complete PR details...
⚠ Could not fetch full PR details: string indices must be integers, not 'str'
✓ New PR created: https://github.com/leanprover-community/mathlib4/pull/30391
Fetching comments from original PR...
✓ Added comments summary from original PR

=== Step 8: Closing old PR and adding comment ===
✓ Added comment to old PR
✗ Command failed: gh pr edit 24395 --repo leanprover-community/mathlib4 --add-label migrated-to-fork
✗ Error: GraphQL: rudynicolop does not have the correct permissions to execute `AddLabelsToLabelable` (addLabelsToLabelable)

[Bryan Gin-ge Chen]

Aha, I see at least one place where we're missing a fallback for missing permissions. I'll try and take a look tomorrow.