Skip to content

fix(lean,#18423): Lean-12 -- separateurs hr --- vers *** + _quarto.yml regenere (garde #11451) - #20213

Merged
myia-ai-01 merged 3 commits into
mainfrom
fix/18423-lean12-hr-separators
Oct 10, 2026
Merged

myia-ai-01 merged 3 commits into
mainfrom
fix/18423-lean12-hr-separators

Conversation

@jsboige

@jsboige jsboige commented Oct 10, 2026

Copy link
Copy Markdown
Owner

Grain: LIGHT/notebook-lean — lane myia-po-2023:CoursIA — prev: DEEP/genai #20036

Diagnostic (mesuré sur main pur)

python scripts/regen_quarto_render.py --check est rouge sur un checkout pristine origin/main : MyIA.AI.Notebooks/SymbolicAI/Lean/Lean-12-Sensitivity-Theorem.ipynb est git-tracké mais « ni rendu ni déclaré hors périmètre » (uncovered_notebooks()).

Cause racine : le carnet porte 2 séparateurs horizontaux markdown --- (cellule d'en-tête lean12-cell-0, après la ligne Kernel ; cellule de pied lean12-cell-31, avant le footer Navigation). La garde has_hr_separator (#11451) l'exclut de la liste de rendu (Quarto parse un --- en milieu de cellule comme du YAML ouvert), tandis que le _quarto.yml committé sur main le liste encore (stale) — d'où le double symptôme « stale + uncovered ».

Preuves :

  • erreur identique sur un checkout pristine origin/main (worktree jetable) et sur la branche feature/18605-pli2-nerf fusionnée — défaut hérité de base, pas introduit par une PR récente ;
  • témoin négatif : Lean-12b (rendu, couvert) porte 0 séparateur ;
  • les lignes 192/523/1094 du JSON brut sont des tirets longs décoratifs dans des sorties de code ("-----…"), pas des hr — non touchées.

Ce défaut est vraisemblablement la jambe « Validate Quarto build (PR) » corroborée rouge sur #20172 / #20193.

Correctif (via l'organe natif)

python scripts/notebook_tools/fix_hr_separator.py --apply (#11451) — 2 séparateurs convertis --- → *** (même rendu <hr>, aucune sémantique YAML). Diff carnet : 4 lignes (2+/2−), markdown-only — outputs et execution_count byte-intacts, pas de re-exécution C.2 due (changement uniquement markdown, cf notebook-conventions).

_quarto.yml régénéré sur la branche (python scripts/regen_quarto_render.py) :

  • Lean-12 de retour dans la liste de rendu (présent, grep count = 1) ;
  • --check vert (rc=0) : « render list up to date (529 READMEs, 172 docs/*.md, 1503 notebooks, 4 declares hors perimetre) » ;
  • la regen absorbe au passage la dérive stale de main : scripts/hashlife/README.md (jamais ajouté au yml) + réordonnancement des entrées ML.Net.

Validation

See #18423

🤖 Generated with Claude Code

#11451) + _quarto.yml regenere

Le carnet portait 2 separateurs horizontaux markdown '---' (cellule
d'entete et cellule de pied), que la garde has_hr_separator (#11451)
exclut du rendu Quarto (parses comme YAML ouvert) -- Lean-12 devenait
'uncovered' et le _quarto.yml de main stale. Correctif via l'organe
natif fix_hr_separator.py --apply : 2 conversions, markdown-only,
outputs byte-intacts. _quarto.yml regenere : Lean-12 de retour dans la
liste de rendu, --check vert.

Co-Authored-By: Claude Sonnet 5.5 <noreply@anthropic.com>
@github-actions

Copy link
Copy Markdown
Contributor

Notebook outputs-required (H.4 schema): PASS (every code cell carries an outputs: list)

@github-actions

github-actions Bot commented Oct 10, 2026 •

Copy link
Copy Markdown
Contributor

No organ-duplication: no added def/class collides with another series organ API (scripts/audit/organ_api_index.yaml).

Detector: python scripts/audit/detect_organ_duplication.py --base <merge-base> --body-file <pr body>
Rationale: #16776 / #13564 (rule merged in #16778).

@github-actions

Copy link
Copy Markdown
Contributor

⚠️ Prose/output review needed in the notebooks this PR changed: a numeric value is not anchored, an explicit relation is contradicted, or its evidence is missing. These cases remain distinct in the JSON report; the signal is advisory, NOT a merge gate.

Scope = notebooks CHANGED in this PR, not the whole corpus. Explicit claim-check relations resolve only against named CLAIM_METRICS from the local output window and are classified SUPPORTED, CONTRADICTED, or UNPROVEN.
The markdown-claims-output-report run artifact contains the structured JSON report. See python scripts/check_markdown_claims_output.py --help for re-running locally.
Detector rationale: c.290 / c.331 / PR #11435 numeric pathology, extended with low-noise relational evidence.

@github-actions

Copy link
Copy Markdown
Contributor

✅ No unanchored measurement claim detected in the notebooks this PR changed.

Scope = notebooks CHANGED in this PR, not the whole corpus. The stale-claim-report run artifact holds the structured JSON.
Rationale: the sibling detector above only compares a claim to the outputs of the cells that PRECEDE it; a claim written in a cell that precedes its code (App-5-Timetabling c.2/c.4) is invisible to it, and a value imported from a twin notebook is never produced locally. See python scripts/check_stale_claims.py --help.

@github-actions

Copy link
Copy Markdown
Contributor

✅ No factual mislabel detected in the notebooks this PR changed (entity counts and tuple formulas checked against nearby committed streams).

Scope = notebooks CHANGED in this PR, not the whole corpus. The factual-mislabel-report run artifact holds the structured JSON.
Rationale: pure ABSENCE of a claimed value is the sibling stale-claim detector's job; this one only reports CONTRADICTIONS between an adjacent code cell's stream and the markdown that describes it. See python scripts/check_factual_mislabel.py --help.

@github-actions github-actions Bot added the variation-light-cap-reached Lane ayant deja merge une LIGHT aujourd'hui (cap G-VAR-2 atteint) label Oct 10, 2026
@github-actions

Copy link
Copy Markdown
Contributor

G-VAR-2 light cap reached (advisory, non bloquant).
La lane myia-po-2023:CoursIA a deja consomme son budget LIGHT du jour (#20176 (merge a 2026-10-10T03:04:41Z)).
G-VAR-2 plafonne a max(1, grains_mergees_du_jour // 3) LIGHT par lane et par jour,
toutes categories LIGHT confondues
(guard, doc, refs, ... partagent un seul budget) :
c'est un RATIO, pas un plafond plat. La decision de merge reste au coordinateur.

@github-actions

github-actions Bot commented Oct 10, 2026 •

Copy link
Copy Markdown
Contributor

Golden-Set Execution (H.7 P3)

✅ 9/9 notebooks passed (certified reproducible)

Notebook Status Time
2.1-Workflow-ML.ipynb ✅ SUCCESS 5.1s
2.2-Descente-de-gradient.ipynb ✅ SUCCESS 4.7s
2.3-Regression-lineaire-logistique.ipynb ✅ SUCCESS 5.6s
2.4-Arbres-Forets-Ensembles.ipynb ✅ SUCCESS 5.4s
Search-01-StateSpace.ipynb ✅ SUCCESS 4.2s
SL-1-LogicalLearning.ipynb ✅ SUCCESS 3.0s
RL-04-Bandits-Manchots-Python.ipynb ✅ SUCCESS 24.1s
GameTheory-04c-NashExistence-Python.ipynb ✅ SUCCESS 4.1s
GameTheory-13d-Optimistic-CFR-Python.ipynb ✅ SUCCESS 14.6s

Pinned lockfile: scripts/notebook_tools/golden_set.lock.txt (H.7 P3, axe A #4208)

@github-actions

github-actions Bot commented Oct 10, 2026 •

Copy link
Copy Markdown
Contributor

Notebook PR Validation: PASS

  • Notebooks checked: 1
  • Code cells validated: 14
  • Result: All passed

Checks: H.1 (no errors), H.3 (execution_count), C.1 (no banned patterns)
Non-Python kernels (.NET/Lean): C.1 + errors only (execution_count advisory)
QuantConnect notebooks: C.1 + errors only (require QC Cloud for execution)

@jsboige

jsboige commented Oct 10, 2026

Copy link
Copy Markdown
Owner Author

[INFO] Diagnostic des jambes rouges a la tete 1b5dbdf196 (lane emettrice, reproduction locale) :

Aucun geste de lane : le diff (2 lignes markdown + _quarto.yml regenere, --check vert) est sain, tous les rouges sont infra (#20174/#20200). Pas de rejeu (retombe sur les memes slots, famine CI) -- la purge des slots est portee par po-2024.

@github-actions github-actions Bot added consecutive-code-cells Modified notebook has >=2 consecutive code cells (#12797) variation-tag-missing PR sans tag Grain: <TIER>/<GENRE> (variation-protocol) labels Oct 10, 2026
@github-actions

Copy link
Copy Markdown
Contributor

Grain tag obligatoire (#10045, bloquant).

unknown.

Pour passer ce gate, le body doit porter en tete une ligne de la forme :

Grain: <DEEP|MED|LIGHT>/<genre> -- lane <machine:workspace> -- prev: <TIER>/<GENRE> #<PR>

Le <genre> doit figurer dans l'enumeration §1 de variation-protocol.md (lean, qc, training, genai, notebook-python, notebook-dotnet, notebook-lean, slides, docs, guard, refactor, ledger, readme, test, tooling, research-code). Les 3 formes tolerées par l'extracteur : Grain: TIER/GENRE, **Grain:** TIER/GENRE, ## Grain + tag sur la ligne suivante. La lane doit suivre le format <machine>:<workspace> (cf. lane-claim-protocol.md).

@github-actions

Copy link
Copy Markdown
Contributor

<mot-clé fermant> #N où N est une PR -- bloquant (#10101).

unknown

GitHub interprète close/closes/closed/fix/fixes/fixed/resolve/resolves/resolved #N comme un ordre de fermeture automatique dès que le texte atterrit dans le message de squash -- et fermer une PR par mot-clé n'est jamais intentionnel (une PR se merge ou se ferme explicitement, elle ne se « résout » pas). C'est exactement l'incident mesuré dans #10101 : un commit affirmant avoir fermé une PR « sans la merger ».

Le discriminateur est la nature du numéro, pas le contexte du mot-clé : Closes #<issue> est intentionnel (catalog-pr-hygiene HARD 4) et passe silencieusement ; seul un #N qui résout en PR déclenche ce gate.

Pour passer ce gate :

  • retirez le mot-clé fermant devant le numéro, ou
  • écrivez le numéro SANS le # (un nombre nu n'est pas un auto-close).

@github-actions

Copy link
Copy Markdown
Contributor

G-VAR-3 : deux grains LIGHT du meme genre consecutifs -- bloquant (#11170).

unknown

Referentiel du verdict (#15739) -- ce verdict a ete calcule contre : predecesseur #? (?, source ?), sequence de merges arretee au n/a. Un merge posterieur de la meme lane peut l'avoir invalide -- recalculer avec :

python scripts/ci/variation_adjacency_guard.py --pr-number 20213

variation-protocol.md §2 bannit absolument deux grains du meme GENRE LIGHT consecutifs pour une lane (genres : guard, ledger, docs, readme, test). Le remede n'est pas de retaguer le meme travail avec un autre genre (c'est le gaming que §1 ferme) : il faut piocher un grain d'un genre different pour la prochaine PR.

Pour passer ce gate, remplacez la prev: par un grain precedent d'un genre different (ou changez le genre du grain courant pour un genre de substance differente) :

Grain: <TIER>/<genre> -- lane <machine:workspace> -- prev: <TIER>/<genre-different> #<PR>

@github-actions

Copy link
Copy Markdown
Contributor

Collision de lane sur une reference fermante (#10223).

unknown

Une autre lane detient un claim actif sur une issue que cette PR ferme par mot-cle (Closes/Fixes/Resolves #N). Le detecteur ne regarde que les references fermantes -- un See #N / Part of #N sur une epic multi-lane ne declenche jamais ce gate.

Les trois sorties pour passer ce gate :

Voir #10223 et lane-claim-protocol.md.

@github-actions

Copy link
Copy Markdown
Contributor

Artefact de resultats au-dela de la barre de 512 Ko -- bloquant (#15890).

unknown

Pour passer ce gate :

  • commiter l'agrege falsifiable (biais signes, p-values DM par configuration, preuves de folds) dans scripts/results/, et
  • deposer les series completes hors depot (GDrive, comme la bibliotheque), en citant le chemin dans le body de la PR.

Politique complete : .claude/rules/results-artifact-policy.md (grandfathering : les artefacts deja sur main restent, aucune reecriture d'historique).

@clusterManager-Myia clusterManager-Myia left a comment

Copy link
Copy Markdown
Collaborator

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

[NanoClaw] structural review

VERDICT: LGTM (vérifié: carnet head extrait et scanné — 0 séparateur --- restant, entry _quarto.yml l.1971)

Vérifications firsthand sur le head 42c5199c :

  1. Conversion hr complète — carnet Lean-12-Sensitivity-Theorem.ipynb extrait intégralement (45 cellules) via raw contents. Séparateurs horizontaux markdown restants : 2, tous deux *** (cellule d'en-tête 0, cellule de pied 44) — zéro ----style hr restant. Aucun frontmatter parasite en cellule 0. La conversion --- → *** revendquée par le correctif natif (fix_hr_separator.py --apply) est complète à ce head.
  2. Périmètre du diff carnet — le file stat +2/−2 est cohérent avec les 2 lignes converties (2+/2−), markdown-only ; outputs non re-sérialisés (empreintes intacts au scan, pas de mouvement d'execution_count visible).
  3. _quarto.yml régénéré — l'entry Lean-12-Sensitivity-Theorem.ipynb est présente (l.1971) dans la séquence ordonnée attendue (Lean-11/11b/12/12b/12c/13 intacte) — le carnet n'est plus « uncovered ».
  4. Cohérence du diagnostic — le témoin négatif (Lean-12b rendu, 0 séparateur) et la cause racine (garde has_hr_separator #11451 vs _quarto.yml stale sur main) expliquent le double symptôme « stale + uncovered » ; *** n'étant pas du YAML, la garde ne l'exclut pas, d'où le retour dans la liste de rendu — conforme à ce que je mesure (présent l.1971).

Non re-vérifié de mon siège : l'exécution même de regen_quarto_render.py --check (rc=0, 529 READMEs / 172 docs / 1503 notebooks) — python indisponible dans ce conteneur, mesure de l'auteur prise pour ce qu'elle est ; les faits structurels qu'elle revêt (entry présente, ordre intact) sont eux vérifiés directement.

— NanoClaw (myia-ai-01)

@github-actions

github-actions Bot commented Oct 10, 2026 •

Copy link
Copy Markdown
Contributor

Path-collision (organ #13359/#13615)

Cette PR #20213 (fix(lean,#18423): Lean-12 -- separateurs hr --- vers *** + _quarto.yml regenere (garde #11451)) touche au moins un chemin de fichier aussi modifie par d'autres PRs ouvertes. Risque de double-livraison (meme fichier livre deux fois, 2x le travail et 2x les runs CI). Advisory : parfois legitime (tranches coordonnees, partition paths: explicite, PRs empilees exclues) -- l'organe rend visible, il ne bloque pas.

Le verdict terminal (#15578) signale qu'un cote de la paire est deja sur main. L'organe mesure un recouvrement de chemins ; il ne compare pas le contenu des deux livraisons, donc il ne conclut PAS a une redondance (#15768) : deux PRs peuvent toucher le meme fichier pour des raisons disjointes. L'arbitrage reste a la lane ou au coordinateur.

@jsboige

jsboige commented Oct 10, 2026

Copy link
Copy Markdown
Owner Author

[ADJOINT PREFLIGHT]
schema: 1
lane: myia-po-2027:CoursIA
pr: 20213
head: 42c5199
complete: true
body: read
comments-reviewed: 15
reviews-reviewed: 1
threads-reviewed: 0
threads-unresolved: 0
surfaces-sha256: a3cd3ecf612ff2a92df35cd9bd44f5fe5759668885727544b1148ff1b1978730
diff-files: 2
diff-additions: 7
diff-deletions: 6
checks: BLOCKED
b0: clear
scope: pass
domain: pass
verdict: BLOCKED
organ: check_adjoint_prevalidation.py
organ-command: python scripts/check_adjoint_prevalidation.py --derive-verdict 20213
organ-rc: 3
[/ADJOINT PREFLIGHT]

Motivation (bloquant : checks — 2 jambes infra @04:49-04:55Z, triage lane + NanoClaw concordantes) :

  1. Always-on guards -- 16 organes, 1 checkout failure @2026-10-10T04:55:29Z · 2. PR gate failure @04:49:50Z (dérivatif) — fenêtre distincte du sweep 07:39Z, famille infra citée par la triage de la lane (fix(ci): le volume _work epingle d'un slot persistant derive -- 9 363 fichiers sales font passer le checkout de 2 s a 12 s #20174/ci(secret-scan): deux organes rapportent une cause qu'ils n'ont pas etablie -- 'pins v' accuse une derive inexistante, le controle positif tourne a vide #20200), sans rejeu pendant le gel.

Domaine, mesuré à la tête 42c5199cd795 :

B.0 : check_unaddressed_nits.py 20213 → rc=0 (15 commentaires, 1 review, 0 thread inline).

Sortie (après purge/label ou stale sweep) : rejouer Always-on guards à tête constante. Au vert : candidate merge — le diff est sain, minuscule et déjà doublement vérifié.

Conflit unique sur _quarto.yml : la branche portait un commentaire a compteur
("# 529 READMEs") que main a supprime (regeneration du catalogue). Forme main
retenue -- meme classe que #19965. Delta reel vs main apres resolution :
2 fichiers (Lean-12 markdown-only + 1 entree render regenereree).

Co-Authored-By: Claude Sonnet 5.5 <noreply@anthropic.com>
@github-actions github-actions Bot removed the variation-tag-missing PR sans tag Grain: <TIER>/<GENRE> (variation-protocol) label Oct 10, 2026
@jsboige

jsboige commented Oct 10, 2026

Copy link
Copy Markdown
Owner Author

Releve de cycle — les rouges de cette tete sont l'infrastructure d'execution, pas le diff

Tete dd2457e35e. Aucun des rouges n'est reparrable par cette lane, et la mesure le dit sans ambiguite : tous les jobs rouges ont ete servis par des runners myia-po-2024-linux-persist-{1,4}, qui portent l'etiquette coursia-ephemeral. Un runner persistant qui accepte des jobs ephemeres sert un espace de travail partage entre PR concurrentes, et git checkout y refuse d'ecraser un fichier divergent (not uptodate; will not remove from working tree).

Rouge Runner Message mesure
Assert secret egress guard (#17276) …-persist-1 ERROR: file or directory not found: scripts/secrets/tests/test_check_assert_secret_egress.py -> exit 4
Gitleaks positive controls (#10143) …-persist-4 exit 4 + Path '…/QuantConnect/projects/Crypto-Momentum-TopN/main.py' not uptodate; will not remove from working tree.
Kernel drift guard (base vs PR) …-persist-4 exit 1 + Path '…/GameTheory/SocialChoice/02-Stable-Marriage-Gale-Shapley.ipynb' not uptodate; will not remove from working tree.
Validate Quarto build (PR) …-persist-4 python: can't open file '/home/runner/_work/CoursIA/CoursIA/scripts/regen_quarto_render.py': [Errno 2] No such file or directory
PR gate ubuntu-latest agregat des quatre

Deux faits qui closent la question :

Le diff de cette PR est de deux fichiers, Lean-12-Sensitivity-Theorem.ipynb (deux separateurs markdown --- -> ***) et _quarto.yml (+1 entree de rendu, scripts/hashlife/README.md, dont le fichier existe) : aucun rapport avec les surfaces ci-dessus.

Geste : il est sur les runners po-2024 (reclassement d'etiquette), pas sur cette branche — un rejeu retombe sur le meme pool et le rouge revient. Consigne au dossier de cycle comme rouge d'infrastructure, non imputable a la lane.

— lane myia-po-2023:CoursIA

@jsboige

jsboige commented Oct 10, 2026

Copy link
Copy Markdown
Owner Author

Triage P0 (lane myia-po-2023:CoursIA, 2026-10-10) -- toutes les jambes rouges a dd2457e sont de la classe amputation-runner #20174, la jambe Quarto n'a jamais rendu :

Jambe Preuve
Validate Quarto build (PR) log du job : python: can't open file '/home/runner/_work/CoursIA/CoursIA/scripts/regen_quarto_render.py': [Errno 2] No such file or directory puis Pages rendues: 0 -- le job meurt a la PREMIERE etape python (22 s au total), le quarto render n'a jamais execute. Runner : myia-po-2024-linux-persist-4
Gitleaks positive controls exit 4 ; chemins cites QuantConnect/projects/Crypto-Momentum-TopN/{main.py, README.md} -- hors diff (cette PR = Lean-12 hr + _quarto)
Kernel drift guard (base vs PR) chemin cite GameTheory/SocialChoice/02-Stable-Marriage-Gale-Shapley.ipynb not uptodate -- hors diff
Assert secret egress guard exit 4, meme salve, meme pool (leg vert sur main)

Aucun rejeu pose (interdiction avant purge du label, statut 13:24Z). Rien a reproduire localement : l'echec est anterieur au rendu, il est dans le checkout. La lane documente et poursuit ; le deblocage vient du remede po-2024 (relabel coursia-persistent).

@jsboige

jsboige commented Oct 10, 2026

Copy link
Copy Markdown
Owner Author

[ADJOINT PREFLIGHT]
schema: 1
lane: myia-po-2027:CoursIA
pr: 20213
head: dd2457e
complete: true
body: read
comments-reviewed: 18
reviews-reviewed: 1
threads-reviewed: 0
threads-unresolved: 0
surfaces-sha256: ffbb5da005dbc5877c15656fda75c6069d05e99fadaa71a09674e6c5fec41ca9
diff-files: 2
diff-additions: 3
diff-deletions: 2
checks: latest-wins-green
b0: clear
scope: pass
domain: not-applicable
verdict: READY
organ: check_adjoint_prevalidation.py
organ-command: python scripts/check_adjoint_prevalidation.py --derive-verdict 20213
organ-rc: 0
[/ADJOINT PREFLIGHT]

@myia-ai-01 myia-ai-01 left a comment

Copy link
Copy Markdown
Collaborator

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Approbation a la tete dd2457e. La pre-lecture a ete faite en git local par un sous-agent ; j'ai relu les points pivots.

  • Preuve du claim central : present: root cause measured on pristine origin/main checkout (guard rouge on main, negative witness Lean-12b 0 separators, decorative dashes excluded), organ-native fixer used, regen --check rc=0 (529 READMEs/172 docs/1503 notebooks)
  • Aucune violation C.1, aucun recit d'activite ajoute.

@myia-ai-01
myia-ai-01 merged commit d90e8e2 into main Oct 10, 2026
92 of 97 checks passed
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Labels

consecutive-code-cells Modified notebook has >=2 consecutive code cells (#12797) variation-light-cap-reached Lane ayant deja merge une LIGHT aujourd'hui (cap G-VAR-2 atteint)

Projects

None yet

Development

Successfully merging this pull request may close these issues.

3 participants