Principia Machina/Progress/Phase 1 - Revision history

PMA Progress: Progress pages rendered from the Principia Machina source

2026-10-21T02:50:28Z

Progress pages rendered from the Principia Machina source

← Older revision		Revision as of 02:50, 21 October 2026
Line 31:		Line 31:
	* 2026-10-18: test T3 on the wiki's host, from one scheduled run: 100 of 100 calls failed (call 1: exit -1); the whole run (PHP, MediaWiki's setup and every child) used 1.418 CPU-seconds, under the budget of 400 (10 per cent of an hourly cap of 4000): FAIL.		* 2026-10-18: test T3 on the wiki's host, from one scheduled run: 100 of 100 calls failed (call 1: exit -1); the whole run (PHP, MediaWiki's setup and every child) used 1.418 CPU-seconds, under the budget of 400 (10 per cent of an hourly cap of 4000): FAIL.
	* 2026-10-18: 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. The line above for the run of 2026-10-18 and its row on the status panel named only the time and the cap, so they read as a budget failure that did not happen; a new step of the closing run reads that run's kept record again, changing nothing on the host, and corrects both. A further step, run only on the Declarer's choice and a typed yes, lets the standing scheduled run make the calls again.		* 2026-10-18: 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. The line above for the run of 2026-10-18 and its row on the status panel named only the time and the cap, so they read as a budget failure that did not happen; a new step of the closing run reads that run's kept record again, changing nothing on the host, and corrects both. A further step, run only on the Declarer's choice and a typed yes, lets the standing scheduled run make the calls again.
			* 2026-10-19: tests T1, T2, T3 and T5 run again on a server the Operator controls, built from nothing by one provisioning script: every test passes. Test T3's hundred calls pass from the shell, from a scheduled run and under the job runner's limits, 0 of 100 failing each time; every context the wiki starts a program from now admits the address space the Calculator reserves.
	* 2026-10-19: the design for how the wiki's calculation jobs are started, written up after the scheduled run of test T3 failed: the calculator is started from a context whose limits admit the address space it reserves, by a trigger sent from outside the wiki's host over one connection held open, while the work, its budget and the check of the program's digest stay on the host. Five choices in it go to the Declarer; nothing is built until he answers.		* 2026-10-19: the design for how the wiki's calculation jobs are started, written up after the scheduled run of test T3 failed: the calculator is started from a context whose limits admit the address space it reserves, by a trigger sent from outside the wiki's host over one connection held open, while the work, its budget and the check of the program's digest stay on the host. Five choices in it go to the Declarer; nothing is built until he answers.
	* 2026-10-20: every place that builds the library now fetches the community mathematics library's compiled files before building, when the library depends on it; the dependency itself follows.		* 2026-10-20: every place that builds the library now fetches the community mathematics library's compiled files before building, when the library depends on it; the dependency itself follows.
			* 2026-10-21: the wiki moved to the server the Operator controls. Its database and its uploads were copied whole and checked row for row against the old host before the switch: every count, the hidden revisions and every upload's checksum equal. The old host was kept read-only during the move and is no longer the wiki's home.

	== Open ==		== Open ==

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 32:		Line 32:
	* 2026-10-18: 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. The line above for the run of 2026-10-18 and its row on the status panel named only the time and the cap, so they read as a budget failure that did not happen; a new step of the closing run reads that run's kept record again, changing nothing on the host, and corrects both. A further step, run only on the Declarer's choice and a typed yes, lets the standing scheduled run make the calls again.		* 2026-10-18: 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. The line above for the run of 2026-10-18 and its row on the status panel named only the time and the cap, so they read as a budget failure that did not happen; a new step of the closing run reads that run's kept record again, changing nothing on the host, and corrects both. A further step, run only on the Declarer's choice and a typed yes, lets the standing scheduled run make the calls again.
	* 2026-10-19: the design for how the wiki's calculation jobs are started, written up after the scheduled run of test T3 failed: the calculator is started from a context whose limits admit the address space it reserves, by a trigger sent from outside the wiki's host over one connection held open, while the work, its budget and the check of the program's digest stay on the host. Five choices in it go to the Declarer; nothing is built until he answers.		* 2026-10-19: the design for how the wiki's calculation jobs are started, written up after the scheduled run of test T3 failed: the calculator is started from a context whose limits admit the address space it reserves, by a trigger sent from outside the wiki's host over one connection held open, while the work, its budget and the check of the program's digest stay on the host. Five choices in it go to the Declarer; nothing is built until he answers.
			* 2026-10-20: every place that builds the library now fetches the community mathematics library's compiled files before building, when the library depends on it; the dependency itself follows.

	== Open ==		== Open ==
