Principia Machina/Progress/Status: Difference between revisions
Appearance
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 11: | Line 11: | ||
<div class="pma-tile pma-lamp-amber"><span class="pma-tile-name">Phase 0</span><span class="pma-tile-word">UNDER WAY</span><span class="pma-tile-meta">4 of 5 done</span><span class="pma-tile-meta">likely 2026-10-18</span></div> | <div class="pma-tile pma-lamp-amber"><span class="pma-tile-name">Phase 0</span><span class="pma-tile-word">UNDER WAY</span><span class="pma-tile-meta">4 of 5 done</span><span class="pma-tile-meta">likely 2026-10-18</span></div> | ||
<div class="pma-tile pma-lamp-amber"><span class="pma-tile-name">Phase 1</span><span class="pma-tile-word">UNDER WAY</span><span class="pma-tile-meta">9 of 14 done</span><span class="pma-tile-meta">likely 2026-10-22</span></div> | <div class="pma-tile pma-lamp-amber"><span class="pma-tile-name">Phase 1</span><span class="pma-tile-word">UNDER WAY</span><span class="pma-tile-meta">9 of 14 done</span><span class="pma-tile-meta">likely 2026-10-22</span></div> | ||
<div class="pma-tile pma-lamp-amber"><span class="pma-tile-name">Phase 2</span><span class="pma-tile-word">UNDER WAY</span><span class="pma-tile-meta"> | <div class="pma-tile pma-lamp-amber"><span class="pma-tile-name">Phase 2</span><span class="pma-tile-word">UNDER WAY</span><span class="pma-tile-meta">7 of 19 done</span><span class="pma-tile-meta">likely 2026-11-26</span></div> | ||
<div class="pma-tile pma-lamp-grey"><span class="pma-tile-name">Phase 3</span><span class="pma-tile-word">NOT STARTED</span><span class="pma-tile-meta">0 of 8 done</span><span class="pma-tile-meta">likely 2026-12-13</span></div> | <div class="pma-tile pma-lamp-grey"><span class="pma-tile-name">Phase 3</span><span class="pma-tile-word">NOT STARTED</span><span class="pma-tile-meta">0 of 8 done</span><span class="pma-tile-meta">likely 2026-12-13</span></div> | ||
<div class="pma-tile pma-lamp-grey"><span class="pma-tile-name">Phase 4</span><span class="pma-tile-word">NOT STARTED</span><span class="pma-tile-meta">0 of 6 done</span><span class="pma-tile-meta">likely 2026-12-20</span></div> | <div class="pma-tile pma-lamp-grey"><span class="pma-tile-name">Phase 4</span><span class="pma-tile-word">NOT STARTED</span><span class="pma-tile-meta">0 of 6 done</span><span class="pma-tile-meta">likely 2026-12-20</span></div> | ||
| Line 78: | Line 78: | ||
! Item !! class="pma-c-state" | State !! class="pma-wide pma-c-owner" | Owner !! class="pma-c-date" | Projected !! class="pma-wide pma-c-date" | Checked | ! Item !! class="pma-c-state" | State !! class="pma-wide pma-c-owner" | Owner !! class="pma-c-date" | Projected !! class="pma-wide pma-c-date" | Checked | ||
|- | |- | ||
| Digests and canonical serialization | | Digests and canonical serialization || class="pma-lamp pma-lamp-green" | DONE || class="pma-wide" | Agent || class="pma-date" | 2026-11-26 || class="pma-wide pma-date" | 2026-10-15 | ||
|- | |- | ||
| Units and dimensions<span class="pma-note">: all seven of version 1's unit functions, with all of its test cases; the Calculator's command for them takes its final form with canonical serialization</span> || class="pma-lamp pma-lamp-lgreen" | PARTIAL 7 of 8 || class="pma-wide" | Agent || class="pma-date" | 2026-11-26 || class="pma-wide pma-date" | 2026-10-15 | | Units and dimensions<span class="pma-note">: all seven of version 1's unit functions, with all of its test cases; the Calculator's command for them takes its final form with canonical serialization</span> || class="pma-lamp pma-lamp-lgreen" | PARTIAL 7 of 8 || class="pma-wide" | Agent || class="pma-date" | 2026-11-26 || class="pma-wide pma-date" | 2026-10-15 | ||
|- | |- | ||
| The zones: Starting Set, Correspondence Table, Criteria Set | | The zones: Starting Set, Correspondence Table, Criteria Set || class="pma-lamp pma-lamp-green" | DONE || class="pma-wide" | Agent || class="pma-date" | 2026-11-26 || class="pma-wide pma-date" | 2026-10-15 | ||
|- | |- | ||
| Declared forms | | Declared forms || class="pma-lamp pma-lamp-green" | DONE || class="pma-wide" | Agent || class="pma-date" | 2026-11-26 || class="pma-wide pma-date" | 2026-10-15 | ||
|- | |- | ||
| Fundamental tests and isomorphism checks | | Fundamental tests and isomorphism checks || class="pma-lamp pma-lamp-green" | DONE || class="pma-wide" | Agent || class="pma-date" | 2026-11-26 || class="pma-wide pma-date" | 2026-10-15 | ||
|- | |- | ||
| Records and the register functions<span class="pma-note">: the functions are ported | | Records and the register functions<span class="pma-note">: the functions are ported, the record digests computed with SHA-256 as in version 1; the verification's difference waits on the numeric meaning, and the Calculator's command follows</span> || class="pma-lamp pma-lamp-lgreen" | PARTIAL 2 of 3 || class="pma-wide" | Agent || class="pma-date" | 2026-11-26 || class="pma-wide pma-date" | 2026-10-15 | ||
|- | |- | ||
| The strike rule, distance, SR8 and SR9<span class="pma-note">: version 1's five test sets pass; its call on the Calculator's command line follows canonical serialization</span> || class="pma-lamp pma-lamp-lgreen" | PARTIAL 5 of 6 || class="pma-wide" | Agent || class="pma-date" | 2026-11-26 || class="pma-wide pma-date" | 2026-10-15 | | The strike rule, distance, SR8 and SR9<span class="pma-note">: version 1's five test sets pass; its call on the Calculator's command line follows canonical serialization</span> || class="pma-lamp pma-lamp-lgreen" | PARTIAL 5 of 6 || class="pma-wide" | Agent || class="pma-date" | 2026-11-26 || class="pma-wide pma-date" | 2026-10-15 | ||
|- | |- | ||
| Hold scope | | Hold scope || class="pma-lamp pma-lamp-green" | DONE || class="pma-wide" | Agent || class="pma-date" | 2026-11-26 || class="pma-wide pma-date" | 2026-10-15 | ||
|- | |- | ||
| The structure check of the equations of motion<span class="pma-note">: version 1's two test sets pass; its call on the Calculator's command line follows canonical serialization</span> || class="pma-lamp pma-lamp-lgreen" | PARTIAL 2 of 3 || class="pma-wide" | Agent || class="pma-date" | 2026-11-26 || class="pma-wide pma-date" | 2026-10-15 | | The structure check of the equations of motion<span class="pma-note">: version 1's two test sets pass; its call on the Calculator's command line follows canonical serialization</span> || class="pma-lamp pma-lamp-lgreen" | PARTIAL 2 of 3 || class="pma-wide" | Agent || class="pma-date" | 2026-11-26 || class="pma-wide pma-date" | 2026-10-15 | ||
|- | |- | ||
| Provisions<span class="pma-note">: the functions are ported, with the kinds Interaction and Convention; | | Provisions<span class="pma-note">: the functions are ported, with the kinds Interaction and Convention, text read in NFC and the digests computed with SHA-256 as in version 1; the Calculator's command for them waits on the Declarer's choice of how it answers a request it cannot judge yet</span> || class="pma-lamp pma-lamp-lgreen" | PARTIAL 2 of 3 || class="pma-wide" | Agent || class="pma-date" | 2026-11-26 || class="pma-wide pma-date" | 2026-10-15 | ||
|- | |- | ||
| Probes and their comparison<span class="pma-note">: version 1's test cases computed, | | Probes and their comparison<span class="pma-note">: the functions are ported, all 252 of version 1's test cases computed and agreeing, the draws with SHA-256 and exact numbers; the Calculator's command for probes follows</span> || class="pma-lamp pma-lamp-lgreen" | PARTIAL 1 of 2 || class="pma-wide" | Agent || class="pma-date" | 2026-11-26 || class="pma-wide pma-date" | 2026-10-15 | ||
|- | |- | ||
| Score and beta<span class="pma-note">: ported with exact values, all of version 1's test cases passing, the user score's evidence with them now that the sponsor's functions are ported; the Calculator's command for the family follows</span> || class="pma-lamp pma-lamp-lgreen" | PARTIAL 2 of 3 || class="pma-wide" | Agent || class="pma-date" | 2026-11-26 || class="pma-wide pma-date" | 2026-10-15 | | Score and beta<span class="pma-note">: ported with exact values, all of version 1's test cases passing, the user score's evidence with them now that the sponsor's functions are ported; the Calculator's command for the family follows</span> || class="pma-lamp pma-lamp-lgreen" | PARTIAL 2 of 3 || class="pma-wide" | Agent || class="pma-date" | 2026-11-26 || class="pma-wide pma-date" | 2026-10-15 | ||
| Line 104: | Line 104: | ||
| Cluster || class="pma-lamp pma-lamp-green" | DONE || class="pma-wide" | Agent || class="pma-date" | 2026-11-26 || class="pma-wide pma-date" | 2026-10-15 | | Cluster || class="pma-lamp pma-lamp-green" | DONE || class="pma-wide" | Agent || class="pma-date" | 2026-11-26 || class="pma-wide pma-date" | 2026-10-15 | ||
|- | |- | ||
| Falcons<span class="pma-note">: the functions are ported, | | Falcons<span class="pma-note">: the functions are ported, all 949 of version 1's test cases passing, text in NFC and the digests in SHA-256 as in version 1; the Calculator's command follows</span> || class="pma-lamp pma-lamp-lgreen" | PARTIAL 3 of 4 || class="pma-wide" | Agent || class="pma-date" | 2026-11-26 || class="pma-wide pma-date" | 2026-10-15 | ||
|- | |- | ||
| Bibliography | | Bibliography || class="pma-lamp pma-lamp-green" | DONE || class="pma-wide" | Agent || class="pma-date" | 2026-11-26 || class="pma-wide pma-date" | 2026-10-15 | ||
|- | |- | ||
| Identity, sponsor and lint<span class="pma-note">: identity and lint are ported, the prompt digest | | Identity, sponsor and lint<span class="pma-note">: identity, sponsor and lint are ported, text in NFC and the prompt digest computed with SHA-256 as in version 1; the Calculator's command for them follows</span> || class="pma-lamp pma-lamp-lgreen" | PARTIAL 3 of 4 || class="pma-wide" | Agent || class="pma-date" | 2026-11-26 || class="pma-wide pma-date" | 2026-10-15 | ||
|- | |- | ||
| Governor and permissions<span class="pma-note">: the permissions function and the governor's admission; five questions on admission wait on the Declarer; the pressure levels, then the traffic stages, follow</span> || class="pma-lamp pma-lamp-lgreen" | PARTIAL 2 of 3 || class="pma-wide" | Agent || class="pma-date" | 2026-11-26 || class="pma-wide pma-date" | 2026-10-15 | | Governor and permissions<span class="pma-note">: the permissions function and the governor's admission; five questions on admission wait on the Declarer; the pressure levels, then the traffic stages, follow</span> || class="pma-lamp pma-lamp-lgreen" | PARTIAL 2 of 3 || class="pma-wide" | Agent || class="pma-date" | 2026-11-26 || class="pma-wide pma-date" | 2026-10-15 | ||
Revision as of 19:52, 17 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 |
The status panel: every item of every phase as a lamp, from the setup to the first release declared; the aim is every lamp green. Each phase's own page tells its items in words.
DONE PARTIAL n of m UNDER WAY BLOCKED NOT STARTED OVERDUE past its likely date and not done; a panel whose rows under way, partial or blocked are unchecked for more than 2 days is STALE. Every lamp carries its word; the colours repeat it.
Master annunciator · lamps judged on 2026-10-17
Phase 0UNDER WAY
Phase 1UNDER WAY
Phase 2UNDER WAY
Phase 3NOT STARTED
Phase 4NOT STARTED
Phase 5NOT STARTED
Phase 6NOT STARTED
First releaseNOT STARTED
Faults
No faults
The seven phases and the first release
| Item | State | Owner | Projected | Checked |
|---|---|---|---|---|
| Check 1: one change builds and passes its tests alike on every machine, in a cloud session and in the automatic checks | DONE | Operator | 2026-10-18 | 2026-10-16 |
| Check 2: a task started in a cloud session from one machine, then finished and merged from another | DONE | Operator | 2026-10-18 | 2026-10-14 |
| Check 3: a session served by machine 2, steered from machine 3 and from a phone or tablet | NOT STARTED | Operator | 2026-10-18 | 2026-10-15 |
| Check 4: a broken proof's error read through the agent's Lean tools in each kind of session | DONE | Operator | 2026-10-18 | 2026-10-16 |
| Check 5: line endings identical when committed from Windows and from Linux | DONE | Operator | 2026-10-18 | 2026-10-14 |
| Item | State | Owner | Projected | Checked |
|---|---|---|---|---|
| Test T1: a Lean program run on the wiki's host | DONE | Operator | 2026-10-18 | 2026-10-14 |
| Test T2: one timed call with a 1 MB input, through the wiki's command framework: kit ready, the run on the host owed | UNDER WAY | Operator | 2026-10-18 | 2026-10-17 |
| Test T3: a hundred calls in one scheduled run, against the hourly budget: kit ready, the run on the host owed | UNDER WAY | Operator | 2026-10-18 | 2026-10-17 |
| Test T5: a proof checked on the host by an independent Lean kernel checker: kit ready, the run on the host owed | UNDER WAY | Operator | 2026-10-18 | 2026-10-17 |
| The terminology page, the register of names, on the wiki | DONE | Declarer | 2026-10-18 | 2026-10-15 |
| The three-letter code table approved | DONE | Declarer | 2026-10-18 | 2026-10-15 |
| Version 1's material copied into the source repository: six specification texts and the full sources of version 1's server extension and research client wait on the Operator's copy | PARTIAL 6 of 8 | Operator | 2026-10-18 | 2026-10-17 |
| The declared parameters and tuning options, in Lean | DONE | Agent | 2026-10-18 | 2026-10-14 |
| The record table as Lean types, with the three forms a derivation may take and the class each earns | DONE | Agent | 2026-10-18 | 2026-10-14 |
| The terminology map | DONE | Agent | 2026-10-18 | 2026-10-14 |
| The monthly survey of Lean's toolchain, as a scheduled task that proposes upgrades: set up to run monthly; its first run falls on 2026-10-22 | UNDER WAY | Agent | 2026-10-22 | 2026-10-17 |
| Publishing the framework's pages from the source, by the Declarer's act | DONE | Agent | 2026-10-18 | 2026-10-14 |
| The push that keeps the progress pages current, after every landing and once a day | DONE | Agent | 2026-10-18 | 2026-10-14 |
| The progress pages' wiki account, and their first unattended push | DONE | Operator | 2026-10-18 | 2026-10-17 |
| Item | State | Owner | Projected | Checked |
|---|---|---|---|---|
| Digests and canonical serialization | DONE | Agent | 2026-11-26 | 2026-10-15 |
| Units and dimensions: all seven of version 1's unit functions, with all of its test cases; the Calculator's command for them takes its final form with canonical serialization | PARTIAL 7 of 8 | Agent | 2026-11-26 | 2026-10-15 |
| The zones: Starting Set, Correspondence Table, Criteria Set | DONE | Agent | 2026-11-26 | 2026-10-15 |
| Declared forms | DONE | Agent | 2026-11-26 | 2026-10-15 |
| Fundamental tests and isomorphism checks | DONE | Agent | 2026-11-26 | 2026-10-15 |
| Records and the register functions: the functions are ported, the record digests computed with SHA-256 as in version 1; the verification's difference waits on the numeric meaning, and the Calculator's command follows | PARTIAL 2 of 3 | Agent | 2026-11-26 | 2026-10-15 |
| The strike rule, distance, SR8 and SR9: version 1's five test sets pass; its call on the Calculator's command line follows canonical serialization | PARTIAL 5 of 6 | Agent | 2026-11-26 | 2026-10-15 |
| Hold scope | DONE | Agent | 2026-11-26 | 2026-10-15 |
| The structure check of the equations of motion: version 1's two test sets pass; its call on the Calculator's command line follows canonical serialization | PARTIAL 2 of 3 | Agent | 2026-11-26 | 2026-10-15 |
| Provisions: the functions are ported, with the kinds Interaction and Convention, text read in NFC and the digests computed with SHA-256 as in version 1; the Calculator's command for them waits on the Declarer's choice of how it answers a request it cannot judge yet | PARTIAL 2 of 3 | Agent | 2026-11-26 | 2026-10-15 |
| Probes and their comparison: the functions are ported, all 252 of version 1's test cases computed and agreeing, the draws with SHA-256 and exact numbers; the Calculator's command for probes follows | PARTIAL 1 of 2 | Agent | 2026-11-26 | 2026-10-15 |
| Score and beta: ported with exact values, all of version 1's test cases passing, the user score's evidence with them now that the sponsor's functions are ported; the Calculator's command for the family follows | PARTIAL 2 of 3 | Agent | 2026-11-26 | 2026-10-15 |
| Cluster | DONE | Agent | 2026-11-26 | 2026-10-15 |
| Falcons: the functions are ported, all 949 of version 1's test cases passing, text in NFC and the digests in SHA-256 as in version 1; the Calculator's command follows | PARTIAL 3 of 4 | Agent | 2026-11-26 | 2026-10-15 |
| Bibliography | DONE | Agent | 2026-11-26 | 2026-10-15 |
| Identity, sponsor and lint: identity, sponsor and lint are ported, text in NFC and the prompt digest computed with SHA-256 as in version 1; the Calculator's command for them follows | PARTIAL 3 of 4 | Agent | 2026-11-26 | 2026-10-15 |
| Governor and permissions: the permissions function and the governor's admission; five questions on admission wait on the Declarer; the pressure levels, then the traffic stages, follow | PARTIAL 2 of 3 | Agent | 2026-11-26 | 2026-10-15 |
| The structured derivation checker, with its soundness proof: the step language, its checker, its credit and the proof that it is sound, with matching a law to an instance of it; which laws may be matched so and what a derivative means wait on the Declarer's choices | UNDER WAY | Agent | 2026-11-26 | 2026-10-15 |
| The generated specification pages and their converter, shipped with each release | NOT STARTED | Agent | 2026-11-26 | 2026-10-14 |
| Item | State | Owner | Projected | Checked |
|---|---|---|---|---|
| A rehearsal wiki running the host's software, MediaWiki 1.46 on PHP 8.4 | NOT STARTED | Operator | 2026-12-13 | 2026-10-14 |
| Custos's page classes | NOT STARTED | Agent | 2026-12-13 | 2026-10-14 |
| Custos's API module | NOT STARTED | Agent | 2026-12-13 | 2026-10-14 |
| Custos's jobs, run outside the web request | NOT STARTED | Agent | 2026-12-13 | 2026-10-14 |
| The call into the Calculator, with the binary's digest checked | NOT STARTED | Agent | 2026-12-13 | 2026-10-14 |
| The governor's meter | NOT STARTED | Agent | 2026-12-13 | 2026-10-14 |
| The derivation class written at landing, and the kernel checker once test T5 has passed | NOT STARTED | Agent | 2026-12-13 | 2026-10-14 |
| Version 1's landing scenarios replayed with the Calculator as the only calculator | NOT STARTED | Agent | 2026-12-13 | 2026-10-14 |
| Item | State | Owner | Projected | Checked |
|---|---|---|---|---|
| The Research Client in Python, calling the Calculator | NOT STARTED | Agent | 2026-12-20 | 2026-10-14 |
| The agent-contract bundle, placed by the client | NOT STARTED | Agent | 2026-12-20 | 2026-10-14 |
| The execution challenge | NOT STARTED | Agent | 2026-12-20 | 2026-10-14 |
| Retry-After obeyed | NOT STARTED | Agent | 2026-12-20 | 2026-10-14 |
| The session log | NOT STARTED | Agent | 2026-12-20 | 2026-10-14 |
| A petition, a push and a release against the rehearsal wiki from machine 2 | NOT STARTED | Operator | 2026-12-20 | 2026-10-14 |
| Item | State | Owner | Projected | Checked |
|---|---|---|---|---|
| The bootstrap test: each family, given only this wiki's address, reproduces the spring's derivation | NOT STARTED | Operator | 2027-01-03 | 2026-10-14 |
| The certification suite and the conformance probes, each family in turn | NOT STARTED | Operator | 2027-01-03 | 2026-10-14 |
| The names check, the digest convention and the execution challenge, from each family's tools | NOT STARTED | Operator | 2027-01-03 | 2026-10-14 |
| Each vendor's thin implementation, derived from the Agent Contract | NOT STARTED | Agent | 2027-01-03 | 2026-10-14 |
| The agent-contract bundle's changes declared as a new version | NOT STARTED | Declarer | 2027-01-03 | 2026-10-14 |
| The walk-through, revised by hand with the new words, readable to each family's reader | NOT STARTED | Agent | 2027-01-03 | 2026-10-14 |
| Item | State | Owner | Projected | Checked |
|---|---|---|---|---|
| A certified agent's lifecycle on the synthetic UWC, for each certified family | NOT STARTED | Agent | 2027-01-13 | 2026-10-14 |
| The Calculator and Custos deployed on the host | NOT STARTED | Operator | 2027-01-13 | 2026-10-14 |
| Version 1's pages left untouched, with a banner pointing forward | NOT STARTED | Declarer | 2027-01-13 | 2026-10-14 |
| TPM marked historical on its hub | NOT STARTED | Declarer | 2027-01-13 | 2026-10-14 |
| Item | State | Owner | Projected | Checked |
|---|---|---|---|---|
| The Principia Framework Specification 1.0.0 and the Calculator 1.0.0 declared | NOT STARTED | Declarer | 2027-01-13 2026-12-09 to 2027-03-03 |
2026-10-14 |
Figure 7: the phases

Figure 7. The seven phases, in order, drawn from the status panel: Phases 0 to 2 under way; Phases 3 to 6 not started. The current focus is Phase 0, the lowest phase not done. A phase may begin before the one before it is done. Every state is written in its box; the colours repeat it: green, done; blue, under way; grey, not started; a heavier outline, the current focus.
This panel
| Item | State | Owner | Checked |
|---|---|---|---|
| Figure 7 copies current: both copies match this page's | DONE | Declarer | 2026-10-17 |
as of 2026-10-17