Principia Machina/Progress/Phase 0 - Revision history

PMA Progress: Progress pages rendered from the Principia Machina source

2026-10-21T02:45:55Z

Progress pages rendered from the Principia Machina source

← Older revision		Revision as of 02:45, 21 October 2026
Line 64:		Line 64:
	* 2026-10-18: machine 2's setup tells an installed runner from a running one: it leaves a stopped runner to the watch that restarts it, never installs it again, and refuses to unpack a new runner over an installed one. It writes its two administrator rules before it sets up the runner, and no longer plans again the spool folders it has already made.		* 2026-10-18: machine 2's setup tells an installed runner from a running one: it leaves a stopped runner to the watch that restarts it, never installs it again, and refuses to unpack a new runner over an installed one. It writes its two administrator rules before it sets up the runner, and no longer plans again the spool folders it has already made.
	* 2026-10-18: a scheduled build session can now take queued tasks unattended. A task enters the queue when the planner marks it ready; the session claims it with a time-limited lease written in its one progress note, works it, leaves every result in proposed changes the Declarer lands in the morning with his one command, and marks the task built or blocked. A session that dies is taken over by the next one from what it saved; a pacing note the Declarer writes bounds how many tasks a session takes, and nothing joins the main line unattended.		* 2026-10-18: a scheduled build session can now take queued tasks unattended. A task enters the queue when the planner marks it ready; the session claims it with a time-limited lease written in its one progress note, works it, leaves every result in proposed changes the Declarer lands in the morning with his one command, and marks the task built or blocked. A session that dies is taken over by the next one from what it saved; a pacing note the Declarer writes bounds how many tasks a session takes, and nothing joins the main line unattended.
			* 2026-10-18: the runner's step that requires a check now names the service that posts it. Before adding a check to the set every change must pass, the step lists each check already required and which service it is bound to, binds the new one to the same service, and refuses, naming both, a check already required under another: requiring a check from a service that no longer posts it would have held every change.
	* 2026-10-19: a check that reads a restricted list now runs only code from the trunk. The text the check judges is the proposed change's, while every program it runs or loads is the trunk's, so no proposed code can hold the list. Where a proposal changes one of those programs, the check's record says that the trunk's copy ran instead, which is what the advisory run tells the reader for a check that is handed no list. As a last guard, each word of the list is replaced by a marker in the check's record before the record is kept or shown.		* 2026-10-19: a check that reads a restricted list now runs only code from the trunk. The text the check judges is the proposed change's, while every program it runs or loads is the trunk's, so no proposed code can hold the list. Where a proposal changes one of those programs, the check's record says that the trunk's copy ran instead, which is what the advisory run tells the reader for a check that is handed no list. As a last guard, each word of the list is replaced by a marker in the check's record before the record is kept or shown.

Line 73:		Line 74:
	Phase 0's acceptance list is closed; the Open items above carry into Phase 1 (charter section 10).		Phase 0's acceptance list is closed; the Open items above carry into Phase 1 (charter section 10).

	as of 2026-10-19		as of 2026-10-21

PMA Progress: Progress pages rendered from the Principia Machina source

2026-10-19T19:52:27Z

Progress pages rendered from the Principia Machina source

← Older revision		Revision as of 19:52, 19 October 2026
Line 64:		Line 64:
	* 2026-10-18: machine 2's setup tells an installed runner from a running one: it leaves a stopped runner to the watch that restarts it, never installs it again, and refuses to unpack a new runner over an installed one. It writes its two administrator rules before it sets up the runner, and no longer plans again the spool folders it has already made.		* 2026-10-18: machine 2's setup tells an installed runner from a running one: it leaves a stopped runner to the watch that restarts it, never installs it again, and refuses to unpack a new runner over an installed one. It writes its two administrator rules before it sets up the runner, and no longer plans again the spool folders it has already made.
	* 2026-10-18: a scheduled build session can now take queued tasks unattended. A task enters the queue when the planner marks it ready; the session claims it with a time-limited lease written in its one progress note, works it, leaves every result in proposed changes the Declarer lands in the morning with his one command, and marks the task built or blocked. A session that dies is taken over by the next one from what it saved; a pacing note the Declarer writes bounds how many tasks a session takes, and nothing joins the main line unattended.		* 2026-10-18: a scheduled build session can now take queued tasks unattended. A task enters the queue when the planner marks it ready; the session claims it with a time-limited lease written in its one progress note, works it, leaves every result in proposed changes the Declarer lands in the morning with his one command, and marks the task built or blocked. A session that dies is taken over by the next one from what it saved; a pacing note the Declarer writes bounds how many tasks a session takes, and nothing joins the main line unattended.
			* 2026-10-19: a check that reads a restricted list now runs only code from the trunk. The text the check judges is the proposed change's, while every program it runs or loads is the trunk's, so no proposed code can hold the list. Where a proposal changes one of those programs, the check's record says that the trunk's copy ran instead, which is what the advisory run tells the reader for a check that is handed no list. As a last guard, each word of the list is replaced by a marker in the check's record before the record is kept or shown.

	== Open ==		== Open ==