Line 40:		Line 41:
	Tests T2, T3 and T5 as the Operator runs them on the wiki's host; the Declarer's approval of the three-letter code table.		Tests T2, T3 and T5 as the Operator runs them on the wiki's host; the Declarer's approval of the three-letter code table.

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

PMA Progress: Progress pages rendered from the Principia Machina source

2026-10-19T19:52:28Z

Progress pages rendered from the Principia Machina source

← Older revision		Revision as of 19:52, 19 October 2026
Line 31:		Line 31:
	* 2026-10-18: test T3 on the wiki's host, from one scheduled run: 100 of 100 calls failed (call 1: exit -1); the whole run (PHP, MediaWiki's setup and every child) used 1.418 CPU-seconds, under the budget of 400 (10 per cent of an hourly cap of 4000): FAIL.		* 2026-10-18: test T3 on the wiki's host, from one scheduled run: 100 of 100 calls failed (call 1: exit -1); the whole run (PHP, MediaWiki's setup and every child) used 1.418 CPU-seconds, under the budget of 400 (10 per cent of an hourly cap of 4000): FAIL.
	* 2026-10-18: 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. The line above for the run of 2026-10-18 and its row on the status panel named only the time and the cap, so they read as a budget failure that did not happen; a new step of the closing run reads that run's kept record again, changing nothing on the host, and corrects both. A further step, run only on the Declarer's choice and a typed yes, lets the standing scheduled run make the calls again.		* 2026-10-18: 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. The line above for the run of 2026-10-18 and its row on the status panel named only the time and the cap, so they read as a budget failure that did not happen; a new step of the closing run reads that run's kept record again, changing nothing on the host, and corrects both. A further step, run only on the Declarer's choice and a typed yes, lets the standing scheduled run make the calls again.
			* 2026-10-19: the design for how the wiki's calculation jobs are started, written up after the scheduled run of test T3 failed: the calculator is started from a context whose limits admit the address space it reserves, by a trigger sent from outside the wiki's host over one connection held open, while the work, its budget and the check of the program's digest stay on the host. Five choices in it go to the Declarer; nothing is built until he answers.

	== Open ==		== Open ==

PMA Progress: Progress pages rendered from the Principia Machina source

2026-10-19T02:15:45Z

Progress pages rendered from the Principia Machina source

