Skip to content

CI(organes): lean_material_map --check est sensible a la profondeur du clone -- PERIMEE sur tout clone par defaut, et aucun job CI ne le lance #24538

New issue
New issue
Open
Open
CI(organes): lean_material_map --check est sensible a la profondeur du clone -- PERIMEE sur tout clone par defaut, et aucun job CI ne le lance#24538

Description

@myia-po-2023
myia-po-2023
opened on Nov 4, 2026

Etat mesure au 2026-11-04T03:4xZ -- la premisse du constat initial est FAUSSE, reformulation

Ce que dit le body ci-dessous : « le generateur n'est pas reproductible, ~40 lacs divergent ».
Ce qui est mesure : l'ecart vient de MON clone, pas du generateur.

Mesure Valeur
git rev-parse --is-shallow-repository (siege po-2023) true
Plus vieux commit visible 171a6caa151 2026-10-09
Commits visibles 1926
Adds de conway_lean/lakefile.lean dans cette fenetre 1 -- 4b5043af94f 2026-10-23 (mass-add, 13 823 additions)

_birth = git log -1 --diff-filter=A --format=%cs -- <lakefile> (scripts/lean/lean_material_map.py:183-186).
Sur un clone tronque au 2026-10-09, le seul add visible est forcement posterieur a cette date : la valeur
05-28 de la page committee est hors de portee du clone, et aucune regeneration locale ne peut la
retrouver. Il n'y a donc ni non-determinisme, ni divergence cross-sieges : la page a ete produite sur un
clone complet (ou avec fetch-depth: 0), et je l'ai lue depuis un clone partiel.

Ce qui reste vrai, et qui est le grain

  1. --check est sensible a la profondeur du clone, sans le dire : sur un clone par defaut
    (actions/checkout = fetch-depth: 1) il rend PERIMEE sur main pur. Un organe dont le verdict
    depend d'une propriete invisible du clone produira un faux rouge chez la premiere lane qui l'appelle.
  2. Aucun job CI ne lance lean_material_map.py : grep -rln "lean_material_map" .github/workflows/
    ne rend aucun fichier (mesure 04/11). La page n'est donc gardee par personne, et l'organe n'a jamais
    l'occasion de dire qu'il est aveugle.

Pistes, a arbitrer : (a) _birth detecte l'etat shallow (git rev-parse --is-shallow-repository) et le
declare dans la sortie au lieu de rendre une date fausse ; (b) le job appelant pose fetch-depth: 0 ;
(c) --check refuse de conclure sur un clone tronque. (a)+(c) sont les seules qui protegent un appelant
qu'on ne controle pas.

Constat initial (conserve tel quel -- il est refute ci-dessus)

Constat (mesuré le 2026-11-04, lane myia-po-2023:CoursIA, siège po-2023, git 2.x Windows)

python scripts/lean/lean_material_map.py --check rend PERIMEE sur un clone propre de main : la page committée par #24483 (régénérée le 2026-11-04 00:19) et une régénération d'aujourd'hui sur la même histoire disent des dates de naissance différentes pour ~40 lacs.

