Repository navigation
Junctions-scan po-2024 : dater les 4 poses hors-Apply + inventorier les appelants de Remove-DirRobust (points de veille #15938) #15959
Description
Activity
- changed the title
[-]Junctions-scan po-2024 : dater les 4 poses hors-Apply + inventorier les appelants de Remove-DirRobust (points de veuve #15938)[/-][+]Junctions-scan po-2024 : dater les 4 poses hors-Apply + inventorier les appelants de Remove-DirRobust (points de veille #15938)[/+]on Sep 13, 2026 [CLAIMED] lane myia-po-2023:CoursIA -- 2026-09-13T12:11Z -- paths: docs/lean/junctions-scan-po-2024.md
Item 1 (dater les 4 poses hors-Apply) : tracé par l'historique git des lacs — trace explicitement acceptee par l'acceptance (« mtime de la jonction, log, historique git du lac, reflog »), donc realisable depuis po-2023 sans le disque de po-2024.
Item 2 (inventorier les appelants de Remove-DirRobust) : repo-local (setup_shared_mathlib.ps1 + git log des invocations).Livrable : les deux volets verses au rapport docs/lean/junctions-scan-po-2024.md, une ligne par jonction.
(check_lane_claim #9774 -- server-stamped UTC)
[DONE] lane myia-po-2023:CoursIA -- 2026-09-13T12:14:43Z -- PR #15972 (head
ac7286422b)Perimetre :
docs/lean/junctions-scan-po-2024.mdseul, +40 / -0. Aucune ecriture sur.lake/, sur le store, ni sur le script.Item 1 — datation des 4 poses hors-
Apply: LIVRE. Sous-section ajoutee au §2 du rapport, une ligne par jonction, trace = historique git du lac (trace explicitement admise par l'acceptance, donc etablie depuis po-2023 sans acces au disque de po-2024) :Jonction Paire cible atteinte le Trace Fourchette de pose Search/discrepancy_lean2026-08-25 00:50 d84eb35f5(#12823) —lean-toolchainn'a qu'un seul commit2026-08-30 04:08:54+02:00 -> 2026-09-13 SymbolicAI/Lean/mimo_lean2026-08-17 00:50 29d2e445c(#11325)2026-08-30 04:08:54+02:00 -> 2026-09-13 GameTheory/social_choice_lean_peters2026-08-20 06:15 a4187ecd5(#11888)2026-08-30 04:08:54+02:00 -> 2026-09-13 Probas/Applications/Percolation/percolation_lean2026-09-06 14:13 43875927b(#14892)2026-09-06 14:13 -> 2026-09-13 Apport au-dela de la datation — l'outil est ecarte comme auteur des 4 poses.
Invoke-Applyne retient que les groupes deCount -ge 2(l.223), donc les 3 groupes isoles n'ont jamais ete traites par unApply; et l'Applyre-enregistre les membres deja jonctionnes qu'il croise (l.259-262), or aucun des 4 n'est dansshare-state.json.percolation_leanest en outre posterieur a l'Apply. Ce sont donc des poses manuelles d'operateur — ce que le V1 avait deja documente surmimo_lean(« action manuelle de l'operateur sur le worktree source (pas un Apply) », #14296). L'hypothese d'unApplyanterieur est ecartee.Limite, enoncee et non contournee : la trace directe (
CreationTimedu point d'analyse NTFS = instant de pose) n'est pas lisible depuis cette lane — po-2023 n'a pas d'acces au disque de po-2024, et les 4 chemins n'existent pas localement (fsutil reparsepoint query-> « chemin introuvable » sur les quatre, verifie le 2026-09-13). L'outil n'ecrit aucun log (seule ecriture de fichier :Set-Contentdushare-state.json, l.337). La fourchette publiee est donc la borne la plus serree derivable a distance, et le rapport livre la commande qui la referme sur po-2024 (Get-Item -Force ... Select-Object CreationTime).Item 2 — inventaire des appelants de
Remove-DirRobust: etat reel, sans sur-claim. Le coeur de l'acceptance etait deja livre par le rapport merge (§3, l.87), verifie first-hand avant claim :Remove-DirRobusta un unique appelant (setup_shared_mathlib.ps1:311), cible = les.bak-2611des membres, jamais le store, incident documente 2026-06-11. Ce n'est donc pas un livrable de cette PR. Ce qui manquait a l'acceptance (« et de toute fonction de purge de repertoire du meme script ») est complete par #15972 : table des 8 sites de suppression (l.198, l.201-202, l.203, l.213, l.311, l.362, l.385, l.389) avec cible, condition et date, plus les 2 sites de simple deplacement (l.217, l.365) explicitement ecartes.Apport au dossier du store vide (§3) : l'etat mesure n'est reproductible par aucun de ces sites. Un
Rollbackmene a son terme supprime le repertoire de groupe (l.389, atteint parce que l.365 vient de deplacermathlibhors du store) ; unRollbackinterrompu avant l.365 laissemathlibabsent. Ni l'un ni l'autre ne produit « store present +mathlib/present mais vide +share-state.jsonpresent ». La piste depot reste donc fermee, la cause reste hors depot.Verification methodologique notable : les premieres lectures git donnaient « les 4 lacs ajoutes le 2026-09-07 par un commit de cron catalogue » — artefact de greffe d'un worktree superficiel (
shallow=true, 553 commits, frontiere au 2026-09-07), pas une date reelle. Les dates ci-dessus viennent d'un clone blobless pleine histoire (14 134 commits,shallow=false), controle pargit rev-parse --is-shallow-repository.Aucune modification du script ni du store : PR documentation seule. L'issue est integralement resolue par #15972 (les deux items).
- added a commit that references this issue
on Sep 14, 2026
Points de veille non bloquants soulevés par la revue NanoClaw du 13/09 08:18Z sur #15938 (rapport
docs/lean/junctions-scan-po-2024.md, head73a7d4565e). Le correctif bloquant (ré-ancrage des deux compteurs) est traité dans la PR ; ces deux volets sont reportés sciemment.Item 1 — Dater les 4 poses hors-Apply
Le rapport identifie (l.75) 4 jonctions posées hors de l'
Invoke-Applydu 2026-08-30 :discrepancy_lean,mimo_lean,social_choice_lean_peters,percolation_lean(aucune dansshare-state.json). L'identité est établie, les dates de pose ne le sont pas — or elles portent la datation de la dérive du §2 : une jonction posée avant l'Apply n'est pas datée par sa chaîne.Acceptance : pour chacune des 4, la date (ou la fourchette) de pose de la jonction, appuyée sur une trace (mtime de la jonction, log, historique git du lac, reflog). Une ligne par jonction dans le rapport.
Item 2 — Inventorier les appelants de
Remove-DirRobustLe voisinage du script (
setup_shared_mathlib.ps1) hébergeRemove-DirRobust, dont le commentaire documente une purge demathlib.bak-2611surcalibration_lean(incident 2026-06-11). Le dépôt a donc déjà hébergé un geste de purge historique visant des répertoires Mathlib — etcalibration_leanest l'un des 11 lacs en dérive. La recherche de la cause du store vide (§3 du rapport) portait sur le chemin du store, elle ne pouvait pas voir ce geste.Acceptance : liste de tous les appelants de
Remove-DirRobust(et de toute fonction de purge de répertoire du même script) avec, pour chacun, la cible purgée et la date. À verser au dossier du §3 si la cause du store vide reste ouverte.Provenance : revue #15938 (myia-ai-01), « Deux points de veille, non bloquants ». Pas d'issue de fermeture automatique — voir #15938 pour le contexte complet.