PMA Progress: Progress pages rendered from the Principia Machina source

2026-10-19T02:28:26Z

Progress pages rendered from the Principia Machina source

← Older revision		Revision as of 02:28, 19 October 2026
Line 63:		Line 63:
	* 2026-10-17: 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. Once that run passes, the Declarer lands the change past the one check that fails by design, with one command that sets that check aside for the merge alone and restores it.		* 2026-10-17: 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. Once that run passes, the Declarer lands the change past the one check that fails by design, with one command that sets that check aside for the merge alone and restores it.
	* 2026-10-18: machine 2's setup tells an installed runner from a running one: it leaves a stopped runner to the watch that restarts it, never installs it again, and refuses to unpack a new runner over an installed one. It writes its two administrator rules before it sets up the runner, and no longer plans again the spool folders it has already made.		* 2026-10-18: machine 2's setup tells an installed runner from a running one: it leaves a stopped runner to the watch that restarts it, never installs it again, and refuses to unpack a new runner over an installed one. It writes its two administrator rules before it sets up the runner, and no longer plans again the spool folders it has already made.
			* 2026-10-18: a scheduled build session can now take queued tasks unattended. A task enters the queue when the planner marks it ready; the session claims it with a time-limited lease written in its one progress note, works it, leaves every result in proposed changes the Declarer lands in the morning with his one command, and marks the task built or blocked. A session that dies is taken over by the next one from what it saved; a pacing note the Declarer writes bounds how many tasks a session takes, and nothing joins the main line unattended.

	== Open ==		== Open ==

PMA Progress: Progress pages rendered from the Principia Machina source

2026-10-19T00:07:29Z

Progress pages rendered from the Principia Machina source

← Older revision		Revision as of 00:07, 19 October 2026
Line 62:		Line 62:
	* 2026-10-17: the status panel says when it was last updated: under its Faults panel, a table of the last three times the push of these pages changed it, newest first, each as a date and a time in Pacific time and in UTC. A push that finds nothing else changed saves nothing, so the table never counts its own times as a change.		* 2026-10-17: the status panel says when it was last updated: under its Faults panel, a table of the last three times the push of these pages changed it, newest first, each as a date and a time in Pacific time and in UTC. A push that finds nothing else changed saves nothing, so the table never counts its own times as a change.
	* 2026-10-17: 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. Once that run passes, the Declarer lands the change past the one check that fails by design, with one command that sets that check aside for the merge alone and restores it.		* 2026-10-17: 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. Once that run passes, the Declarer lands the change past the one check that fails by design, with one command that sets that check aside for the merge alone and restores it.
			* 2026-10-18: machine 2's setup tells an installed runner from a running one: it leaves a stopped runner to the watch that restarts it, never installs it again, and refuses to unpack a new runner over an installed one. It writes its two administrator rules before it sets up the runner, and no longer plans again the spool folders it has already made.

	== Open ==		== Open ==
Line 70:		Line 71:
	Phase 0's acceptance list is closed; the Open items above carry into Phase 1 (charter section 10).		Phase 0's acceptance list is closed; the Open items above carry into Phase 1 (charter section 10).

	as of 2026-10-18		as of 2026-10-19

PMA Progress: Progress pages rendered from the Principia Machina source

2026-10-18T15:43:55Z

Progress pages rendered from the Principia Machina source

← Older revision		Revision as of 15:43, 18 October 2026
Line 65:		Line 65:
	== Open ==		== Open ==
	* The Declarer's next publish: the section maps with the Main Page's entrance to the Lean edition, and the 22 physics tool pages' titles, both recorded on Phase 1's page; neither gates an item of any phase.		* The Declarer's next publish: the section maps with the Main Page's entrance to the Lean edition, and the 22 physics tool pages' titles, both recorded on Phase 1's page; neither gates an item of any phase.
	* v1's seed: the 33 vector corpora and their generators were found on this wiki and copied verbatim (recorded on Phase 1's page); six specification texts at the versions the charter names still wait on the Operator's copy.

	== Next ==		== Next ==

