Progress log

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

Progress log: one line per item done, newest first; each phase's page has the whole item.

2026-10-19, Phase 2: the program that reads the specification from the checked library now states the Calculator's version and the Lean that checked it at the head of what it writes, and gives each file comment the line it opens on beside its text, so that the pages can show a file's comments and its definitions in the order they stand in the source
2026-10-18, Phase 0: machine 2's setup tells an installed runner from a running one
2026-10-18, Phase 0: a scheduled build session can now take queued tasks unattended
2026-10-18, Phase 1: version 1's named texts copied from the Operator's copy
2026-10-18, Phase 1: test T3 on the wiki's host, from one scheduled run
2026-10-18, Phase 1: the closing run's record of test T3's scheduled run now names how many of the 100 calls failed and the first failure, and gives the processor time as the whole run's, under or over the budget of a tenth of the hourly cap
2026-10-18, Phase 2: the Calculator's command for the structure check of the equations of motion
2026-10-18, Phase 2: the Calculator's command for the falcons
2026-10-18, Phase 2: the Calculator's command for identity, the sponsor and the prompt lint
2026-10-18, Phase 2: the Calculator's command for Provisions
2026-10-18, Phase 2: the Calculator's command for the register functions
2026-10-18, Phase 2: the Calculator's command for score and beta
2026-10-18, Phase 2: the strike rule's parts that read the Research Assembly and the register answer on the Calculator's command line
2026-10-18, Phase 2: the Calculator's command for units and dimensions, in its final form
2026-10-17, Phase 0: a session served by machine 2 was steered from machine 3 and from a phone (acceptance check 3)
2026-10-17, Phase 0: the status panel says when it was last updated
2026-10-17, Phase 0: a change that edits an automatic check's own script together with what that script checks now gets a second, advisory run of that check with the change's own copy of the script
2026-10-17, Phase 1: the survey of Lean's toolchain set to run once a month, on the 22nd, as a scheduled task of its own
2026-10-17, Phase 1: test T2 on the wiki's host, under MediaWiki's shell framework from the command line
2026-10-17, Phase 1: test T3 on the wiki's host, from the shell
2026-10-17, Phase 1: test T5 on the wiki's host, under the wiki's command framework from the command line
2026-10-17, Phase 1: version 1's named texts copied from the Operator's copy
2026-10-17, Phase 2: the Declarer's choices on eight more questions about the Calculator, recorded in the charter
2026-10-17, Phase 2: the program that reads the specification from the checked library, written in Lean's core alone, as the Declarer chose
2026-10-17, Phase 2: the Calculator's command for probes
2026-10-17, Phase 2: the bound on the size of an exact number, as the Declarer chose
2026-10-17, Phase 2: a Provision's kind read from its text, as the Declarer chose
2026-10-17, Phase 2: the Declarer's answers on the governor's admission, built
2026-10-16, Phase 0: machine 2 set up by the setup script
2026-10-16, Phase 0: the names check runs on machine 2 from its own local list, clean over every file
2026-10-16, Phase 0: on machine 2 the current commit built and passed its tests with the same output as the automatic checks on Linux and Windows for that commit (5728401 of 5728401 vectors, 15585 definitions and theorems through the proof gate, 0 failures) (acceptance check 1)
2026-10-16, Phase 0: machine 2 serves Remote Control sessions, kept running as a user service
2026-10-16, Phase 0: on machine 2, a deliberately broken theorem's error and goal were read through the agent's Lean tools rather than pasted from a terminal (acceptance check 4)
2026-10-16, Phase 0: the account that keeps these pages current exists
2026-10-16, Phase 1: the first unattended push of these pages, by that account
2026-10-15, Phase 0: a working session now re-reads its task's instructions and any new directions at every step boundary, so a direction that pauses, stops or narrows the work reaches it without a restart
2026-10-15, Phase 0: the Declarer's choices on ten open questions, recorded in the charter
2026-10-15, Phase 0: one command, the Declarer's, now lands the finished changes
2026-10-15, Phase 0: changes built side by side now land without touching the same lines
2026-10-15, Phase 1: the 22 physics tool pages show their tool's name as their title, not their place in the wiki's tree
2026-10-15, Phase 1: the Research Toolkit's chart on the Main Page fits its column at every width
2026-10-15, Phase 1: version 1's calculator library, the 25 Python files its corpus generators import, and the 31 input files they read, copied verbatim from the version 1 tree published on this wiki, so those generators now run from the source repository
2026-10-15, Phase 1: the survey of Lean's toolchain, built
2026-10-15, Phase 1: test T5's run on the wiki's host became a step of the Operator's closing run, as the runs of T1 to T3 are
2026-10-15, Phase 1: the closing run now lands what the Operator's run produces on this page and on the status panel too, each item once, the figure of the phases redrawn when a state changes
2026-10-15, Phase 1: the Declarer approved the three-letter code table as it stands
2026-10-15, Phase 1: the terminology page and the terminology map show the three-letter codes as approved
2026-10-15, Phase 1: the closing run can now set up test T3's scheduled run on the wiki's host itself, as the Declarer chose, when the Operator asks it to
2026-10-15, Phase 2: the cluster rule and its resolving step, which place the leading models in or out of the top group each month, ported with exact arithmetic in place of version 1's floating point
2026-10-15, Phase 2: the strike rule, distance, SR8 and SR9 in Lean, all but the parts that read the zones
2026-10-15, Phase 2: the canonical serialization, ported
2026-10-15, Phase 2: units and dimensions, in Lean
2026-10-15, Phase 2: units and dimensions
2026-10-15, Phase 2: the Calculator's command line, built
2026-10-15, Phase 2: the cluster rule, the strike rule and SR9 answer on the Calculator's command line
2026-10-15, Phase 2: the three zones' checks, in Lean
2026-10-15, Phase 2: the structured derivation checker's first increment, in Lean
2026-10-15, Phase 2: the bibliography, in Lean
2026-10-15, Phase 2: the fundamental tests T2, T3 and T5, the isomorphism checks IC1 to IC4 and the final pass over the three zones, in Lean
2026-10-15, Phase 2: the strike rule's parts that read the zones and the register's records, in Lean
2026-10-15, Phase 2: the structure check of the equations of motion, in Lean
2026-10-15, Phase 2: hold scope, in Lean
2026-10-15, Phase 2: the yardsticks a Criteria Set declares, in Lean
2026-10-15, Phase 2: the third check of SR9 proved with no condition left
2026-10-15, Phase 2: the permissions function, version 1's table of who may read, change or protect each kind of page, now one Lean function that the wiki's gatekeeper will ask
2026-10-15, Phase 2: the cluster rule's tests compare each result with version 1's expected text field by field, as values of their own kind, rather than as one printed line in which two different results could print alike
2026-10-15, Phase 2: the declared forms, in Lean
2026-10-15, Phase 2: SHA-256 read wherever the zones, the hold, the bibliography, identity, the records and Provisions compute a digest, in place of the answers that waited on it
2026-10-15, Phase 2: SHA-256 in the falcons and the probes
2026-10-15, Phase 2: the falcons in Lean
2026-10-15, Phase 2: the declared forms read in the zones' checks and in the fundamental tests
2026-10-15, Phase 2: the governor's admission, in Lean
2026-10-15, Phase 2: identity in Lean
2026-10-15, Phase 2: the prompt lint, in Lean
2026-10-15, Phase 2: probes and their comparison, all but the draws
2026-10-15, Phase 2: Provisions, in Lean
2026-10-15, Phase 2: the records and the register functions, in Lean
2026-10-15, Phase 2: the reliability score and its Beta layer, in Lean
2026-10-15, Phase 2: SHA-256, written in Lean as part of the Calculator, as the standard FIPS 180-4 defines it, with no library and no code from outside
2026-10-15, Phase 2: the digests of the specification and of the instruction set, in Lean
2026-10-15, Phase 2: the sponsor's functions, in Lean
2026-10-15, Phase 2: SR6's independence count now runs version 1's branch and bound, which stops a search as soon as it cannot beat the best count found, in place of trying every group of contradictions
2026-10-15, Phase 2: the structured derivation checker joined to the credit a result's derivation earns
2026-10-15, Phase 2: the structured derivation checker matches a law to an instance of it
2026-10-15, Phase 2: Unicode's tables read wherever the Calculator reads text, in place of the interim tables
2026-10-15, Phase 2: Unicode's normalization and general category, in Lean, as version 1 used them
2026-10-14, Phase 0: the push that keeps these pages current, built
2026-10-14, Phase 0: the kit for tests T2 and T3 beside T1's
2026-10-14, Phase 0: one closing run for machine 1
2026-10-14, Phase 0: the closing run's first start stopped at its own preflight
2026-10-14, Phase 0: two terms added to the disclosure check's list
2026-10-14, Phase 0: test T1 on the wiki's host, measured three ways
2026-10-14, Phase 0: v1's seed, the other half, from the work folder
2026-10-14, Phase 0: one run for machine 2
2026-10-14, Phase 0: the page on the move to Lean corrected at its source, for the next publish
2026-10-14, Phase 0: the disclosure check runs in the automatic checks on every proposed change, over the wiki's page sources and over these pages as rendered, so no text reaches the main line unread by it
2026-10-14, Phase 0: the proof gate closed a gap
2026-10-14, Phase 0: test T1's kit and its run now give each of the test's three calls its own verdict, as the charter defines them
2026-10-14, Phase 0: the kits for tests T2 and T3 rebuilt to call the binary the way the wiki calls its diagram renderer, through the wiki's own command framework, from a maintenance task on the command line rather than a web request
2026-10-14, Phase 0: the kit for test T5, a check by Lean's kernel rules on the host
2026-10-14, Phase 0: the status panel, a progress page of its own
2026-10-14, Phase 0: staleness on the status panel counts only the items under way, partly done or blocked
2026-10-14, Phase 0: the names check keeps a citation faithful to its source
2026-10-14, Phase 0: the Declarer's publish put on the wiki the page on the move to Lean as corrected, under its plain title "The move to Lean", the Main Page's box with the figure of the phases computed from the status panel and a link to the panel, and the short title "Principia Machina/Lean transition/Status", which leads to the panel
2026-10-14, Phase 1: begun beside Phase 0
2026-10-14, Phase 1: version 1's 33 vector corpora, 6,786 test cases in all, and the 33 programs that generated them, copied verbatim from the version 1 tree published on this wiki
2026-10-14, Phase 1: the declared parameters and tuning options of version 1's specification, in Lean
2026-10-14, Phase 1: the terminology page
2026-10-14, Phase 1: the record table as Lean types, with the three forms a derivation may take (prose, structured steps, a Lean proof) and the class each earns
2026-10-14, Phase 1: a map for every section of the wiki, after the one version 1's pages carry
2026-10-14, Phase 1: the terminology page went up on the wiki with the Declarer's publish, its codes marked proposed until he approves them
2026-10-13, Phase 0: v1's pages that should not have been public
2026-10-13, Phase 0: the wiki's extension updated to TPX 0.6.1, with the check that guards publishing
2026-10-13, Phase 0: wide figures shrink to their column on every page, through a shared style sheet ("Template:Principia Machina/styles.css")
2026-10-13, Phase 0: a separate management dialog plans this work
2026-10-13, Phase 0: the standing rules for agents name the Agent Contract's versions among what the Declarer declares, and Custos beside TPX among the deployments that are his
2026-10-13, Phase 0: cloud sessions read the wiki's public interface
2026-10-13, Phase 0: v1's record seeded from the wiki, read only
2026-10-13, Phase 0: these progress pages rewritten as PUBLIC text, and the session check reading the date they carry
2026-10-13, Phase 0: the renderer for these pages
2026-10-13, Phase 0: a survey of ways to cut the manual steps in the remote workflow, each rated for security, time saved and steps removed
2026-10-13, Phase 0: a daily read-only measurement of how reliably automated reads reach the wiki, by the kind of machine that sends them
2026-10-13, Phase 0: a read-only survey script lists which wiki pages use the server-rendered diagram tags and the external-data functions, and whether the wiki's search index is built
2026-10-12, Phase 0: a names check refuses any personal name on a private list in every file
2026-10-12, Phase 0: a session check runs at the start of every working session on every machine and in the cloud, and reports whether these progress pages are current and whether the working copy is behind
2026-10-12, Phase 0: two design notes
2026-10-12, Phase 0: machine 1 set up by the setup script
2026-10-12, Phase 0: the same commit built and passed its tests (6 of 6 vectors, 7 definitions and theorems through the proof gate, 0 failures) on Linux and Windows in the automatic checks, in a cloud session and on machine 1
2026-10-12, Phase 0: in a cloud session and on machine 1, a deliberately broken theorem's error and goal were read through the agent's Lean tools rather than pasted from a terminal
2026-10-12, Phase 0: the cloud working environment created
2026-10-12, Phase 0: a change started in a cloud session from machine 3 was continued on machine 1 with its whole history, finished there and merged with every check green (acceptance check 2)
2026-10-12, Phase 0: line endings
2026-10-12, Phase 0: publishing and disclosure settled
2026-10-11, Phase 0: naming rules for the project's documents
2026-10-10, Phase 0: the source repository created, private, with its main line protected against deletion and history rewriting
2026-10-10, Phase 0: the skeleton

as of 2026-10-19