← Older revision		Revision as of 02:15, 19 October 2026
Line 29:		Line 29:
	* 2026-10-17: version 1's named texts copied from the Operator's copy: the full source of version 1's server extension at 0.6.0; four declarations files; each checked against the digest the project holds where it holds one.		* 2026-10-17: version 1's named texts copied from the Operator's copy: the full source of version 1's server extension at 0.6.0; four declarations files; each checked against the digest the project holds where it holds one.
	* 2026-10-18: version 1's named texts copied from the Operator's copy: the six specification texts at the versions the charter names; the full source of version 1's server extension at 0.6.0; the full source of its research client at 0.1.1; six declarations files; each checked against the digest the project holds where it holds one.		* 2026-10-18: version 1's named texts copied from the Operator's copy: the six specification texts at the versions the charter names; the full source of version 1's server extension at 0.6.0; the full source of its research client at 0.1.1; six declarations files; each checked against the digest the project holds where it holds one.
	* 2026-10-18: test T3 on the wiki's host, from one scheduled run: 100 calls ~~took~~ 1.418 CPU-seconds ~~together~~, ~~against~~ 10 per cent of an hourly cap of 4000 ~~CPU-seconds~~: FAIL.		* 2026-10-18: test T3 on the wiki's host, from one scheduled run: 100 of 100 calls failed (call 1: exit -1); the whole run (PHP, MediaWiki's setup and every child) used 1.418 CPU-seconds, under the budget of 400 (10 per cent of an hourly cap of 4000): FAIL.
	* 2026-10-18: 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. The line above for the run of 2026-10-18 and its row on the status panel named only the time and the cap, so they read as a budget failure that did not happen; a new step of the closing run reads that run's kept record again, changing nothing on the host, and corrects both. A further step, run only on the Declarer's choice and a typed yes, lets the standing scheduled run make the calls again.		* 2026-10-18: 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. The line above for the run of 2026-10-18 and its row on the status panel named only the time and the cap, so they read as a budget failure that did not happen; a new step of the closing run reads that run's kept record again, changing nothing on the host, and corrects both. A further step, run only on the Declarer's choice and a typed yes, lets the standing scheduled run make the calls again.

PMA Progress: Progress pages rendered from the Principia Machina source

2026-10-19T01:23:39Z

Progress pages rendered from the Principia Machina source

← Older revision		Revision as of 01:23, 19 October 2026
Line 30:		Line 30:
	* 2026-10-18: version 1's named texts copied from the Operator's copy: the six specification texts at the versions the charter names; the full source of version 1's server extension at 0.6.0; the full source of its research client at 0.1.1; six declarations files; each checked against the digest the project holds where it holds one.		* 2026-10-18: version 1's named texts copied from the Operator's copy: the six specification texts at the versions the charter names; the full source of version 1's server extension at 0.6.0; the full source of its research client at 0.1.1; six declarations files; each checked against the digest the project holds where it holds one.
	* 2026-10-18: test T3 on the wiki's host, from one scheduled run: 100 calls took 1.418 CPU-seconds together, against 10 per cent of an hourly cap of 4000 CPU-seconds: FAIL.		* 2026-10-18: test T3 on the wiki's host, from one scheduled run: 100 calls took 1.418 CPU-seconds together, against 10 per cent of an hourly cap of 4000 CPU-seconds: FAIL.
			* 2026-10-18: 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. The line above for the run of 2026-10-18 and its row on the status panel named only the time and the cap, so they read as a budget failure that did not happen; a new step of the closing run reads that run's kept record again, changing nothing on the host, and corrects both. A further step, run only on the Declarer's choice and a typed yes, lets the standing scheduled run make the calls again.

	== Open ==		== Open ==

PMA Progress: Progress pages rendered from the Principia Machina source

2026-10-19T00:07:31Z

Progress pages rendered from the Principia Machina source

← Older revision		Revision as of 00:07, 19 October 2026
Line 38:		Line 38:
	Tests T2, T3 and T5 as the Operator runs them on the wiki's host; the Declarer's approval of the three-letter code table.		Tests T2, T3 and T5 as the Operator runs them on the wiki's host; the Declarer's approval of the three-letter code table.

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

PMA Progress: Progress pages rendered from the Principia Machina source

2026-10-18T16:08:51Z

Progress pages rendered from the Principia Machina source

← Older revision		Revision as of 16:08, 18 October 2026
Line 29:		Line 29:
	* 2026-10-17: version 1's named texts copied from the Operator's copy: the full source of version 1's server extension at 0.6.0; four declarations files; each checked against the digest the project holds where it holds one.		* 2026-10-17: version 1's named texts copied from the Operator's copy: the full source of version 1's server extension at 0.6.0; four declarations files; each checked against the digest the project holds where it holds one.
	* 2026-10-18: version 1's named texts copied from the Operator's copy: the six specification texts at the versions the charter names; the full source of version 1's server extension at 0.6.0; the full source of its research client at 0.1.1; six declarations files; each checked against the digest the project holds where it holds one.		* 2026-10-18: version 1's named texts copied from the Operator's copy: the six specification texts at the versions the charter names; the full source of version 1's server extension at 0.6.0; the full source of its research client at 0.1.1; six declarations files; each checked against the digest the project holds where it holds one.
			* 2026-10-18: test T3 on the wiki's host, from one scheduled run: 100 calls took 1.418 CPU-seconds together, against 10 per cent of an hourly cap of 4000 CPU-seconds: FAIL.

	== Open ==		== Open ==
	* The monthly survey of Lean's toolchain: set up; its first run falls on 2026-10-22.		* The monthly survey of Lean's toolchain: set up; its first run falls on 2026-10-22.
	* Test T3 from one scheduled run on the wiki's host, which the closing run can set up there, its removal left to the Operator; its run from the shell is recorded.

	== Next ==		== Next ==

PMA Progress: Progress pages rendered from the Principia Machina source

2026-10-18T15:43:56Z

Progress pages rendered from the Principia Machina source

← Older revision		Revision as of 15:43, 18 October 2026
Line 28:		Line 28:
	* 2026-10-17: test T5 on the wiki's host, under the wiki's command framework from the command line: an independent Lean kernel checker took 0.083 CPU-seconds (84 ms) on one of the library's theorems with everything it depends on (528 items), which it accepted; a copy with the statement altered was refused, and a copy whose proof is an unpermitted axiom was refused (pass: under 2 CPU-seconds): PASS.		* 2026-10-17: test T5 on the wiki's host, under the wiki's command framework from the command line: an independent Lean kernel checker took 0.083 CPU-seconds (84 ms) on one of the library's theorems with everything it depends on (528 items), which it accepted; a copy with the statement altered was refused, and a copy whose proof is an unpermitted axiom was refused (pass: under 2 CPU-seconds): PASS.
	* 2026-10-17: version 1's named texts copied from the Operator's copy: the full source of version 1's server extension at 0.6.0; four declarations files; each checked against the digest the project holds where it holds one.		* 2026-10-17: version 1's named texts copied from the Operator's copy: the full source of version 1's server extension at 0.6.0; four declarations files; each checked against the digest the project holds where it holds one.
			* 2026-10-18: version 1's named texts copied from the Operator's copy: the six specification texts at the versions the charter names; the full source of version 1's server extension at 0.6.0; the full source of its research client at 0.1.1; six declarations files; each checked against the digest the project holds where it holds one.

	== Open ==		== Open ==
	* The monthly survey of Lean's toolchain: set up; its first run falls on 2026-10-22.		* The monthly survey of Lean's toolchain: set up; its first run falls on 2026-10-22.
	* Test T3 from one scheduled run on the wiki's host, which the closing run can set up there, its removal left to the Operator; its run from the shell is recorded.		* Test T3 from one scheduled run on the wiki's host, which the closing run can set up there, its removal left to the Operator; its run from the shell is recorded.
	* Version 1's specification texts at the versions the charter names: six of them still wait on the Operator's copy, as does the full source of version 1's research client.

	== Next ==		== Next ==

PMA Progress: Progress pages rendered from the Principia Machina source

2026-10-18T01:13:35Z

Progress pages rendered from the Principia Machina source

← Older revision		Revision as of 01:13, 18 October 2026
Line 27:		Line 27:
	* 2026-10-15: 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: it adds the one line the test needs to the host's list of scheduled runs only when no line there runs the test already, shows the line and the change and asks before writing, and leaves every other line as it is. Removing the line after the run stays the Operator's.		* 2026-10-15: 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: it adds the one line the test needs to the host's list of scheduled runs only when no line there runs the test already, shows the line and the change and asks before writing, and leaves every other line as it is. Removing the line after the run stays the Operator's.
	* 2026-10-17: test T5 on the wiki's host, under the wiki's command framework from the command line: an independent Lean kernel checker took 0.083 CPU-seconds (84 ms) on one of the library's theorems with everything it depends on (528 items), which it accepted; a copy with the statement altered was refused, and a copy whose proof is an unpermitted axiom was refused (pass: under 2 CPU-seconds): PASS.		* 2026-10-17: test T5 on the wiki's host, under the wiki's command framework from the command line: an independent Lean kernel checker took 0.083 CPU-seconds (84 ms) on one of the library's theorems with everything it depends on (528 items), which it accepted; a copy with the statement altered was refused, and a copy whose proof is an unpermitted axiom was refused (pass: under 2 CPU-seconds): PASS.
			* 2026-10-17: version 1's named texts copied from the Operator's copy: the full source of version 1's server extension at 0.6.0; four declarations files; each checked against the digest the project holds where it holds one.

	== Open ==		== Open ==
	* Version 1's specification texts at the versions the charter names: six of them are not on the public wiki and wait on the Operator's copy, as do version 1's server extension in full and its research client.
	* The monthly survey of Lean's toolchain: set up; its first run falls on 2026-10-22.		* The monthly survey of Lean's toolchain: set up; its first run falls on 2026-10-22.
	* Test T3 from one scheduled run on the wiki's host, which the closing run can set up there, its removal left to the Operator; its run from the shell is recorded.		* Test T3 from one scheduled run on the wiki's host, which the closing run can set up there, its removal left to the Operator; its run from the shell is recorded.
			* Version 1's specification texts at the versions the charter names: six of them still wait on the Operator's copy, as does the full source of version 1's research client.

	== Next ==		== Next ==
Line 37:		Line 38:
	Tests T2, T3 and T5 as the Operator runs them on the wiki's host; the Declarer's approval of the three-letter code table.		Tests T2, T3 and T5 as the Operator runs them on the wiki's host; the Declarer's approval of the three-letter code table.

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

PMA Progress: Progress pages rendered from the Principia Machina source

2026-10-17T23:59:20Z

Progress pages rendered from the Principia Machina source

← Older revision		Revision as of 23:59, 17 October 2026
Line 26:		Line 26:
	* 2026-10-17: test T3 on the wiki's host, from the shell: 100 calls in one run took 7.432 CPU-seconds together, against 10 per cent of an hourly cap of 4000 CPU-seconds: PASS; its scheduled run follows.		* 2026-10-17: test T3 on the wiki's host, from the shell: 100 calls in one run took 7.432 CPU-seconds together, against 10 per cent of an hourly cap of 4000 CPU-seconds: PASS; its scheduled run follows.
	* 2026-10-15: 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: it adds the one line the test needs to the host's list of scheduled runs only when no line there runs the test already, shows the line and the change and asks before writing, and leaves every other line as it is. Removing the line after the run stays the Operator's.		* 2026-10-15: 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: it adds the one line the test needs to the host's list of scheduled runs only when no line there runs the test already, shows the line and the change and asks before writing, and leaves every other line as it is. Removing the line after the run stays the Operator's.
			* 2026-10-17: test T5 on the wiki's host, under the wiki's command framework from the command line: an independent Lean kernel checker took 0.083 CPU-seconds (84 ms) on one of the library's theorems with everything it depends on (528 items), which it accepted; a copy with the statement altered was refused, and a copy whose proof is an unpermitted axiom was refused (pass: under 2 CPU-seconds): PASS.

	== Open ==		== Open ==
	* Version 1's specification texts at the versions the charter names: six of them are not on the public wiki and wait on the Operator's copy, as do version 1's server extension in full and its research client.		* Version 1's specification texts at the versions the charter names: six of them are not on the public wiki and wait on the Operator's copy, as do version 1's server extension in full and its research client.
	* The monthly survey of Lean's toolchain: set up; its first run falls on 2026-10-22.		* The monthly survey of Lean's toolchain: set up; its first run falls on 2026-10-22.
	* ~~Test T5 on the wiki's host, run by the Operator from the closing run; its kit is ready.~~ Test T3 from one scheduled run on the wiki's host, which the closing run can set up there, its removal left to the Operator; its run from the shell is recorded~~. T5 checks a proof with a Lean kernel written independently of Lean's own~~.		* Test T3 from one scheduled run on the wiki's host, which the closing run can set up there, its removal left to the Operator; its run from the shell is recorded.

	== Next ==		== Next ==