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 10: | Line 10: | ||
<div class="pma-strip-head">Master annunciator · lamps judged on 2026-10-17</div> | <div class="pma-strip-head">Master annunciator · lamps judged on 2026-10-17</div> | ||
<div class="pma-tile pma-lamp-green"><span class="pma-tile-name">Phase 0</span><span class="pma-tile-word">DONE</span><span class="pma-tile-meta">5 of 5 done</span><span class="pma-tile-meta">likely 2026-10-18</span></div> | <div class="pma-tile pma-lamp-green"><span class="pma-tile-name">Phase 0</span><span class="pma-tile-word">DONE</span><span class="pma-tile-meta">5 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"> | <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">10 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">8 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 21: | Line 21: | ||
== Faults == | == Faults == | ||
<div class="pma-faults"><span class="pma-label pma-lamp-green">No faults</span></div> | <div class="pma-faults"><span class="pma-label pma-lamp-green">No faults</span></div> | ||
{| class="wikitable" | |||
! updated Date: !! Pacific Time !! UTC | |||
|- | |||
| 2026-10-17 || 15:41 PDT || 2026-10-17 22:41 | |||
|- | |||
| 2026-10-17 || 13:02 PDT || 2026-10-17 20:02 | |||
|- | |||
| 2026-10-17 || 12:52 PDT || 2026-10-17 19:52 | |||
|} | |||
== The seven phases and the first release == | == The seven phases and the first release == | ||
| Line 46: | Line 56: | ||
| Test T1: a Lean program run on the wiki's host || class="pma-lamp pma-lamp-green" | DONE || class="pma-wide" | Operator || class="pma-date" | 2026-10-18 || class="pma-wide pma-date" | 2026-10-14 | | Test T1: a Lean program run on the wiki's host || class="pma-lamp pma-lamp-green" | DONE || class="pma-wide" | Operator || class="pma-date" | 2026-10-18 || class="pma-wide pma-date" | 2026-10-14 | ||
|- | |- | ||
| Test T2: one timed call with a 1 MB input, through the wiki's command framework<span class="pma-note">: | | Test T2: one timed call with a 1 MB input, through the wiki's command framework<span class="pma-note">: PASS, 0.070 CPU-seconds a call</span> || class="pma-lamp pma-lamp-green" | DONE || class="pma-wide" | Operator || class="pma-date" | 2026-10-18 || class="pma-wide pma-date" | 2026-10-17 | ||
|- | |- | ||
| Test T3: a hundred calls in one scheduled run, against the hourly budget<span class="pma-note">: | | Test T3: a hundred calls in one scheduled run, against the hourly budget<span class="pma-note">: PASS from the shell, 7.432 CPU-seconds for 100 calls; the scheduled run owed</span> || class="pma-lamp pma-lamp-amber" | UNDER WAY || class="pma-wide" | Operator || class="pma-date" | 2026-10-18 || class="pma-wide pma-date" | 2026-10-17 | ||
|- | |- | ||
| Test T5: a proof checked on the host by an independent Lean kernel checker<span class="pma-note">: kit ready, the run on the host owed</span> || class="pma-lamp pma-lamp-amber" | UNDER WAY || class="pma-wide" | Operator || class="pma-date" | 2026-10-18 || class="pma-wide pma-date" | 2026-10-17 | | Test T5: a proof checked on the host by an independent Lean kernel checker<span class="pma-note">: kit ready, the run on the host owed</span> || class="pma-lamp pma-lamp-amber" | UNDER WAY || class="pma-wide" | Operator || class="pma-date" | 2026-10-18 || class="pma-wide pma-date" | 2026-10-17 | ||
| Line 75: | Line 85: | ||
<div class="pma-panel-wrap"> | <div class="pma-panel-wrap"> | ||
{| class="pma-panel" | {| class="pma-panel" | ||
|+ [[Principia Machina/Progress/Phase 2|Phase 2]]: The Calculator · checked 2026-10- | |+ [[Principia Machina/Progress/Phase 2|Phase 2]]: The Calculator · checked 2026-10-17 | ||
! 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 || 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 | | 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- | | 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-17 | ||
|- | |- | ||
| 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 | | 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 | ||
| Line 88: | Line 98: | ||
| 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 | | 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, 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- | | 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-17 | ||
|- | |- | ||
| 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- | | 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-17 | ||
|- | |- | ||
| 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 | | 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- | | 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-17 | ||
|- | |- | ||
| 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 | | Provisions<span class="pma-note">: the functions are ported, with the kinds Interaction and Convention, a Provision's kind read from its text, text read in NFC and the digests computed with SHA-256 as in version 1; the Calculator's command for them follows, answering what it cannot judge yet as owed</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-17 | ||
|- | |- | ||
| Probes and their comparison | | Probes and their comparison || class="pma-lamp pma-lamp-green" | DONE || class="pma-wide" | Agent || class="pma-date" | 2026-11-26 || class="pma-wide pma-date" | 2026-10-17 | ||
|- | |- | ||
| 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- | | 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-17 | ||
|- | |- | ||
| 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, 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- | | 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-17 | ||
|- | |- | ||
| 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 | | 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, 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- | | 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-17 | ||
|- | |- | ||
| 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- | | 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-17 | ||
|- | |- | ||
| The structured derivation checker, with its soundness proof<span class="pma-note">: 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</span> || class="pma-lamp pma-lamp-amber" | UNDER WAY || class="pma-wide" | Agent || class="pma-date" | 2026-11-26 || class="pma-wide pma-date" | 2026-10- | | The structured derivation checker, with its soundness proof<span class="pma-note">: 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</span> || class="pma-lamp pma-lamp-amber" | UNDER WAY || class="pma-wide" | Agent || class="pma-date" | 2026-11-26 || class="pma-wide pma-date" | 2026-10-17 | ||
|- | |- | ||
| The generated specification pages and their converter, shipped with each release || class="pma-lamp pma-lamp-grey" | NOT STARTED || class="pma-wide" | Agent || class="pma-date" | 2026-11-26 || class="pma-wide pma-date" | 2026-10-14 | | The generated specification pages and their converter, shipped with each release || class="pma-lamp pma-lamp-grey" | NOT STARTED || class="pma-wide" | Agent || class="pma-date" | 2026-11-26 || class="pma-wide pma-date" | 2026-10-14 | ||
Revision as of 22:41, 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 0DONE
Phase 1UNDER WAY
Phase 2UNDER WAY
Phase 3NOT STARTED
Phase 4NOT STARTED
Phase 5NOT STARTED
Phase 6NOT STARTED
First releaseNOT STARTED
Faults
No faults
| updated Date: | Pacific Time | UTC |
|---|---|---|
| 2026-10-17 | 15:41 PDT | 2026-10-17 22:41 |
| 2026-10-17 | 13:02 PDT | 2026-10-17 20:02 |
| 2026-10-17 | 12:52 PDT | 2026-10-17 19:52 |
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 | DONE | Operator | 2026-10-18 | 2026-10-17 |
| 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: PASS, 0.070 CPU-seconds a call | DONE | Operator | 2026-10-18 | 2026-10-17 |
| Test T3: a hundred calls in one scheduled run, against the hourly budget: PASS from the shell, 7.432 CPU-seconds for 100 calls; the scheduled run 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-17 |
| 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-17 |
| 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-17 |
| 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-17 |
| Provisions: the functions are ported, with the kinds Interaction and Convention, a Provision's kind read from its text, text read in NFC and the digests computed with SHA-256 as in version 1; the Calculator's command for them follows, answering what it cannot judge yet as owed | PARTIAL 2 of 3 | Agent | 2026-11-26 | 2026-10-17 |
| Probes and their comparison | DONE | Agent | 2026-11-26 | 2026-10-17 |
| 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-17 |
| 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-17 |
| 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-17 |
| 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-17 |
| 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-17 |
| 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: Phase 0 done; Phases 1 and 2 under way; Phases 3 to 6 not started. The current focus is Phase 1, 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: waiting for the next publish: the copy on the Lean transition page and on the Main Page differs | UNDER WAY | Declarer | 2026-10-17 |
as of 2026-10-17