Principia Machina/Progress/Phase 3: Difference between revisions
PMA Progress (talk | contribs) Progress pages rendered from the Principia Machina source |
PMA Progress (talk | contribs) Progress pages rendered from the Principia Machina source |
||
| Line 6: | Line 6: | ||
== Done == | == Done == | ||
* 2026-10-21: the rehearsal wiki: made when a release needs one, on a fresh server, by the same provisioning script that built the wiki's server, running the same software. The standing rehearsal copy used before the move is retired. | |||
== Open == | == Open == | ||
* The Calculator's residence on the host and the step that places a released binary there. | * The Calculator's residence on the host and the step that places a released binary there. | ||
Latest revision as of 02:50, 21 October 2026
| Principia Machina: map |
|---|
| Reading the program The move to Lean Status Terminology: the words of both versions |
| Lean itself Lean theorem prover Principia Machina in Lean |
| Version 1 The Principia Machina its specification |
Phase 3: Custos
Goal: the wiki's thin gatekeeper, Custos, built against a rehearsal wiki running the host's software: its page classes, its API module, its jobs run outside the web request, its call into the Calculator with the binary's digest checked, the governor's meter, the derivation class written at landing and the kernel checker, and version 1's landing scenarios replayed with the Calculator as the only calculator.
Done
- 2026-10-21: the rehearsal wiki: made when a release needs one, on a fresh server, by the same provisioning script that built the wiki's server, running the same software. The standing rehearsal copy used before the move is retired.
Open
- The Calculator's residence on the host and the step that places a released binary there.
Next
The first unit: the extension's skeleton, the store seam, the call into the Calculator with the digest check, and a harness that runs without the host.
as of 2026-10-21