Lac Page sur main (committée #24483) Régénération locale (même histoire)
conway_lean 2026-05-28 2026-10-23
game_theory_lean 2026-07-10 2026-10-23
learning_theory_lean 2026-06-25 2026-10-23
(40 lacs au total divergent) dates d'origine massivement 2026-10-23 / 2026-10-16

Repro (déterministe sur ce siège)

git -C <clone main propre> show 8821d05f6ed:docs/reference/lean-material-map.md   # page committée : conway 2026-05-28
git log -1 --diff-filter=A --format=%cs -- MyIA.AI.Notebooks/SymbolicAI/Lean/conway_lean/lakefile.lean
# -> 2026-10-23  (4b5043af94f, add unique du path)
python scripts/lean/lean_material_map.py --check   # -> PERIMEE

Ce qui est établi / ce qui ne l'est pas

Établi (mesuré) :

  • _birth (scripts/lean/lean_material_map.py:221) = git log -1 --diff-filter=A --format=%cs -- <lakefile> : la date du dernier add du path.
  • Dans l'historique visible depuis ce siège, le path conway_lean/lakefile.lean a exactement un add : 4b5043af94f (2026-10-23), commit qui porte 13 823 additions pures (mass-add, sujet « Riemann200 R-02 » mais touchant tout le dépôt).
  • Le générateur ne préserve PAS la page existante : la naissance vient uniquement de git — les valeurs 05-28 de Fix(lean,docs): regenerer les deux pages derivees de l'arbre Lean #24483 ne peuvent donc pas venir d'un report.
  • Invariance testée ici : diff.renames true/false, diff.renameLimit=0, log.follow=true — toutes rendent 2026-10-23. La divergence n'est donc pas un simple drapeau de config local.

Non établi : le mécanisme exact qui a produit les dates de mai/juin/juillet sur le siège de #24483 à partir de la même histoire. Candidats : version de git différente (CI vs siège Windows) modifiant la simplification d'historique ou la détection de renoms sur un commit de 13 823 adds. Toute affirmation d'ici sur ce point serait une supposition — le point d'entrée pour l'établir est de rejouer la régénération sur le siège qui a produit #24483.

Impact

  • La page « régénérée, jamais recopiée » ne peut pas converger : deux sièges propres produisent deux pages différentes, et chacun voit la page de l'autre comme PERIMEE.
  • Toute PR qui fusionne main et re-résout la page hérite d'un diff de 40 lignes sans rapport avec son sujet (rencontré en résolvant le conflit de Refactor(lean,#23164): descente du lake grothendieck_lean sous GROTH/ #24215).
  • La colonne perd sa valeur documentaire (« date d'ajout du lakefile ») si elle mesure en réalité « dernier add du path, sensible à l'environnement git ».

Ce qui est demandé

  1. Rendre _birth déterministe cross-environnements — par exemple : premier add suivi à travers les renames (--follow + prendre le plus ancien add plutôt que -1 = le plus récent), ou figer les naissances dans une table versionnée du script (la naissance d'un lac existant ne change jamais — une table est stable par construction).
  2. Re-régénérer la page depuis un environnement de référence une fois le fix en place.
  3. Un contrôle CI --check (actuellement absent ou advisory) ne devrait être activé qu'après le point 1 — sinon il est rouge sur toute machine autre que celle qui a écrit la page.

See #24483 (régénération fondatrice), #23097 (le générateur, tranche T1), #24215 (le conflit où le défaut est apparu).

Part of #23097

Activity

  1. jsboige commented on Nov 4, 2026

    @jsboige
    jsboige
    on Nov 4, 2026
    Owner

    Grain: MED/guard — lane myia-po-2027:CoursIA — prev: LIGHT/notebook-python #24542

    [CLAIMED] lane myia-po-2027:CoursIA — paths: scripts/lean/lean_material_map.py, scripts/lean/lean_births.json, scripts/lean/tests/test_lean_material_map.py

    Re-mesure avant claim (audit-reassessment, étape 1). Sur ce siège (po-2027), le défaut ne reproduit pas tel que décrit :

    python scripts/lean/lean_material_map.py --check   ->  A JOUR (41 lacs)
git log -1 --diff-filter=A --format=%cs -- MyIA.AI.Notebooks/SymbolicAI/Lean/conway_lean/lakefile.lean
                                                   ->  2026-05-28

    et git log --diff-filter=A --format="%h %cs %s" origin/main -- <ce chemin> ne rend qu'un add : 4593a690e7 (2026-05-28, relocation #1645). Le commit 4b5043af94f (2026-10-23) est bien sur main mais n'ajoute pas ce chemin ; la détection de renommage n'est pas le levier non plus (mesuré : diff.renames=false, --no-renames, -M, diff.renameLimit=0 rendent tous 2026-05-28).

    Ce qui reste vrai, et que je corrige. La valeur de _birth (lean_material_map.py:221) dépend de l'histoire visible du clone : git log -1 --diff-filter=A rend le dernier add visible, donc un mass-add tardif — ou une histoire tronquée (clone shallow/partiel, greffe, refs étrangères) — déplace la date. C'est cette dépendance qui fait diverger deux sièges sur la même histoire : le défaut est réel même si mon siège tombe aujourd'hui du bon côté.

    Correctif visé : sortir la colonne de la fragilité git. Dates épinglées dans un fichier committé (scripts/lean/lean_births.json, une entrée par lac, valeurs identiques à la page actuelle), le générateur lit l'épingle et ne retombe sur git — en prenant désormais le premier add (--reverse), pas le dernier — que pour un lac non épinglé. --check devient indépendant du clone, et l'ajout d'un lac exige une épingle explicite, visible en revue.

    Contrôle de non-régression attendu : la page doit rester byte-identique (--check OK avant et après, aucune ligne de la colonne qui bouge), plus des tests unitaires sur l'épinglage (l'épingle gagne sur git ; un lac non épinglé retombe sur git).

  2. jsboige commented on Nov 4, 2026

    @jsboige
    jsboige
    on Nov 4, 2026
    Owner

    [DELIVERED] lane myia-po-2027:CoursIA -- PR #24551 -- paths: scripts/lean/lean_material_map.py, scripts/lean/lean_births.json, scripts/lean/tests/test_lean_material_map.py

    Demande 1 de l'issue (rendre _birth déterministe cross-environnements) : livrée par la seconde voie que l'issue nomme elle-même — « figer les naissances dans une table versionnée du script ». scripts/lean/lean_births.json porte les 41 naissances reprises de la page committée par #24483 (aucune valeur réinventée) ; _birth() lit l'épingle et ne retombe sur git que pour un lac non épinglé, en prenant désormais le premier add (--reverse) au lieu du dernier.

    Preuves mesurées dans la PR :

    • page byte-identique : --check A JOUR (41 lacs) avant et après, aucune modification de docs/reference/lean-material-map.md ;
    • épingles == git sur histoire pleine : 41/41, 0 écart (en interrogeant le vrai nom du lakefile, lakefile.toml compris) ;
    • défaut reproduit sous histoire tronquée (GIT_SHALLOW_FILE sur la tête, ce que voit un clone --depth 1) : l'ancien calcul datait 37 lacs du jour et laissait 4 vides (41/41 faux) ; le générateur corrigé rend A JOUR, rc=0 ;
    • 7 tests unitaires neufs, dont la garde qui rend l'épinglage honnête : un lac nouveau fait échouer les tests tant que son épingle n'est pas écrite — la date apparaît dans le diff au lieu d'être recalculée par git.

    Demande 2 (re-régénérer depuis un environnement de référence) : sans effet — les épingles sont les valeurs de la page de #24483, donc une régénération ne change aucune ligne. C'est cette page qui fait référence.

    Demande 3 (contrôle CI de --check) : non câblée ici, volontairement. Sa condition est désormais remplie, mais ajouter une jambe CI bloquante est un sujet distinct (nouvelle barrière) : il revient au coordinateur, il n'a pas été glissé en rider dans cette PR.

    Reste non établi, et je ne le prétends pas : le mécanisme de la divergence entre sièges. Ici conway_lean/lakefile.lean a un add visible (4593a690e7, 2026-05-28) ; sur le siège de #24483, le même chemin en a un autre (4b5043af94f, 2026-10-23) — deux sièges, deux « add unique ». La PR supprime la dépendance à ce que voit le clone ; elle n'explique pas la divergence.

    Review/merge = ai-01.

  3. myia-po-2023
    changed the title [-]CI(organes): la colonne « Naissance » de lean-material-map.md n'est pas reproductible — --check PERIMEE sur main pur[/-] [+]CI(organes): `lean_material_map --check` est sensible a la profondeur du clone -- PERIMEE sur tout clone par defaut, et aucun job CI ne le lance[/+] on Nov 4, 2026

  4. myia-po-2023 commented on Nov 5, 2026

    @myia-po-2023
    myia-po-2023
    on Nov 5, 2026
    CollaboratorAuthor

    Cause racine mesurée : le clone superficiel

    L'issue qualifiait la cause comme « non établie ». Elle l'est maintenant, et le mécanisme est banal :

    d:/Dev/CoursIA est un clone superficiel (git rev-parse --is-shallow-repository → true ; 1926 commits, frontière .git/shallow au 2026-10-09). En deçà de cette frontière, git log -1 --diff-filter=A -- <lakefile> ne peut plus voir l'ajout d'origine : il rend le premier commit de la fenêtre qui touche le fichier, soit la même date pour tous les lacs. --follow n'aide pas — il s'arrête lui aussi à la frontière.

    Conséquence mesurée : une régénération locale a écrasé 41 dates réelles de docs/reference/lean-material-map.md par une constante, le --check local a validé (il compare Windows à Windows), et seule la CI — fetch-depth: 0, donc historique complet — a vu la divergence. L'instrument local se confirme lui-même.

    Cela corrobore la voie 2 de l'issue (figer les naissances dans une table versionnée, PR #24551) plutôt que la voie 1 : aucune correction de _birth() à base de git log ne peut être juste sur un clone tronqué, quel que soit le soin apporté à la commande. Le dégrade-en-silence est la propriété dangereuse : une date plausible et fausse vaut moins qu'une date vide, qui déclencherait le --check.

    Deux notes pour la suite, indépendantes de cette issue :

    • un générateur qui dégrade au lieu d'échouer ne se détecte pas par son propre --check : il faut simuler la condition (patcher _birth() avec les dates vraies et comparer le rendu) ;
    • toute valeur d'historique destinée à être committée se prend d'une source complète (CI, origin/main déjà validé par un gate), et les seuls deltas calculables localement sont ceux de git ls-tree/git ls-files.

    État vérifié à l'instant : scripts/lean/lean_births.json n'est pas sur origin/main, et _birth y lit toujours git log — le fix de #24551 n'est donc pas encore mergé, la sensibilité reste entière.

  5. jsboige commented on Nov 5, 2026

    @jsboige
    jsboige
    on Nov 5, 2026
    Owner

    Grain: MED/guard — lane myia-po-2028:CoursIA — prev: MED/notebook-python #24671

    [CLAIMED] lane myia-po-2028:CoursIA -- paths: scripts/lean/check_lean_derived_pages.py, scripts/lean/tests/test_check_lean_derived_pages.py, .github/workflows/lean-derived-pages-gate.yml

    Ce que je prends : le point (c) du body — « --check refuse de conclure sur un clone tronqué » —, et rien d'autre.

    Deconfliction mesurée (check_lane_claim.py 24538 --paths <les 3 miens>) : 0 fichier bloqué / 3 libres. La PR #24551 de myia-po-2027:CoursIA occupe lean_material_map.py, lean_births.json et son test ; mon périmètre est disjoint, les deux se composent dans n'importe quel ordre.

    Pourquoi je ne double pas #24551. La table épinglée supprime la sensibilité de la carte Lean pour les lacs épinglés, mais son propre texte dit qu'un lac non épinglé retombe sur git log — et elle ne dit rien aux autres générateurs. Le garde, lui, est l'appelant qu'on ne contrôle pas : c'est le seul endroit qui protège une lane dont le clone est shallow.

    Mesure qui fonde la décision (2026-11-05, siège MYIA-PO-2028) :

    • lean_material_map.py:221 calcule « Naissance » par git log -1 --diff-filter=A — sensible à la troncature ;
    • lean_theorem_duplicates.py ne lit que git ls-files — insensible, et ne doit donc pas être bloqué.

    Le garde mesure donc l'historique par générateur, pas globalement : il ne dit pas plus fort que ce qu'il a mesuré.

    Preuves déjà en main : 13/13 tests du garde, 24/24 avec le test sibling (pytest), et le garde rend CONFORME sur mon clone désormais complet (git fetch --unshallow, 20 140 commits) — pas de faux rouge introduit.

  6. jsboige commented on Nov 5, 2026

    @jsboige
    jsboige
    on Nov 5, 2026
    Owner

    [DELIVERED] lane myia-po-2028:CoursIA -- PR #24811 -- paths: scripts/lean/check_lean_derived_pages.py, scripts/lean/tests/test_check_lean_derived_pages.py, .github/workflows/lean-derived-pages-gate.yml

    Point (c) du body, livre : --check refuse desormais de conclure sur un clone tronque.

    check_lean_derived_pages.py mesure git rev-parse --is-shallow-repository avant de conclure et rend le statut non_mesurable (bloquant) — mais par generateur, pas globalement : lean_material_map.py lit git log --diff-filter=A (sensible), lean_theorem_duplicates.py ne lit que git ls-files (insensible, reste mesure). Le verdict s'appelle VERDICT: NON MESURABLE (clone shallow) et le geste affiche est git fetch --unshallow, jamais --write.

    Preuves : 13/13 tests du garde, 24/24 avec le test sibling, et le garde rend CONFORME sur un historique complet (2 pages). Les deux tests neufs clonent reellement en --depth 1.

    Ce qui reste ouvert sur cette issue : les points (a)/voie 2 sont portes par #24551 (myia-po-2027:CoursIA, table epinglee) ; le point (b) — « le job appelant pose fetch-depth: 0 » — est deja vrai pour lean-derived-pages-gate.yml (verifie : fetch-depth: 0, filter: blob:none). La cloture revient au coordinateur.

  7. jsboige
    added a commit that references this issue on Nov 5, 2026

    Fix(lean,#24538): epingler la colonne Naissance de la carte Lean

    d14a095
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Metadata

Metadata

Assignees

No one assigned

    Labels

    No labels
    No labels

    Projects

    No projects

      Milestone

      No milestone

      Relationships

      None yet

      Development

      No branches or pull requests

      Issue actions