Archived from monogate.dev
The page you followed a link to has been retired from monogate.dev. Nothing was deleted from history, and the sections below say how to bring it back.
What went, and why
- Evidence workbenches: the evidence browser, the bundle builder and gallery, the rescue suite, proof digestion, the IR bridge, the atlas annex, and the evidence-governed-computation case study. Why: read from fixtures captured in May and June 2026. Tag
attic/research-stack-2026-06. - Research explorers: the advantage lab, the prime residual benchmark, and the template search. Why: read from fixtures captured in May 2026. Tag
attic/research-stack-2026-06. - Lean practice lanes: the PETAL lanes with their certificates and leaderboard. Why: unchanged since May 2026. Tag
attic/research-stack-2026-06. - Challenge board: the challenge list, the per-challenge submission pages, the leaderboard, the in-browser search, and the how-to-submit guide. Why: the database behind it no longer resolves, so no challenge could be listed and no submission stored. Tag
attic/product-wave-2026-09. - Explorer: the operator explorer and the EML language page. Why: their tables and status labels came from fixtures captured in May and June 2026 that nothing re-derives. Tag
attic/product-wave-2026-09. - Math Lab: the optimizer, the cost calculator, the playground and the calculator. Why: hand-typed tables unchanged since April 2026; the games had already moved to 1op.io. Tag
attic/product-wave-2026-09. - Interactive EML lesson: the in-browser course at /learn/eml/interactive. Why: it showed sample outputs instead of running the compiler, and nothing linked to it. Tag
attic/product-wave-2026-09.
What the site checks instead
Four checks run before each deploy. They are not scheduled, so a result can change between deploys without the site noticing.
- Every eml-compile command on the site is run against the newest monogate-forge on PyPI, the compiler
pip install monogate-forgegives you, in a directory holding the source its page shows, and must succeed or fail as the page says. A command whose source the page does not show is checked for argument errors only, and printed output is not compared. - The figures registered in
scripts/site_figures.jsonmust match what measures them, and phrases retired as false must not come back. A number that is not registered there is not checked. - A page that labels a Lean theorem as checked must name it in
scripts/lean_claims.json, and that theorem must compile at a pinned revision with nosorryAxin its#print axioms. - A lesson line that gives a theorem's verdict, proved or not, is re-derived: the page's own Lean command runs on the page's own source, the emitted file is compiled against MachLib, and its
#print axiomsmust agree with the page (scripts/lesson_proofs.json).
Getting one back
Each group's code is in the site's repository at the git tag named beside it. For example, git checkout attic/research-stack-2026-06 -- app/evidence restores the evidence browser, and git checkout attic/product-wave-2026-09 -- app/explorer lib/explorerrestores the Explorer. Every route's redirect lives in next.config.mjs; remove it with the restore.
If you worked through the Lean practice lanes, your progress is still saved in your own browser. Nothing here cleared it, so it picks up again if the lanes come back.