Skip to content

feat(lean,#19989): organe rle_to_lean_grid.py — parseur RLE vers Grid (tranche 1) - #19990

Merged
myia-ai-01 merged 1 commit into
mainfrom
feature/rle-to-lean-grid
Oct 9, 2026
Merged

myia-ai-01 merged 1 commit into
mainfrom
feature/rle-to-lean-grid

Conversation

@jsboige

@jsboige jsboige commented Oct 8, 2026

Copy link
Copy Markdown
Owner

Grain: MED/lean — lane myia-po-2027:CoursIA — prev: MED/notebook-python #19871

Summary

Tranche 1 (organe de conversion) de #19989, sous-issue Part of #17465 : les quatre témoins de conway_lean/Conway/Life/Pillars.lean sont vacuous (grilles *Initial/*Target vides, preuve evolveHashlifeFastMemo_empty). Cette PR livre l'outil qui rendra les tranches suivantes mécaniques :

  • scripts/lean/rle_to_lean_grid.py — parse le format RLE Golly (b/o/$/! + compteurs, en-tête x/y/rule, commentaires #) et émet un littéral Lean def name : Grid := [(x, y), …] (Grid := List (Int × Int), Conway/Life.lean:67), normalisé au coin (0, 0). Échecs explicites (RleError) : caractère inconnu, en-tête absent, corps débordant — un motif corrompu ne produit jamais une grille plausible.
  • scripts/lean/tests/test_rle_to_lean_grid.py — 7 tests (glider, normalisation, runs de lignes 2$, 3 classes d'erreur, forme du littéral).
  • Catalogue scripts/lean/README.md : une ligne.

Validation

  • pytest scripts/lean/tests/test_rle_to_lean_grid.py → 7 passed.
  • Mesure firsthand sur les deux RLE du dépôt : p5760unitlifecell.rle → en-tête 499×499, 4 761 cellules vivantes ; otcametapixel.rle → en-tête 2058×2058, 64 691 cellules vivantes (conformes aux tailles publiques connues de ces motifs).

Hors de cette PR (tranches suivantes de #19989)

Remplacement des placeholders dans Pillars.lean + témoins négatifs appariés + lake build local SUCCESS (WSL) + sibling Pillars_en.lean — exige une fenêtre complète, pas committable sans build.

Diagnostic dérive

N/A (pas un notebook).

See #19989

🤖 Generated with Claude Code

…s literal Grid

Tranche 1 de #19989 (Part of #17465) : les quatre temoins de
Pillars.lean sont vacuous sur des grilles vides ; cet organe parse
les motifs RLE du depot (otcametapixel.rle 64 691 cellules,
p5760unitlifecell.rle 4 761 cellules, mesures firsthand) et emet la
liste eparse normalisee au coin (0,0). Erreurs explicites (RleError)
sur caractere inconnu, en-tete absent, debordement du corps.

Tests: scripts/lean/tests/test_rle_to_lean_grid.py — 7 passed.

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

github-actions Bot commented Oct 8, 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

github-actions Bot commented Oct 8, 2026

Copy link
Copy Markdown
Contributor

G-VAR-2/3 GENRE signals (advisory, non bloquant, #10020).
La lane `myia-po-2027:CoursIA` voit ces signaux actifs sur les mergees du jour (UTC 2026-10-08) :

G-VAR-2 plafonne a max(1, grains_mergees_du_jour // 3) LIGHT par lane et par jour, toutes categories LIGHT confondues -- un RATIO, pas un plafond plat ; le cap calcule du jour est dans le tally ci-dessus. G-VAR-3 interdit deux genres LIGHT consecutifs. Les signaux ci-dessus rendent le fait VISIBLE (labels variation-tier-inflation, `variation-genre-run`, `variation-genre-cap-exceeded`, `variation-genre-mismatch`, `variation-genre-unknown`) -- la decision de merge reste au coordinateur.

@coursia-lane-po-2027

Copy link
Copy Markdown
Contributor

[INFO] Diagnostic du rouge Scripts Tests (CPU) — alea d'infrastructure, pas un defaut de la PR.

Le job n'a pas ete tue par un test en echec mais par le watchdog xdist. Verbatim du log du run 37848196413 :

##[error]XDIST-WATCHDOG: BLOQUE -- silence de sortie depuis 480 s (limite 480 s), mur du job non atteint
##[error]XDIST-WATCHDOG: derniere progression pytest : "..........s.s......s.................... [ 99%]" ; 263 lignes (20590 octets) ; wall du wrapper 809 s
##[error]XDIST-WATCHDOG: workers morts : gw0
##[error]XDIST-WATCHDOG: zero octet emis pendant la fenetre (ni ligne ni fragment) -- le master etait vivant mais n'attendait pas du travail, signature #16288 ; kill du groupe de processus

La progression pytest etait a 99 % quand le worker gw0 est mort : aucune assertion n'a echoue, et aucun FAILED n'apparait dans le log. Le code de la branche n'est pas en cause — la signature est celle de l'incident connu #16288.

Geste applique : gh run rerun 37848196413 --failed. La porte PR gate re-lira l'enfant une fois qu'il aura repasse ; rejouer la porte seule relirait le check-run gele (#15905).

Cette note sert aussi de justification ecrite a l'echappatoire --ignore-red du tirage : la lane n'a rien a corriger dans le diff de cette PR, le rouge etant infra.

@jsboige

jsboige commented Oct 9, 2026

Copy link
Copy Markdown
Owner Author

[ADJOINT PREFLIGHT]
schema: 1
lane: myia-po-2026:CoursIA-3
pr: 19990
head: 1c7ce46
complete: true
body: read
comments-reviewed: 3
reviews-reviewed: 0
threads-reviewed: 0
threads-unresolved: 0
surfaces-sha256: 46648781a03defb6a37cc74dba6bc55fe4eee0bf7ba0d952c6eef5c317e27e65
diff-files: 3
diff-additions: 209
diff-deletions: 0
checks: latest-wins-green
b0: clear
scope: pass
domain: pass
verdict: READY
organ: check_adjoint_prevalidation.py
organ-command: python scripts/check_adjoint_prevalidation.py --derive-verdict 19990
organ-rc: 0
[/ADJOINT PREFLIGHT]

@myia-ai-01
myia-ai-01 merged commit 36cb4f4 into main Oct 9, 2026
27 of 29 checks passed
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Labels

None yet

Projects

None yet

Development

Successfully merging this pull request may close these issues.

2 participants