[infra][lean] setup_shared_mathlib.ps1 : valider un cache existant avant jonction + isoler git du repo parent #18584

Grain: MED/tooling — lane myia-po-2024:CoursIA — prev: DEEP/qc #18582

Constat (Apply po-2024, 30/09, issue #13962)

L'Apply -Group db584cd6 -Build a échoué sur tous les membres (rollback auto partout — état final intact, vérifié) pour deux causes chaînées :

1. Cache pré-existant vide non validé : .mathlib-cache/leanprover_lean4_v4.33.0-db584cd6/mathlib/ existait depuis le 25/09 vide (reste d'une tentative précédente). Le script l'a réutilisé tel quel : jonctions créées vers un dossier vide, aucune copie du donneur.
2. lake build tente un clone/checkout dans le path jonctionné ; sans .git dans le cache, git remonte au repo parent CoursIA (remote jsboige/CoursIA) et tente d'y appliquer un checkout — refusé uniquement par les modifications locales de l'arbre partagé (M .vscode/settings.json, M Z3.Linq). Le WIP d'une session tierze a involontairement protégé le repo principal. Sur un arbre propre, le comportement serait une mutation du repo parent par un chemin non prévu.

Fixes demandés

• Apply : si .mathlib-cache/<groupe>/mathlib existe, valider qu'il est non vide ET porte un .git (révision = mathlibRev du groupe) avant de jonctionner le moindre membre ; sinon le repeupler depuis le donneur ou échouer avant toute jonction.
• Isolation git : avant tout lake build/commande de vérification dans un membre jonctionné, vérifier que <membre>/.lake/packages/mathlib/.git existe ; un path sans .git ne doit JAMAIS laisser git opérer sur le repo parent.
• Nettoyage : les restes vides (.mathlib-cache/<groupe>/mathlib vide) d'une tentative échouée devraient être retirés par le rollback, pas laissés pour empoisonner la tentative suivante.

Reproduction

pwsh scripts/lean/setup_shared_mathlib.ps1 -Mode Apply -Group db584cd6 -Build sur un arbre où .mathlib-cache/leanprover_lean4_v4.33.0-db584cd6/mathlib/ est vide : chaque membre échoue avec info: mathlib: URL has changed puis error: Your local changes to the following files would be overwritten by checkout: .vscode/settings.json (message du repo parent, pas de mathlib).

See #13962 (application), #2611 (outillage d'origine).

🤖 Generated with Claude Code