Jump to content

Principia Machina/Progress/Status: Difference between revisions

From The Invariance Itself
← Older edit

PMA Progress (talk | contribs)

1 user group
81 edits
PMA Progress (talk | contribs)
approved
81 edits
Progress pages rendered from the Principia Machina source
PMA Progress (talk | contribs)
approved
81 edits
Progress pages rendered from the Principia Machina source
 
(10 intermediate revisions by the same user not shown)
Line 8: Line 8:


<div class="pma-strip">
<div class="pma-strip">
<div class="pma-strip-head">Master annunciator &middot; lamps judged on 2026-10-17</div>
<div class="pma-strip-head">Master annunciator &middot; lamps judged on 2026-10-21</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">11 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">13 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">8 of 19 done</span><span class="pma-tile-meta">likely 2026-11-26</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">16 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-amber"><span class="pma-tile-name">Phase 3</span><span class="pma-tile-word">UNDER WAY</span><span class="pma-tile-meta">1 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>
<div class="pma-tile pma-lamp-grey"><span class="pma-tile-name">Phase 5</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 2027-01-03</span></div>
<div class="pma-tile pma-lamp-grey"><span class="pma-tile-name">Phase 5</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 2027-01-03</span></div>
Line 25: Line 25:
! updated Date: !! Pacific Time !! UTC
! updated Date: !! Pacific Time !! UTC
|-
|-
| 2026-10-17 || 16:59 PDT || 2026-10-17 23:59
| 2026-10-20 || 19:50 PDT || 2026-10-21 02:50
|-
|-
| 2026-10-17 || 16:01 PDT || 2026-10-17 23:01
| 2026-10-20 || 19:45 PDT || 2026-10-21 02:45
|-
|-
| 2026-10-17 || 15:41 PDT || 2026-10-17 22:41
| 2026-10-18 || 19:29 PDT || 2026-10-19 02:29
|}
|}


