[Deicyde]

bot/refresh_tagged.py made every batch open slow. It is the step #65 found running 18 to 30+ minutes, and in 2026-08 200 of 221 batch-open ticks were cancelled inside it at the old 30-minute job limit.

Cause

The poller clones the fork with git clone --filter=blob:none (wikidata-poll.yml). refresh_tagged.py then runs git fetch --depth=1 <upstream> master and git grep … FETCH_HEAD -- Mathlib/.

• The clone has every fork branch's commits and trees but only the blobs of the master it checked out, and the fork's master lags upstream (today it dates from 2026-09-11 and is 882 commits behind).
• The fork's batch branches sit on recent upstream commits. The fetch negotiates, so the server treats those commits as already present and leaves out every blob reachable from them, which the blob:none clone never downloaded.
• git grep then reaches those blobs through the promisor remote, which is the fork, one blob per fetch.

Fix

Add --refetch (Git 2.36+): it skips negotiation, so the single shallow pack carries every blob in master's tree. Also add --no-auto-maintenance. After a refetch, git fetch sets gc.autoPackLimit=1 for its post-fetch maintenance, which repacks the whole repository on every run. On CI's throwaway clone that happens in the background next to the batch open, and on a long-lived local checkout it happens every time. Ordinary gc --auto at its default thresholds still consolidates the extra pack later. The log line fetching … master (shallow)… is unchanged, so the README guidance from #65 still applies. An older git fails the fetch, and the refresh already fails closed on a fetch error.

Evidence

Reproduced on leanprover-community/batteries with the bot's sequence: a blob:none clone checked out at a 2026-03 commit (standing in for the stale fork), then a shallow fetch of main and git grep FETCH_HEAD -- Batteries/, with GIT_TRACE2_EVENT counting child fetches.

	fetch	grep	lazy fetches	grep output
main	1 s	101 s	179	2027 lines
--refetch	1 s	<1 s	0	byte-identical (repacked to 2 packs in the background)
--refetch --no-auto-maintenance	1 s	1 s	0	byte-identical (3 packs kept, no repack)

At Mathlib scale the refetch downloads one shallow snapshot of master instead of thousands of single-blob fetches. I haven't measured it on Mathlib; the next batch open after mathlib4#42608 merges will show the real time. A local run against a long-lived full checkout (bot/daily_bot.py:101, bot/open_batch.py:228) also downloads the snapshot instead of an incremental fetch, and leaves one extra pack per run until ordinary gc --auto consolidates them.

Tests

bot/test_refresh_tagged.py (new, wired into scripts/ci-python.sh next to the other bot tests) stubs subprocess.run. It pins the fetch arguments (--depth=1 --refetch --no-auto-maintenance <upstream> master), checks that the grep runs on FETCH_HEAD, and checks both written lists. I didn't run it locally because machine load was above the agreed limit; CI runs it.

#65's timeouts (job 60 minutes, Poll tick 50) stay as headroom.

Not changed here: open_batch.py ignores refresh_tagged.py's exit code. A failed refresh doesn't overwrite the lists, but the open still proceeds with the previous ones.

[Deicyde]

Recommendation: close. Closing it now; reopen if the next batch open is still slow. An independent adversarial review of d9df2f95 found the code correct. But the problem it fixes no longer exists on the runner, and this PR's account of the cause had an error.

• The slow path was Git 2.54 and older.
  • Git 2.55.0 (tagged 2026-06-29) taught git grep and git cherry to collect the blobs a lazy clone is missing and fetch them in one request (RelNotes 2.55.0, lines 110-113). prefetch_grep_blobs() is in builtin/grep.c at v2.55.0 and not at v2.54.0.
  • The August batch opens ran Git 2.54.0 (for example run 32181933034). The poller has run 2.55.0 since about 2026-08-22 (for example run 39071619406), and the ubuntu-24.04 image lists Git 2.55.0.
  • No refresh has run since that change, so "fast on 2.55" is inferred from the source, not measured. My batteries reproduction used a local Git 2.53, so it reproduced August's runner, not today's.
• What the PR would cost now. On CI the old fetch plus the bulk prefetch should already be one or two requests, so --refetch gains nothing there. In exchange it costs:
  • a full shallow snapshot of Mathlib master (about 9,400 blobs, ~104 MB uncompressed) on every local run against a full checkout (bot/daily_bot.py:101, bot/open_batch.py:228), plus a pack left behind each time;
  • a Git 2.36 floor, whose failure those callers ignore, since sh() doesn't check the exit code.
• One correction to my body and comment. The newer commits that negotiation reports as present don't come from the fork's batch branches; those are older than its master. They come from personal PR branches on the fork, for example zlattice-torus, 1 commit behind upstream. The mechanism stood; the attribution was wrong.

If the next batch open after mathlib4#42608 merges still spends long in refresh_tagged.py, reopen this PR. -c fetch.negotiationAlgorithm=noop is a lighter alternative to test, since it avoids --refetch's forced repack hint. #65's 60/50-minute limits stay as headroom either way.