prune_merged_worktrees.py : des REMOVE que git refusera toujours -- tolerance untracked par defaut vs remove sans --force #14509

prune_merged_worktrees.py peut décider REMOVE sur des worktrees que git worktree remove refusera toujours. Ces entrées sont re-proposées à chaque exécution et ne quittent jamais le disque : c'est exactement l'accumulation que #14195 devait arrêter.

Les deux règles se contredisent

L'invariant 3 de l'en-tête du module est explicite :

Aucun git worktree remove --force. Le retrait est git worktree remove sans --force ; si git refuse (worktree sale), on log la cause et FAILED.

Mais is_source_dirty ne salit un worktree que si un chemin untracked se termine par une extension source :

def is_source_dirty(path: str) -> bool:
    p = path.replace("\\", "/")
    if is_untracked_artifact(p):
        return False
    return any(p.endswith(ext) for ext in SOURCE_EXTENSIONS)

La tolérance est donc par défaut, pas par liste blanche : tout untracked qui n'est pas un fichier source est toléré, y compris ce que l'allowlist UNTRACKED_ARTIFACT_TOKENS n'a jamais nommé. Un répertoire untracked (bg_logs/) ne se termine par aucune extension et passe. Un fichier à suffixe inattendu (lake_7012.log.relaunch) aussi.

git worktree remove sans --force, lui, refuse sur tout untracked non-ignoré. Les deux prédicats ne peuvent pas coïncider.

Mesure (ai-01, 2026-09-03)

Passe de retrait sur 64 worktrees : 20 retirés, 3 refusés par git, 41 refusés par l'organe.

Les deux premiers sont le défaut décrit ici. Le troisième est une limite de git indépendante (un worktree qui contient des sous-modules initialisés n'est pas retirable) — CoursIA en déclare huit (correction coursia-50 : la table de submodule-maintenance.md en nomme cinq, mais ce sont les cinq maintenus ; .gitmodules en déclare huit, les trois foundry-lib/lib/* vendorés compris, et git ne fait aucune différence entre les deux catégories au moment du retrait). Tout worktree où git submodule update --init a tourné est donc concerné, et la surface est plus large que ce que la table de maintenance laisse voir.

Aucun n'est un accident isolé : ils reviennent à chaque exécution, removable=3 en permanence, failed à chaque --apply.

Ce que le contrôle a par ailleurs trouvé (à conserver)

git status --porcelain est aveugle aux fichiers gitignorés, que le retrait emporte pourtant. Passe --ignored=matching sur les 10 candidats de cette session (merci coursia-33 pour le contrôle) :

• C:/wtprover : un .env gitignoré (5 clés d'API), plus 8 fichiers de trace prover uniques — dont HashlifeCorrectness_6c433f03a7_L2904.json, sur le lake qui porte l'essentiel de la dette formelle du dépôt.
• 3 autres : .lake/ (caches Mathlib, reconstructibles).
• Les 6 restants : uniquement __pycache__.

Le .env était reproductible (.secrets/master.env + render_envs.py), les traces prover ne l'étaient pas — elles ont été recopiées vers D:/CoursIA/.../agent_tests/ avant le retrait. Sans ce contrôle, elles disparaissaient en silence : l'organe les déclarait REMOVE et n'avait rien à signaler.

Correctif décidé

Option A — rendre is_source_dirty fail-closed. Un chemin untracked non listé dans UNTRACKED_ARTIFACT_TOKENS salit le worktree, au lieu d'être toléré par défaut faute d'extension reconnue. Les deux worktrees ci-dessus deviennent alors REFUSE reason=uncommitted_untracked:<chemin> — un verdict honnête et stable — plutôt qu'un REMOVE que git annulera.

Rejetée, option B (--force quand tous les untracked sont allowlistés) : elle contredit l'invariant 3, et la mesure ci-dessus montre pourquoi cet invariant est bon — ce sont précisément les chemins « tolérés par défaut » qui portaient les traces prover.

À joindre au même correctif :

1. Signaler les gitignorés non-cache dans le verdict (--ignored=matching, filtré des caches connus). Ne pas bloquer dessus : les afficher, pour que la décision de retrait soit prise en les voyant.
2. Détecter les worktrees à sous-modules initialisés et les classer REFUSE reason=contains_submodules plutôt que REMOVE, puisque git ne les retirera jamais.
3. Afficher la branche à côté du chemin dans le rendu de retrait (merci coursia-50) : .worktrees/ai01-14501-fix était sur docs/c890-bdh-evaluation — qui relit la liste et vérifie « 14501 » de tête contrôle le mauvais objet.

Voir #14195 (organe), #14476 / #14481 (faux positifs du verdict par contenu), #14507 / #14508 (SKIP_CURRENT inatteignable).

Pourquoi ce n'est pas un simple faux positif — le verdict est CONSTANT

removable=3 en permanence et failed à chaque --apply : ce n'est pas du
bruit, c'est la signature d'un organe éteint sur ces entrées. Un détecteur
qui rend le même verdict à chaque exécution, quoi qu'il arrive au disque, ne
mesure plus le disque — il récite. Les trois worktrees ne quittent jamais la
liste et n'ont jamais quitté le disque : la sortie a l'air vivante (elle nomme
des chemins, elle propose une action) alors que son contenu est indépendant de
l'état réel.

C'est le critère qui distingue ce défaut d'un réglage de seuil : un seuil mal
placé donne des verdicts qui changent quand l'entrée change. Ici, aucune
action de l'opérateur ne peut faire sortir ces trois entrées de REMOVE —
ni committer, ni nettoyer, puisque l'organe ne regarde pas ce qui bloque git.
Le correctif A n'améliore donc pas une précision : il rebranche le prédicat sur
la question que git pose réellement.

Corollaire de mesure, à vérifier sur le correctif : après A, le verdict de ces
trois worktrees doit changer (REMOVE -> REFUSE avec la cause nommée),
et une passe --apply doit rendre failed=0. Un correctif qui laisse
failed=3 a traité l'affichage, pas la cause.