Line 51: Line 51:
<div class="pma-panel-wrap">
<div class="pma-panel-wrap">
{| class="pma-panel"
{| class="pma-panel"
|+ [[Principia Machina/Progress/Phase 1|Phase 1]]: Foundations &middot; checked 2026-10-17
|+ [[Principia Machina/Progress/Phase 1|Phase 1]]: Foundations &middot; checked 2026-10-21
! 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
|-
|-
Line 58: Line 58:
| 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 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">: 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 T3: a hundred calls in one scheduled run, against the hourly budget<span class="pma-note">: PASS on the server the Operator controls, 0 of 100 calls failed from a scheduled run and under the job runner's limits</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-21
|-
|-
| Test T5: a proof checked on the host by an independent Lean kernel checker<span class="pma-note">: PASS, 0.083 CPU-seconds for a theorem and its closure</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 T5: a proof checked on the host by an independent Lean kernel checker<span class="pma-note">: PASS, 0.083 CPU-seconds for a theorem and its closure</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
Line 66: Line 66:
| The three-letter code table approved || class="pma-lamp pma-lamp-green" | DONE || class="pma-wide" | Declarer || class="pma-date" | 2026-10-18 || class="pma-wide pma-date" | 2026-10-15
| The three-letter code table approved || class="pma-lamp pma-lamp-green" | DONE || class="pma-wide" | Declarer || class="pma-date" | 2026-10-18 || class="pma-wide pma-date" | 2026-10-15
|-
|-
| Version 1's material copied into the source repository<span class="pma-note">: six specification texts and the full sources of version 1's server extension and research client wait on the Operator's copy</span> || class="pma-lamp pma-lamp-lgreen" | PARTIAL 6 of 8 || class="pma-wide" | Operator || class="pma-date" | 2026-10-18 || class="pma-wide pma-date" | 2026-10-17
| Version 1's material copied into the source repository || class="pma-lamp pma-lamp-green" | DONE || class="pma-wide" | Operator || class="pma-date" | 2026-10-18 || class="pma-wide pma-date" | 2026-10-18
|-
|-
| The declared parameters and tuning options, in Lean || class="pma-lamp pma-lamp-green" | DONE || class="pma-wide" | Agent || class="pma-date" | 2026-10-18 || class="pma-wide pma-date" | 2026-10-14
| The declared parameters and tuning options, in Lean || class="pma-lamp pma-lamp-green" | DONE || class="pma-wide" | Agent || class="pma-date" | 2026-10-18 || class="pma-wide pma-date" | 2026-10-14
Line 74: Line 74:
| The terminology map || class="pma-lamp pma-lamp-green" | DONE || class="pma-wide" | Agent || class="pma-date" | 2026-10-18 || class="pma-wide pma-date" | 2026-10-14
| The terminology map || class="pma-lamp pma-lamp-green" | DONE || class="pma-wide" | Agent || class="pma-date" | 2026-10-18 || class="pma-wide pma-date" | 2026-10-14
|-
|-
| The monthly survey of Lean's toolchain, as a scheduled task that proposes upgrades<span class="pma-note">: set up to run monthly; its first run falls on 2026-10-22</span> || class="pma-lamp pma-lamp-amber" | UNDER WAY || class="pma-wide" | Agent || class="pma-date" | 2026-10-22 || class="pma-wide pma-date" | 2026-10-17
| The monthly survey of Lean's toolchain, as a scheduled task that proposes upgrades<span class="pma-note">: set up to run monthly; its first run falls on 2026-10-22</span> || class="pma-lamp pma-lamp-amber" | UNDER WAY || class="pma-wide" | Agent || class="pma-date" | 2026-10-22 || class="pma-wide pma-date" | 2026-10-21
|-
|-
| Publishing the framework's pages from the source, by the Declarer's act || class="pma-lamp pma-lamp-green" | DONE || class="pma-wide" | Agent || class="pma-date" | 2026-10-18 || class="pma-wide pma-date" | 2026-10-14
| Publishing the framework's pages from the source, by the Declarer's act || class="pma-lamp pma-lamp-green" | DONE || class="pma-wide" | Agent || class="pma-date" | 2026-10-18 || class="pma-wide pma-date" | 2026-10-14
Line 85: 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 &middot; checked 2026-10-17
|+ [[Principia Machina/Progress/Phase 2|Phase 2]]: The Calculator &middot; checked 2026-10-21
! 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-17
| Units and dimensions || class="pma-lamp pma-lamp-green" | DONE || class="pma-wide" | Agent || class="pma-date" | 2026-11-26 || class="pma-wide pma-date" | 2026-10-18
|-
|-
| 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 98: 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-17
| Records and the register functions || class="pma-lamp pma-lamp-green" | DONE || class="pma-wide" | Agent || class="pma-date" | 2026-11-26 || class="pma-wide pma-date" | 2026-10-20
|-
|-
| 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
| The strike rule, distance, SR8 and SR9 || class="pma-lamp pma-lamp-green" | DONE || class="pma-wide" | Agent || class="pma-date" | 2026-11-26 || class="pma-wide pma-date" | 2026-10-18
|-
|-
| 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-17
| The structure check of the equations of motion || class="pma-lamp pma-lamp-green" | DONE || class="pma-wide" | Agent || class="pma-date" | 2026-11-26 || class="pma-wide pma-date" | 2026-10-18
|-
|-
| 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
| Provisions || class="pma-lamp pma-lamp-green" | DONE || class="pma-wide" | Agent || class="pma-date" | 2026-11-26 || class="pma-wide pma-date" | 2026-10-18
|-
|-
| 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
| 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-17
| Score and beta || class="pma-lamp pma-lamp-green" | DONE || class="pma-wide" | Agent || class="pma-date" | 2026-11-26 || class="pma-wide pma-date" | 2026-10-18
|-
|-
| 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-17
| Falcons || class="pma-lamp pma-lamp-green" | DONE || class="pma-wide" | Agent || class="pma-date" | 2026-11-26 || class="pma-wide pma-date" | 2026-10-18
|-
|-
| 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-17
| Identity, sponsor and lint || class="pma-lamp pma-lamp-green" | DONE || class="pma-wide" | Agent || class="pma-date" | 2026-11-26 || class="pma-wide pma-date" | 2026-10-18
|-
|-
| 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
| Governor and permissions<span class="pma-note">: the permissions function and the governor's admission, with the Declarer's answers on it; 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-21
|-
|-
| 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 structured derivation checker, with its soundness proof<span class="pma-note">: the checker, its credit and the command that credits a record's derivation; approximation steps with checked bounds follow</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-21
|-
|-
| The generated specification pages and their converter, shipped with each release<span class="pma-note">: the program that reads the checked library; the converter, its checks and the rewrite of the comments the pages carry follow</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<span class="pma-note">: the program that reads the checked library and the converter with its checks; the rewrite of the comments the pages carry follows</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-21
|}
|}
</div>
</div>
<div class="pma-panel-wrap">
<div class="pma-panel-wrap">
{| class="pma-panel"
{| class="pma-panel"
|+ Phase 3: Custos &middot; checked 2026-10-14
|+ [[Principia Machina/Progress/Phase 3|Phase 3]]: Custos &middot; checked 2026-10-21
! 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
|-
|-
| A rehearsal wiki running the host's software, MediaWiki 1.46 on PHP 8.4 || class="pma-lamp pma-lamp-grey" | NOT STARTED || class="pma-wide" | Operator || class="pma-date" | 2026-12-13 || class="pma-wide pma-date" | 2026-10-14
| A rehearsal wiki running the host's software, MediaWiki 1.46 on PHP 8.4<span class="pma-note">: made on demand on a fresh server by the provisioning script, when a release needs one</span> || class="pma-lamp pma-lamp-green" | DONE || class="pma-wide" | Operator || class="pma-date" | 2026-12-13 || class="pma-wide pma-date" | 2026-10-21
|-
|-
| Custos's page classes || class="pma-lamp pma-lamp-grey" | NOT STARTED || class="pma-wide" | Agent || class="pma-date" | 2026-12-13 || class="pma-wide pma-date" | 2026-10-14
| Custos's page classes || class="pma-lamp pma-lamp-grey" | NOT STARTED || class="pma-wide" | Agent || class="pma-date" | 2026-12-13 || class="pma-wide pma-date" | 2026-10-14
Line 219: Line 219:
   P1 [label="Phase 1  Foundations\nunder way: the current focus", fillcolor="#cedff2", color="#6a8fbf", penwidth=2.4];
   P1 [label="Phase 1  Foundations\nunder way: the current focus", fillcolor="#cedff2", color="#6a8fbf", penwidth=2.4];
   P2 [label="Phase 2  The Calculator\nunder way", fillcolor="#cedff2", color="#6a8fbf"];
   P2 [label="Phase 2  The Calculator\nunder way", fillcolor="#cedff2", color="#6a8fbf"];
   P3 [label="Phase 3  Custos\nnot started"];
   P3 [label="Phase 3  Custos\nunder way", fillcolor="#cedff2", color="#6a8fbf"];
   P4 [label="Phase 4  The Research Client\nnot started"];
   P4 [label="Phase 4  The Research Client\nnot started"];
   P5 [label="Phase 5  Other model families\nnot started"];
   P5 [label="Phase 5  Other model families\nnot started"];
Line 228: Line 228:
</graphviz>
</graphviz>
</div>
</div>
<div class="pma-caption">'''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.</div>
<div class="pma-caption">'''Figure 7.''' The seven phases, in order, drawn from the status panel: Phase 0 done; Phases 1 to 3 under way; Phases 4 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.</div>


== This panel ==
== This panel ==
Line 235: Line 235:
! Item !! class="pma-c-state" | State !! class="pma-wide pma-c-owner" | Owner !! class="pma-c-date" | Checked
! Item !! class="pma-c-state" | State !! class="pma-wide pma-c-owner" | Owner !! class="pma-c-date" | Checked
|-
|-
| Figure 7 copies current<span class="pma-note">: waiting for the next publish: the copy on the Lean transition page and on the Main Page differs</span> || class="pma-lamp pma-lamp-amber" | UNDER WAY || class="pma-wide" | Declarer || class="pma-date" | 2026-10-17
| Figure 7 copies current<span class="pma-note">: waiting for the next publish: the copy on the Lean transition page and on the Main Page differs</span> || class="pma-lamp pma-lamp-amber" | UNDER WAY || class="pma-wide" | Declarer || class="pma-date" | 2026-10-21
|}
|}
</div>
</div>


as of 2026-10-17
as of 2026-10-21

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

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-21
Phase 0DONE5 of 5 donelikely 2026-10-18
Phase 1UNDER WAY13 of 14 donelikely 2026-10-22
Phase 2UNDER WAY16 of 19 donelikely 2026-11-26
Phase 3UNDER WAY1 of 8 donelikely 2026-12-13
Phase 4NOT STARTED0 of 6 donelikely 2026-12-20
Phase 5NOT STARTED0 of 6 donelikely 2027-01-03
Phase 6NOT STARTED0 of 4 donelikely 2027-01-13
First releaseNOT STARTED0 of 1 donelikely 2027-01-13

Faults

No faults
updated Date: Pacific Time UTC
2026-10-20 19:50 PDT 2026-10-21 02:50
2026-10-20 19:45 PDT 2026-10-21 02:45
2026-10-18 19:29 PDT 2026-10-19 02:29

The seven phases and the first release

Phase 0: The development setup · checked 2026-10-17
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
Phase 1: Foundations · checked 2026-10-21
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 on the server the Operator controls, 0 of 100 calls failed from a scheduled run and under the job runner's limits DONE Operator 2026-10-18 2026-10-21
Test T5: a proof checked on the host by an independent Lean kernel checker: PASS, 0.083 CPU-seconds for a theorem and its closure DONE 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 DONE Operator 2026-10-18 2026-10-18
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-21
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
Phase 2: The Calculator · checked 2026-10-21
Item State Owner Projected Checked
Digests and canonical serialization DONE Agent 2026-11-26 2026-10-15
Units and dimensions DONE Agent 2026-11-26 2026-10-18
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 DONE Agent 2026-11-26 2026-10-20
The strike rule, distance, SR8 and SR9 DONE Agent 2026-11-26 2026-10-18
Hold scope DONE Agent 2026-11-26 2026-10-15
The structure check of the equations of motion DONE Agent 2026-11-26 2026-10-18
Provisions DONE Agent 2026-11-26 2026-10-18
Probes and their comparison DONE Agent 2026-11-26 2026-10-17
Score and beta DONE Agent 2026-11-26 2026-10-18
Cluster DONE Agent 2026-11-26 2026-10-15
Falcons DONE Agent 2026-11-26 2026-10-18
Bibliography DONE Agent 2026-11-26 2026-10-15
Identity, sponsor and lint DONE Agent 2026-11-26 2026-10-18
Governor and permissions: the permissions function and the governor's admission, with the Declarer's answers on it; the pressure levels, then the traffic stages, follow PARTIAL 2 of 3 Agent 2026-11-26 2026-10-21
The structured derivation checker, with its soundness proof: the checker, its credit and the command that credits a record's derivation; approximation steps with checked bounds follow PARTIAL 1 of 2 Agent 2026-11-26 2026-10-21
The generated specification pages and their converter, shipped with each release: the program that reads the checked library and the converter with its checks; the rewrite of the comments the pages carry follows UNDER WAY Agent 2026-11-26 2026-10-21
Phase 3: Custos · checked 2026-10-21
Item State Owner Projected Checked
A rehearsal wiki running the host's software, MediaWiki 1.46 on PHP 8.4: made on demand on a fresh server by the provisioning script, when a release needs one DONE Operator 2026-12-13 2026-10-21
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
Phase 4: The Research Client · checked 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
Phase 5: Other model families · checked 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
Phase 6: Lifecycle and cutover · checked 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
First release declared · checked 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

Diagrams error (with dot command): /bin/sh: 1: /home/u2504-hc9fzwzjsgj6/bin/dot: not found

Figure 7. The seven phases, in order, drawn from the status panel: Phase 0 done; Phases 1 to 3 under way; Phases 4 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-21

as of 2026-10-21

Retrieved from "https://invarians.org/index.php?title=Principia_Machina/Progress/Status&oldid=6903"