PMA Progress: Progress pages rendered from the Principia Machina source

2026-10-18T01:13:34Z

Progress pages rendered from the Principia Machina source

← Older revision		Revision as of 01:13, 18 October 2026
Line 61:		Line 61:
	* 2026-10-17: a session served by machine 2 was steered from machine 3 and from a phone (acceptance check 3).		* 2026-10-17: a session served by machine 2 was steered from machine 3 and from a phone (acceptance check 3).
	* 2026-10-17: the status panel says when it was last updated: under its Faults panel, a table of the last three times the push of these pages changed it, newest first, each as a date and a time in Pacific time and in UTC. A push that finds nothing else changed saves nothing, so the table never counts its own times as a change.		* 2026-10-17: the status panel says when it was last updated: under its Faults panel, a table of the last three times the push of these pages changed it, newest first, each as a date and a time in Pacific time and in UTC. A push that finds nothing else changed saves nothing, so the table never counts its own times as a change.
			* 2026-10-17: 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. Once that run passes, the Declarer lands the change past the one check that fails by design, with one command that sets that check aside for the merge alone and restores it.

	== Open ==		== Open ==
Line 70:		Line 71:
	Phase 0's acceptance list is closed; the Open items above carry into Phase 1 (charter section 10).		Phase 0's acceptance list is closed; the Open items above carry into Phase 1 (charter section 10).

	as of 2026-10-17		as of 2026-10-18

PMA Progress: Progress pages rendered from the Principia Machina source

2026-10-17T23:59:19Z

Progress pages rendered from the Principia Machina source

← Older revision		Revision as of 23:59, 17 October 2026
Line 64:		Line 64:
	== Open ==		== Open ==
	* The Declarer's next publish: the section maps with the Main Page's entrance to the Lean edition, and the 22 physics tool pages' titles, both recorded on Phase 1's page; neither gates an item of any phase.		* The Declarer's next publish: the section maps with the Main Page's entrance to the Lean edition, and the 22 physics tool pages' titles, both recorded on Phase 1's page; neither gates an item of any phase.
	* Test T5, a kernel checker on the host: its kit is ready.
	* v1's seed: the 33 vector corpora and their generators were found on this wiki and copied verbatim (recorded on Phase 1's page); six specification texts at the versions the charter names still wait on the Operator's copy.		* v1's seed: the 33 vector corpora and their generators were found on this wiki and copied verbatim (recorded on Phase 1's page); six specification texts at the versions the charter names still wait on the Operator's copy.

PMA Progress: Progress pages rendered from the Principia Machina source

2026-10-17T22:41:23Z

Progress pages rendered from the Principia Machina source

← Older revision		Revision as of 22:41, 17 October 2026
Line 60:		Line 60:
	* 2026-10-16: the account that keeps these pages current exists; its first unattended push is recorded on Phase 1's page.		* 2026-10-16: the account that keeps these pages current exists; its first unattended push is recorded on Phase 1's page.
	* 2026-10-17: a session served by machine 2 was steered from machine 3 and from a phone (acceptance check 3).		* 2026-10-17: a session served by machine 2 was steered from machine 3 and from a phone (acceptance check 3).
			* 2026-10-17: the status panel says when it was last updated: under its Faults panel, a table of the last three times the push of these pages changed it, newest first, each as a date and a time in Pacific time and in UTC. A push that finds nothing else changed saves nothing, so the table never counts its own times as a change.

	== Open ==		== Open ==
	* The Declarer's next publish: the section maps with the Main Page's entrance to the Lean edition, and the 22 physics tool pages' titles, both recorded on Phase 1's page; neither gates an item of any phase.		* The Declarer's next publish: the section maps with the Main Page's entrance to the Lean edition, and the 22 physics tool pages' titles, both recorded on Phase 1's page; neither gates an item of any phase.
	* Tests T2 and T3 on the wiki's host: their kit is ready; T3 also from one scheduled run.
	* Test T5, a kernel checker on the host: its kit is ready.		* Test T5, a kernel checker on the host: its kit is ready.
	* v1's seed: the 33 vector corpora and their generators were found on this wiki and copied verbatim (recorded on Phase 1's page); six specification texts at the versions the charter names still wait on the Operator's copy.		* v1's seed: the 33 vector corpora and their generators were found on this wiki and copied verbatim (recorded on Phase 1's page); six specification texts at the versions the charter names still wait on the Operator's copy.

PMA Progress: Progress pages rendered from the Principia Machina source

2026-10-17T20:02:30Z

Progress pages rendered from the Principia Machina source

← Older revision		Revision as of 20:02, 17 October 2026
Line 59:		Line 59:
	* 2026-10-16: 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: 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: the account that keeps these pages current exists; its first unattended push is recorded on Phase 1's page.		* 2026-10-16: the account that keeps these pages current exists; its first unattended push is recorded on Phase 1's page.
			* 2026-10-17: a session served by machine 2 was steered from machine 3 and from a phone (acceptance check 3).

	== Open ==		== Open ==
Line 65:		Line 66:
	* Test T5, a kernel checker on the host: its kit is ready.		* Test T5, a kernel checker on the host: its kit is ready.
	* v1's seed: the 33 vector corpora and their generators were found on this wiki and copied verbatim (recorded on Phase 1's page); six specification texts at the versions the charter names still wait on the Operator's copy.		* v1's seed: the 33 vector corpora and their generators were found on this wiki and copied verbatim (recorded on Phase 1's page); six specification texts at the versions the charter names still wait on the Operator's copy.
	* Acceptance: check 3, a session served by machine 2 steered from machine 3 and from a phone or tablet.

	== Next ==		== Next ==

	~~A session served by machine 2, steered from machine 3 and from a phone or tablet: acceptance check 3, the last open item of~~ Phase 0's acceptance list.		Phase 0's acceptance list is closed; the Open items above carry into Phase 1 (charter section 10).

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

PMA Progress: Progress pages rendered from the Principia Machina source

2026-10-17T19:52:38Z

Progress pages rendered from the Principia Machina source

← Older revision		Revision as of 19:52, 17 October 2026
Line 49:		Line 49:
	* 2026-10-14: the names check keeps a citation faithful to its source. A bibliography entry that cites an author by a published name containing a word on the private list passes only once that exact line has been reviewed and listed; any change to the line ends the exception, prose is never excepted, and an exception that no longer matches its line fails the check.		* 2026-10-14: the names check keeps a citation faithful to its source. A bibliography entry that cites an author by a published name containing a word on the private list passes only once that exact line has been reviewed and listed; any change to the line ends the exception, prose is never excepted, and an exception that no longer matches its line fails the check.
	* 2026-10-14: 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. The same publish saved the terminology page (recorded on Phase 1's page), the shared style sheet and the 71 pages of the Lean theorem prover edition, new.		* 2026-10-14: 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. The same publish saved the terminology page (recorded on Phase 1's page), the shared style sheet and the 71 pages of the Lean theorem prover edition, new.
			* 2026-10-15: 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. A direction that would add to or change the work is recorded and waits for the Declarer's own word.
	* 2026-10-15: the Declarer's choices on ten open questions, recorded in the charter: the Calculator written in Lean's core alone, without Mathlib; its SHA-256 and its Unicode normalization written in the source repository, checked against published test data and normalizing as version 1 did; the three-letter code table approved as it stands; the two kinds of Provision confirmed; every number the Calculator computes exact, each difference from version 1's floating-point rounding recorded as a divergence; the governor's admission first, its other parts after it in a recorded order; test T3's scheduled run set up on the wiki's host by the closing run, its removal left to the Operator; the eight readings of version 1's permissions table kept as built; and the agent's Lean tool pinned to one version on every machine.		* 2026-10-15: the Declarer's choices on ten open questions, recorded in the charter: the Calculator written in Lean's core alone, without Mathlib; its SHA-256 and its Unicode normalization written in the source repository, checked against published test data and normalizing as version 1 did; the three-letter code table approved as it stands; the two kinds of Provision confirmed; every number the Calculator computes exact, each difference from version 1's floating-point rounding recorded as a divergence; the governor's admission first, its other parts after it in a recorded order; test T3's scheduled run set up on the wiki's host by the closing run, its removal left to the Operator; the eight readings of version 1's permissions table kept as built; and the agent's Lean tool pinned to one version on every machine.
	* 2026-10-15: one command, the Declarer's, now lands the finished changes: each change whose checks all pass joins the main line, in the order the changes build on one another, and a change that does not pass is set aside with every change built on it, each named with the reason.		* 2026-10-15: one command, the Declarer's, now lands the finished changes: each change whose checks all pass joins the main line, in the order the changes build on one another, and a change that does not pass is set aside with every change built on it, each named with the reason.