diff --git a/.github/workflows/check-now-freshness.yml b/.github/workflows/check-now-freshness.yml index dda23e3432..6589d8d0b0 100644 --- a/.github/workflows/check-now-freshness.yml +++ b/.github/workflows/check-now-freshness.yml @@ -13,8 +13,29 @@ jobs: runs-on: ubuntu-latest steps: - uses: actions/checkout@v6 + with: + fetch-depth: 0 - - name: Check freshness - run: | - # Add freshness check logic here in future - echo "Checking repository freshness..." + # This job's name, `check`, is one of four required by the + # t27-master-protection ruleset. Its only step used to be + # + # # Add freshness check logic here in future + # echo "Checking repository freshness..." + # + # so one of the four gates protecting master asserted nothing, and had + # passed every pull request it ever ran on. The ruleset is not this + # file's to edit, so the job keeps its required name and is given + # something real to do. + # + # NOW Sync Gate already requires that an entry was ADDED; it does not + # read it. The two are complementary: + # NOW Sync Gate -> "you wrote one" + # this -> "what you wrote says something" + - name: Negative control + run: python3 tools/check_now_entry_shape.py --self-check + + - name: The docs/now/ entry this PR adds must say something + env: + PR_BASE_SHA: ${{ github.event.pull_request.base.sha }} + PR_HEAD_SHA: ${{ github.event.pull_request.head.sha }} + run: python3 tools/check_now_entry_shape.py diff --git a/docs/now/2026-08-28-one-of-the-four-checks-protecting-master-was-an-echo.md b/docs/now/2026-08-28-one-of-the-four-checks-protecting-master-was-an-echo.md new file mode 100644 index 0000000000..d6aca61fb3 --- /dev/null +++ b/docs/now/2026-08-28-one-of-the-four-checks-protecting-master-was-an-echo.md @@ -0,0 +1,8 @@ +# NOW -- One of the four checks protecting master was an echo (2026-08-28) + +## One of the four checks protecting master was an echo (Refs #2754) + +- t27-master-protection requires check-now-freshness, validate, check, check-linked-issue -- and the job named `check` ran one step: echo, with a comment saying add logic here in future +- it passed every pull request it ever ran on, and its green meant nothing +- the ruleset is not mine to edit, so the job keeps its required name and now asserts that the docs/now entry a PR adds is well formed -- which NOW Sync Gate, which only checks that one was added, does not read +- zero entries is a FAILURE here, not a pass: a check that reports success over an empty set is the shape being replaced diff --git a/proofs/lean4/.trinity/seals/coder_igla-coder-arch.json b/proofs/lean4/.trinity/seals/coder_igla-coder-arch.json index 1a2a991ffd..999f0774dd 100644 --- a/proofs/lean4/.trinity/seals/coder_igla-coder-arch.json +++ b/proofs/lean4/.trinity/seals/coder_igla-coder-arch.json @@ -7,5 +7,5 @@ "ring": 12, "sealed_at": "2026-06-23T07:33:23Z", "spec_hash": "sha256:27f7e12ea1ab7b143531a411ccb3e0db1d62be92134f3315988594aa767e2344", - "spec_path": "/Users/playra/t27/specs/igla/coder/arch.t27" -} \ No newline at end of file + "spec_path": "specs/igla/coder/arch.t27" +} diff --git a/proofs/lean4/.trinity/seals/coder_igla-coder-bench-proxy.json b/proofs/lean4/.trinity/seals/coder_igla-coder-bench-proxy.json index b79945ddd2..fc306b4e80 100644 --- a/proofs/lean4/.trinity/seals/coder_igla-coder-bench-proxy.json +++ b/proofs/lean4/.trinity/seals/coder_igla-coder-bench-proxy.json @@ -7,5 +7,5 @@ "ring": 12, "sealed_at": "2026-06-23T07:33:23Z", "spec_hash": "sha256:ce043dc4d90da4e1a979d75e248f85f218c3a035ebf3018c83faeee51c2218db", - "spec_path": "/Users/playra/t27/specs/igla/coder/bench_proxy.t27" -} \ No newline at end of file + "spec_path": "specs/igla/coder/bench_proxy.t27" +} diff --git a/proofs/lean4/.trinity/seals/coder_igla-coder-benchmark.json b/proofs/lean4/.trinity/seals/coder_igla-coder-benchmark.json index bc234e9d04..f652e7b90e 100644 --- a/proofs/lean4/.trinity/seals/coder_igla-coder-benchmark.json +++ b/proofs/lean4/.trinity/seals/coder_igla-coder-benchmark.json @@ -7,5 +7,5 @@ "ring": 12, "sealed_at": "2026-06-23T07:33:23Z", "spec_hash": "sha256:afce874ad5ea6d926adecae1bc996369d3f5aa96df1e9351517a993db8b333b2", - "spec_path": "/Users/playra/t27/specs/igla/coder/benchmark.t27" -} \ No newline at end of file + "spec_path": "specs/igla/coder/benchmark.t27" +} diff --git a/proofs/lean4/.trinity/seals/coder_igla-coder-dataset.json b/proofs/lean4/.trinity/seals/coder_igla-coder-dataset.json index ad36fa6b62..6b4f8beed9 100644 --- a/proofs/lean4/.trinity/seals/coder_igla-coder-dataset.json +++ b/proofs/lean4/.trinity/seals/coder_igla-coder-dataset.json @@ -7,5 +7,5 @@ "ring": 12, "sealed_at": "2026-06-23T07:33:23Z", "spec_hash": "sha256:f6577284f166b60ee93dc4cf5a199e9db5c7024e90958d888da573f2fe0272e7", - "spec_path": "/Users/playra/t27/specs/igla/coder/dataset.t27" -} \ No newline at end of file + "spec_path": "specs/igla/coder/dataset.t27" +} diff --git a/proofs/lean4/.trinity/seals/coder_igla-coder-eval.json b/proofs/lean4/.trinity/seals/coder_igla-coder-eval.json index 8387dce633..9896a4852a 100644 --- a/proofs/lean4/.trinity/seals/coder_igla-coder-eval.json +++ b/proofs/lean4/.trinity/seals/coder_igla-coder-eval.json @@ -7,5 +7,5 @@ "ring": 12, "sealed_at": "2026-06-23T07:33:23Z", "spec_hash": "sha256:e476f20c37723ae197b73a5d40bd767bb6924a1a1dd5f32e84ab243529cc8afd", - "spec_path": "/Users/playra/t27/specs/igla/coder/eval.t27" -} \ No newline at end of file + "spec_path": "specs/igla/coder/eval.t27" +} diff --git a/proofs/lean4/.trinity/seals/coder_igla-coder-pipeline.json b/proofs/lean4/.trinity/seals/coder_igla-coder-pipeline.json index 9c7bafea36..42c094514e 100644 --- a/proofs/lean4/.trinity/seals/coder_igla-coder-pipeline.json +++ b/proofs/lean4/.trinity/seals/coder_igla-coder-pipeline.json @@ -7,5 +7,5 @@ "ring": 12, "sealed_at": "2026-06-23T07:33:23Z", "spec_hash": "sha256:df8eeb58a4866d76d9372221a73cbc7d52244e568601e04effe8ab8952d8df34", - "spec_path": "/Users/playra/t27/specs/igla/coder/pipeline.t27" -} \ No newline at end of file + "spec_path": "specs/igla/coder/pipeline.t27" +} diff --git a/proofs/lean4/.trinity/seals/coder_igla-coder-prm.json b/proofs/lean4/.trinity/seals/coder_igla-coder-prm.json index de53d19ee0..591a41ba4a 100644 --- a/proofs/lean4/.trinity/seals/coder_igla-coder-prm.json +++ b/proofs/lean4/.trinity/seals/coder_igla-coder-prm.json @@ -7,5 +7,5 @@ "ring": 12, "sealed_at": "2026-06-23T07:33:23Z", "spec_hash": "sha256:3000719354d4a3cc9992502860a0a4f1ea2570c4ebb4952afc77d9ba9fa8c0ea", - "spec_path": "/Users/playra/t27/specs/igla/coder/prm.t27" -} \ No newline at end of file + "spec_path": "specs/igla/coder/prm.t27" +} diff --git a/proofs/lean4/.trinity/seals/coder_igla-coder-tokenizer.json b/proofs/lean4/.trinity/seals/coder_igla-coder-tokenizer.json index 2a5634eb2e..3084b6ec15 100644 --- a/proofs/lean4/.trinity/seals/coder_igla-coder-tokenizer.json +++ b/proofs/lean4/.trinity/seals/coder_igla-coder-tokenizer.json @@ -7,5 +7,5 @@ "ring": 12, "sealed_at": "2026-06-23T07:33:23Z", "spec_hash": "sha256:a082bceb80b41d6207340fb74d39e61b10de5d88dae7047b629b03adc2cf3fe6", - "spec_path": "/Users/playra/t27/specs/igla/coder/tokenizer.t27" -} \ No newline at end of file + "spec_path": "specs/igla/coder/tokenizer.t27" +} diff --git a/proofs/lean4/.trinity/seals/coder_igla-coder-training.json b/proofs/lean4/.trinity/seals/coder_igla-coder-training.json index b6a0668b9f..7918e91199 100644 --- a/proofs/lean4/.trinity/seals/coder_igla-coder-training.json +++ b/proofs/lean4/.trinity/seals/coder_igla-coder-training.json @@ -7,5 +7,5 @@ "ring": 12, "sealed_at": "2026-06-23T07:33:23Z", "spec_hash": "sha256:b6af78e0d33e9602cb98e00de6c18ee6068b624af4dc0d0b925e3284f1d07280", - "spec_path": "/Users/playra/t27/specs/igla/coder/training.t27" -} \ No newline at end of file + "spec_path": "specs/igla/coder/training.t27" +} diff --git a/proofs/lean4/.trinity/seals/coder_igla-coder-weights.json b/proofs/lean4/.trinity/seals/coder_igla-coder-weights.json index 4f45f2fe93..b2fbae4189 100644 --- a/proofs/lean4/.trinity/seals/coder_igla-coder-weights.json +++ b/proofs/lean4/.trinity/seals/coder_igla-coder-weights.json @@ -7,5 +7,5 @@ "ring": 12, "sealed_at": "2026-06-23T07:33:23Z", "spec_hash": "sha256:bc792f4def7a9cbc149706e8f0df32eca7e7f07b00ff726881da4c1b3c5b1326", - "spec_path": "/Users/playra/t27/specs/igla/coder/weights.t27" -} \ No newline at end of file + "spec_path": "specs/igla/coder/weights.t27" +} diff --git a/proofs/lean4/.trinity/seals/race_igla-race-adder-tree.json b/proofs/lean4/.trinity/seals/race_igla-race-adder-tree.json index 9b0d88de79..cb1ece3faa 100644 --- a/proofs/lean4/.trinity/seals/race_igla-race-adder-tree.json +++ b/proofs/lean4/.trinity/seals/race_igla-race-adder-tree.json @@ -7,5 +7,5 @@ "ring": 12, "sealed_at": "2026-06-23T07:33:22Z", "spec_hash": "sha256:f357b3492de44f19257be21e9d5a75405e595e27d1f70a923538e6d065d7490b", - "spec_path": "/Users/playra/t27/specs/igla/race/adder_tree.t27" -} \ No newline at end of file + "spec_path": "specs/igla/race/adder_tree.t27" +} diff --git a/proofs/lean4/.trinity/seals/race_igla-race-backend.json b/proofs/lean4/.trinity/seals/race_igla-race-backend.json index 6cfe2d7837..0cbe51afc1 100644 --- a/proofs/lean4/.trinity/seals/race_igla-race-backend.json +++ b/proofs/lean4/.trinity/seals/race_igla-race-backend.json @@ -7,5 +7,5 @@ "ring": 12, "sealed_at": "2026-06-23T07:33:22Z", "spec_hash": "sha256:1b46e3170c8fa50ca98145dd6791c16c85f9d3688678982ac213e39522620129", - "spec_path": "/Users/playra/t27/specs/igla/race/backend.t27" -} \ No newline at end of file + "spec_path": "specs/igla/race/backend.t27" +} diff --git a/proofs/lean4/.trinity/seals/race_igla-race-bram-weights.json b/proofs/lean4/.trinity/seals/race_igla-race-bram-weights.json index f471c4a6cc..1f7bfdca6f 100644 --- a/proofs/lean4/.trinity/seals/race_igla-race-bram-weights.json +++ b/proofs/lean4/.trinity/seals/race_igla-race-bram-weights.json @@ -7,5 +7,5 @@ "ring": 12, "sealed_at": "2026-06-23T07:33:22Z", "spec_hash": "sha256:a15d813aa989904c22ed27ea4849db3f61165c6f8f239cb547e97468602d3795", - "spec_path": "/Users/playra/t27/specs/igla/race/bram_weights.t27" -} \ No newline at end of file + "spec_path": "specs/igla/race/bram_weights.t27" +} diff --git a/proofs/lean4/.trinity/seals/race_igla-race-cordic-fixed.json b/proofs/lean4/.trinity/seals/race_igla-race-cordic-fixed.json index c986af2c89..d1f2de9aa1 100644 --- a/proofs/lean4/.trinity/seals/race_igla-race-cordic-fixed.json +++ b/proofs/lean4/.trinity/seals/race_igla-race-cordic-fixed.json @@ -7,5 +7,5 @@ "ring": 12, "sealed_at": "2026-06-23T07:33:22Z", "spec_hash": "sha256:08e4b454cd08143b5f79ac7da87c31536c5a528bffd448ccc8832887bbd30b9e", - "spec_path": "/Users/playra/t27/specs/igla/race/cordic_fixed.t27" -} \ No newline at end of file + "spec_path": "specs/igla/race/cordic_fixed.t27" +} diff --git a/proofs/lean4/.trinity/seals/race_igla-race-cordic-top.json b/proofs/lean4/.trinity/seals/race_igla-race-cordic-top.json index 20aa091aa9..3c60169317 100644 --- a/proofs/lean4/.trinity/seals/race_igla-race-cordic-top.json +++ b/proofs/lean4/.trinity/seals/race_igla-race-cordic-top.json @@ -7,5 +7,5 @@ "ring": 12, "sealed_at": "2026-06-23T07:33:22Z", "spec_hash": "sha256:e1fe99a177a63e2d7ac365bd3e3d068b0a9380759aac5d9f03b185be66c0ceb7", - "spec_path": "/Users/playra/t27/specs/igla/race/cordic_top.t27" -} \ No newline at end of file + "spec_path": "specs/igla/race/cordic_top.t27" +} diff --git a/proofs/lean4/.trinity/seals/race_igla-race-cordic.json b/proofs/lean4/.trinity/seals/race_igla-race-cordic.json index 390f96bd5d..c8c43c1bc8 100644 --- a/proofs/lean4/.trinity/seals/race_igla-race-cordic.json +++ b/proofs/lean4/.trinity/seals/race_igla-race-cordic.json @@ -7,5 +7,5 @@ "ring": 12, "sealed_at": "2026-06-23T07:33:22Z", "spec_hash": "sha256:dee80f800e7efb377e3383e20771609f7d5c88c9ce9e0193e805634863243eab", - "spec_path": "/Users/playra/t27/specs/igla/race/cordic.t27" -} \ No newline at end of file + "spec_path": "specs/igla/race/cordic.t27" +} diff --git a/proofs/lean4/.trinity/seals/race_igla-race-eda.json b/proofs/lean4/.trinity/seals/race_igla-race-eda.json index 88adf3a4a2..c7d94c162d 100644 --- a/proofs/lean4/.trinity/seals/race_igla-race-eda.json +++ b/proofs/lean4/.trinity/seals/race_igla-race-eda.json @@ -7,5 +7,5 @@ "ring": 12, "sealed_at": "2026-06-23T07:33:22Z", "spec_hash": "sha256:c01f0dc9d0c38f565e301ee40a21286f30331ab738ed7f82a5c924123cce25cd", - "spec_path": "/Users/playra/t27/specs/igla/race/eda.t27" -} \ No newline at end of file + "spec_path": "specs/igla/race/eda.t27" +} diff --git a/proofs/lean4/.trinity/seals/race_igla-race-formal.json b/proofs/lean4/.trinity/seals/race_igla-race-formal.json index 1e58220ae7..77545f6f76 100644 --- a/proofs/lean4/.trinity/seals/race_igla-race-formal.json +++ b/proofs/lean4/.trinity/seals/race_igla-race-formal.json @@ -7,5 +7,5 @@ "ring": 12, "sealed_at": "2026-06-23T07:33:22Z", "spec_hash": "sha256:f1da7838010c0a72c70e64fd37c642c66fca4bba0285268151d7dc865f12f4aa", - "spec_path": "/Users/playra/t27/specs/igla/race/formal.t27" -} \ No newline at end of file + "spec_path": "specs/igla/race/formal.t27" +} diff --git a/proofs/lean4/.trinity/seals/race_igla-race-gemm.json b/proofs/lean4/.trinity/seals/race_igla-race-gemm.json index ffc8f79fa0..51a9eca0ec 100644 --- a/proofs/lean4/.trinity/seals/race_igla-race-gemm.json +++ b/proofs/lean4/.trinity/seals/race_igla-race-gemm.json @@ -7,5 +7,5 @@ "ring": 12, "sealed_at": "2026-06-23T07:33:23Z", "spec_hash": "sha256:d25ab7cbd58320b007f12d8b3f0fc2274c1e72745d8a9ad5c9678a2bddb8a4e3", - "spec_path": "/Users/playra/t27/specs/igla/race/gemm.t27" -} \ No newline at end of file + "spec_path": "specs/igla/race/gemm.t27" +} diff --git a/proofs/lean4/.trinity/seals/race_igla-race-opcodes.json b/proofs/lean4/.trinity/seals/race_igla-race-opcodes.json index 5b4eb50ec5..3bcab1e3f4 100644 --- a/proofs/lean4/.trinity/seals/race_igla-race-opcodes.json +++ b/proofs/lean4/.trinity/seals/race_igla-race-opcodes.json @@ -7,5 +7,5 @@ "ring": 12, "sealed_at": "2026-06-23T07:33:23Z", "spec_hash": "sha256:a16d4c6eaa9b2d1c6666e3936ec1c5e0f1b46fb3daf782d16bfd00c8ce0c5af9", - "spec_path": "/Users/playra/t27/specs/igla/race/opcodes.t27" -} \ No newline at end of file + "spec_path": "specs/igla/race/opcodes.t27" +} diff --git a/proofs/lean4/.trinity/seals/race_igla-race-rtl.json b/proofs/lean4/.trinity/seals/race_igla-race-rtl.json index 589c5a6975..1017e63534 100644 --- a/proofs/lean4/.trinity/seals/race_igla-race-rtl.json +++ b/proofs/lean4/.trinity/seals/race_igla-race-rtl.json @@ -7,5 +7,5 @@ "ring": 12, "sealed_at": "2026-06-23T07:33:23Z", "spec_hash": "sha256:326abce4a3a4ac58ec106f2914aeb7c57fc9b713a1a3ca7fa0e95194cf6cd8bf", - "spec_path": "/Users/playra/t27/specs/igla/race/rtl.t27" -} \ No newline at end of file + "spec_path": "specs/igla/race/rtl.t27" +} diff --git a/proofs/lean4/.trinity/seals/race_igla-race-systolic-array.json b/proofs/lean4/.trinity/seals/race_igla-race-systolic-array.json index 55b6c5a48f..3d250c06dd 100644 --- a/proofs/lean4/.trinity/seals/race_igla-race-systolic-array.json +++ b/proofs/lean4/.trinity/seals/race_igla-race-systolic-array.json @@ -7,5 +7,5 @@ "ring": 12, "sealed_at": "2026-06-23T07:33:23Z", "spec_hash": "sha256:c784bd6931791d71f90cf3e33ffbfe8dfe7ae8aa1063ae41eb2fe5aadda3438a", - "spec_path": "/Users/playra/t27/specs/igla/race/systolic_array.t27" -} \ No newline at end of file + "spec_path": "specs/igla/race/systolic_array.t27" +} diff --git a/proofs/lean4/.trinity/seals/race_igla-race-systolic-ternary.json b/proofs/lean4/.trinity/seals/race_igla-race-systolic-ternary.json index cbe6f6b5e5..207279170c 100644 --- a/proofs/lean4/.trinity/seals/race_igla-race-systolic-ternary.json +++ b/proofs/lean4/.trinity/seals/race_igla-race-systolic-ternary.json @@ -7,5 +7,5 @@ "ring": 12, "sealed_at": "2026-06-23T07:33:23Z", "spec_hash": "sha256:e6a1833428296a3803979e69c0ba3c86414627071a645feb48a9a7b928be6499", - "spec_path": "/Users/playra/t27/specs/igla/race/systolic_ternary.t27" -} \ No newline at end of file + "spec_path": "specs/igla/race/systolic_ternary.t27" +} diff --git a/proofs/lean4/.trinity/seals/race_igla-race-ternary-gemm.json b/proofs/lean4/.trinity/seals/race_igla-race-ternary-gemm.json index 9ee52c4729..d1f70e14d7 100644 --- a/proofs/lean4/.trinity/seals/race_igla-race-ternary-gemm.json +++ b/proofs/lean4/.trinity/seals/race_igla-race-ternary-gemm.json @@ -7,5 +7,5 @@ "ring": 12, "sealed_at": "2026-06-23T07:33:23Z", "spec_hash": "sha256:d950b7e77d15124102b3ba2b99d42324c528db7f76361c04458a2afe3febd2a8", - "spec_path": "/Users/playra/t27/specs/igla/race/ternary_gemm.t27" -} \ No newline at end of file + "spec_path": "specs/igla/race/ternary_gemm.t27" +} diff --git a/proofs/lean4/.trinity/seals/race_igla-race-ternary-inference.json b/proofs/lean4/.trinity/seals/race_igla-race-ternary-inference.json index deb6d23157..701b987e72 100644 --- a/proofs/lean4/.trinity/seals/race_igla-race-ternary-inference.json +++ b/proofs/lean4/.trinity/seals/race_igla-race-ternary-inference.json @@ -7,5 +7,5 @@ "ring": 12, "sealed_at": "2026-06-23T07:33:23Z", "spec_hash": "sha256:588d9d16edb5b9defbf6f3a9aab83b780e380f3ccaf21a5305fb4a44e39db7d5", - "spec_path": "/Users/playra/t27/specs/igla/race/ternary_inference.t27" -} \ No newline at end of file + "spec_path": "specs/igla/race/ternary_inference.t27" +} diff --git a/proofs/lean4/.trinity/seals/race_igla-race-ternary-mac.json b/proofs/lean4/.trinity/seals/race_igla-race-ternary-mac.json index 6cdd89d7b9..088d7a60a9 100644 --- a/proofs/lean4/.trinity/seals/race_igla-race-ternary-mac.json +++ b/proofs/lean4/.trinity/seals/race_igla-race-ternary-mac.json @@ -7,5 +7,5 @@ "ring": 12, "sealed_at": "2026-06-23T07:33:23Z", "spec_hash": "sha256:5b7da1ecbdd319447a4731d0aa400783ee388b9cc0d4cb73865003486d49dd2a", - "spec_path": "/Users/playra/t27/specs/igla/race/ternary_mac.t27" -} \ No newline at end of file + "spec_path": "specs/igla/race/ternary_mac.t27" +} diff --git a/proofs/lean4/.trinity/seals/race_igla-race-yosys.json b/proofs/lean4/.trinity/seals/race_igla-race-yosys.json index 44c1c1c1ef..bdaa18da12 100644 --- a/proofs/lean4/.trinity/seals/race_igla-race-yosys.json +++ b/proofs/lean4/.trinity/seals/race_igla-race-yosys.json @@ -7,5 +7,5 @@ "ring": 12, "sealed_at": "2026-06-23T07:33:23Z", "spec_hash": "sha256:0bc486f8ed0079fbcd856bc41564797e73b614ee9b7e0a5c03a7986a1b5f24a5", - "spec_path": "/Users/playra/t27/specs/igla/race/yosys.t27" -} \ No newline at end of file + "spec_path": "specs/igla/race/yosys.t27" +} diff --git a/scripts/fix_v09_latex.py b/scripts/fix_v09_latex.py index 8d8bd26d8b..e8c3467704 100644 --- a/scripts/fix_v09_latex.py +++ b/scripts/fix_v09_latex.py @@ -59,7 +59,7 @@ def fix_latex(content): return content # Read original file -with open('/Users/playra/t27/research/trinity-pellis-paper/G2_ALPHA_S_PHI_FRAMEWORK_V0.9.tex', 'r') as f: +with open(str(ROOT / "research/trinity-pellis-paper/G2_ALPHA_S_PHI_FRAMEWORK_V0.9.tex"), 'r') as f: original = f.read() # Apply fixes diff --git a/scripts/gen_w367_lean.py b/scripts/gen_w367_lean.py index 1ed28808c2..9c06faf962 100644 --- a/scripts/gen_w367_lean.py +++ b/scripts/gen_w367_lean.py @@ -3,7 +3,13 @@ from pathlib import Path -ROOT = Path("/Users/playra/t27") +# The repository root, derived from where this file sits, not from the +# machine it was written on. This was an absolute path into one +# developer's home directory, so it could run for exactly one person -- +# and the secret-scan gate rejects that path, which is how it was found. +# (The old literal is deliberately not quoted here: a comment naming it +# trips the same gate.) +ROOT = Path(__file__).resolve().parent.parent LEAN_FILE = ROOT / "proofs" / "lean4" / "Trinity" / "TernaryInference.lean" diff --git a/scripts/gen_w368_lean.py b/scripts/gen_w368_lean.py index 88ec619e4b..28baedccf9 100644 --- a/scripts/gen_w368_lean.py +++ b/scripts/gen_w368_lean.py @@ -3,7 +3,13 @@ from pathlib import Path -ROOT = Path("/Users/playra/t27") +# The repository root, derived from where this file sits, not from the +# machine it was written on. This was an absolute path into one +# developer's home directory, so it could run for exactly one person -- +# and the secret-scan gate rejects that path, which is how it was found. +# (The old literal is deliberately not quoted here: a comment naming it +# trips the same gate.) +ROOT = Path(__file__).resolve().parent.parent LEAN_FILE = ROOT / "proofs" / "lean4" / "Trinity" / "TernaryInference.lean" diff --git a/scripts/gen_w369_lean.py b/scripts/gen_w369_lean.py index 1cf853bb34..ce247d6727 100644 --- a/scripts/gen_w369_lean.py +++ b/scripts/gen_w369_lean.py @@ -3,7 +3,13 @@ from pathlib import Path -ROOT = Path("/Users/playra/t27") +# The repository root, derived from where this file sits, not from the +# machine it was written on. This was an absolute path into one +# developer's home directory, so it could run for exactly one person -- +# and the secret-scan gate rejects that path, which is how it was found. +# (The old literal is deliberately not quoted here: a comment naming it +# trips the same gate.) +ROOT = Path(__file__).resolve().parent.parent LEAN_FILE = ROOT / "proofs" / "lean4" / "Trinity" / "TernaryInference.lean" diff --git a/scripts/gen_w370_lean.py b/scripts/gen_w370_lean.py index 88e522a6e6..14ecdd7c04 100644 --- a/scripts/gen_w370_lean.py +++ b/scripts/gen_w370_lean.py @@ -3,7 +3,13 @@ from pathlib import Path -ROOT = Path("/Users/playra/t27") +# The repository root, derived from where this file sits, not from the +# machine it was written on. This was an absolute path into one +# developer's home directory, so it could run for exactly one person -- +# and the secret-scan gate rejects that path, which is how it was found. +# (The old literal is deliberately not quoted here: a comment naming it +# trips the same gate.) +ROOT = Path(__file__).resolve().parent.parent LEAN_FILE = ROOT / "proofs" / "lean4" / "Trinity" / "TernaryInference.lean" diff --git a/scripts/gen_w371_lean.py b/scripts/gen_w371_lean.py index 976ea57b3d..b577194a1b 100644 --- a/scripts/gen_w371_lean.py +++ b/scripts/gen_w371_lean.py @@ -3,7 +3,13 @@ from pathlib import Path -ROOT = Path("/Users/playra/t27") +# The repository root, derived from where this file sits, not from the +# machine it was written on. This was an absolute path into one +# developer's home directory, so it could run for exactly one person -- +# and the secret-scan gate rejects that path, which is how it was found. +# (The old literal is deliberately not quoted here: a comment naming it +# trips the same gate.) +ROOT = Path(__file__).resolve().parent.parent LEAN_FILE = ROOT / "proofs" / "lean4" / "Trinity" / "TernaryInference.lean" diff --git a/scripts/gen_w372_lean.py b/scripts/gen_w372_lean.py index 0e6a638151..e956f479ab 100644 --- a/scripts/gen_w372_lean.py +++ b/scripts/gen_w372_lean.py @@ -3,7 +3,13 @@ from pathlib import Path -ROOT = Path("/Users/playra/t27") +# The repository root, derived from where this file sits, not from the +# machine it was written on. This was an absolute path into one +# developer's home directory, so it could run for exactly one person -- +# and the secret-scan gate rejects that path, which is how it was found. +# (The old literal is deliberately not quoted here: a comment naming it +# trips the same gate.) +ROOT = Path(__file__).resolve().parent.parent LEAN_FILE = ROOT / "proofs" / "lean4" / "Trinity" / "TernaryInference.lean" diff --git a/scripts/gen_w373_lean.py b/scripts/gen_w373_lean.py index 35f7043db5..8a7d3f22f4 100644 --- a/scripts/gen_w373_lean.py +++ b/scripts/gen_w373_lean.py @@ -3,7 +3,13 @@ from pathlib import Path -ROOT = Path("/Users/playra/t27") +# The repository root, derived from where this file sits, not from the +# machine it was written on. This was an absolute path into one +# developer's home directory, so it could run for exactly one person -- +# and the secret-scan gate rejects that path, which is how it was found. +# (The old literal is deliberately not quoted here: a comment naming it +# trips the same gate.) +ROOT = Path(__file__).resolve().parent.parent LEAN_FILE = ROOT / "proofs" / "lean4" / "Trinity" / "TernaryInference.lean" diff --git a/scripts/gen_w374_lean.py b/scripts/gen_w374_lean.py index f0aa49fc30..52b175d56d 100644 --- a/scripts/gen_w374_lean.py +++ b/scripts/gen_w374_lean.py @@ -3,7 +3,13 @@ from pathlib import Path -ROOT = Path("/Users/playra/t27") +# The repository root, derived from where this file sits, not from the +# machine it was written on. This was an absolute path into one +# developer's home directory, so it could run for exactly one person -- +# and the secret-scan gate rejects that path, which is how it was found. +# (The old literal is deliberately not quoted here: a comment naming it +# trips the same gate.) +ROOT = Path(__file__).resolve().parent.parent LEAN_FILE = ROOT / "proofs" / "lean4" / "Trinity" / "TernaryInference.lean" diff --git a/scripts/gen_w375_lean.py b/scripts/gen_w375_lean.py index 774ba315ef..7a048329de 100644 --- a/scripts/gen_w375_lean.py +++ b/scripts/gen_w375_lean.py @@ -3,7 +3,13 @@ from pathlib import Path -ROOT = Path("/Users/playra/t27") +# The repository root, derived from where this file sits, not from the +# machine it was written on. This was an absolute path into one +# developer's home directory, so it could run for exactly one person -- +# and the secret-scan gate rejects that path, which is how it was found. +# (The old literal is deliberately not quoted here: a comment naming it +# trips the same gate.) +ROOT = Path(__file__).resolve().parent.parent LEAN_FILE = ROOT / "proofs" / "lean4" / "Trinity" / "TernaryInference.lean" diff --git a/scripts/gen_w376_lean.py b/scripts/gen_w376_lean.py index 01a6e04e1c..855145f84d 100644 --- a/scripts/gen_w376_lean.py +++ b/scripts/gen_w376_lean.py @@ -3,7 +3,13 @@ from pathlib import Path -ROOT = Path("/Users/playra/t27") +# The repository root, derived from where this file sits, not from the +# machine it was written on. This was an absolute path into one +# developer's home directory, so it could run for exactly one person -- +# and the secret-scan gate rejects that path, which is how it was found. +# (The old literal is deliberately not quoted here: a comment naming it +# trips the same gate.) +ROOT = Path(__file__).resolve().parent.parent LEAN_FILE = ROOT / "proofs" / "lean4" / "Trinity" / "TernaryInference.lean" diff --git a/scripts/gen_w377_lean.py b/scripts/gen_w377_lean.py index f96d909dab..06516ea34a 100644 --- a/scripts/gen_w377_lean.py +++ b/scripts/gen_w377_lean.py @@ -3,7 +3,13 @@ from pathlib import Path -ROOT = Path("/Users/playra/t27") +# The repository root, derived from where this file sits, not from the +# machine it was written on. This was an absolute path into one +# developer's home directory, so it could run for exactly one person -- +# and the secret-scan gate rejects that path, which is how it was found. +# (The old literal is deliberately not quoted here: a comment naming it +# trips the same gate.) +ROOT = Path(__file__).resolve().parent.parent LEAN_FILE = ROOT / "proofs" / "lean4" / "Trinity" / "TernaryInference.lean" diff --git a/scripts/gen_w378_lean.py b/scripts/gen_w378_lean.py index 7f2fe7719b..2f14eee236 100644 --- a/scripts/gen_w378_lean.py +++ b/scripts/gen_w378_lean.py @@ -3,7 +3,13 @@ from pathlib import Path -ROOT = Path("/Users/playra/t27") +# The repository root, derived from where this file sits, not from the +# machine it was written on. This was an absolute path into one +# developer's home directory, so it could run for exactly one person -- +# and the secret-scan gate rejects that path, which is how it was found. +# (The old literal is deliberately not quoted here: a comment naming it +# trips the same gate.) +ROOT = Path(__file__).resolve().parent.parent LEAN_FILE = ROOT / "proofs" / "lean4" / "Trinity" / "TernaryInference.lean" diff --git a/scripts/gen_w379_lean.py b/scripts/gen_w379_lean.py index d55fdf05a0..4d58bfc54c 100644 --- a/scripts/gen_w379_lean.py +++ b/scripts/gen_w379_lean.py @@ -3,7 +3,13 @@ from pathlib import Path -ROOT = Path("/Users/playra/t27") +# The repository root, derived from where this file sits, not from the +# machine it was written on. This was an absolute path into one +# developer's home directory, so it could run for exactly one person -- +# and the secret-scan gate rejects that path, which is how it was found. +# (The old literal is deliberately not quoted here: a comment naming it +# trips the same gate.) +ROOT = Path(__file__).resolve().parent.parent LEAN_FILE = ROOT / "proofs" / "lean4" / "Trinity" / "TernaryInference.lean" diff --git a/scripts/gen_w380_lean.py b/scripts/gen_w380_lean.py index c3b4b5e106..dbde5870d4 100644 --- a/scripts/gen_w380_lean.py +++ b/scripts/gen_w380_lean.py @@ -3,7 +3,13 @@ from pathlib import Path -ROOT = Path("/Users/playra/t27") +# The repository root, derived from where this file sits, not from the +# machine it was written on. This was an absolute path into one +# developer's home directory, so it could run for exactly one person -- +# and the secret-scan gate rejects that path, which is how it was found. +# (The old literal is deliberately not quoted here: a comment naming it +# trips the same gate.) +ROOT = Path(__file__).resolve().parent.parent LEAN_FILE = ROOT / "proofs" / "lean4" / "Trinity" / "TernaryInference.lean" diff --git a/scripts/gen_w380_lean_extra.py b/scripts/gen_w380_lean_extra.py index 000c88d627..2f5a3f7e50 100644 --- a/scripts/gen_w380_lean_extra.py +++ b/scripts/gen_w380_lean_extra.py @@ -3,7 +3,13 @@ from pathlib import Path -ROOT = Path("/Users/playra/t27") +# The repository root, derived from where this file sits, not from the +# machine it was written on. This was an absolute path into one +# developer's home directory, so it could run for exactly one person -- +# and the secret-scan gate rejects that path, which is how it was found. +# (The old literal is deliberately not quoted here: a comment naming it +# trips the same gate.) +ROOT = Path(__file__).resolve().parent.parent LEAN_FILE = ROOT / "proofs" / "lean4" / "Trinity" / "TernaryInference.lean" diff --git a/scripts/gen_w381_lean.py b/scripts/gen_w381_lean.py index c81a862996..38bc355235 100644 --- a/scripts/gen_w381_lean.py +++ b/scripts/gen_w381_lean.py @@ -3,7 +3,13 @@ from pathlib import Path -ROOT = Path("/Users/playra/t27") +# The repository root, derived from where this file sits, not from the +# machine it was written on. This was an absolute path into one +# developer's home directory, so it could run for exactly one person -- +# and the secret-scan gate rejects that path, which is how it was found. +# (The old literal is deliberately not quoted here: a comment naming it +# trips the same gate.) +ROOT = Path(__file__).resolve().parent.parent LEAN_FILE = ROOT / "proofs" / "lean4" / "Trinity" / "TernaryInference.lean" diff --git a/scripts/gen_w382_lean.py b/scripts/gen_w382_lean.py index 6f60612aa9..a9a0382646 100644 --- a/scripts/gen_w382_lean.py +++ b/scripts/gen_w382_lean.py @@ -3,7 +3,13 @@ from pathlib import Path -ROOT = Path("/Users/playra/t27") +# The repository root, derived from where this file sits, not from the +# machine it was written on. This was an absolute path into one +# developer's home directory, so it could run for exactly one person -- +# and the secret-scan gate rejects that path, which is how it was found. +# (The old literal is deliberately not quoted here: a comment naming it +# trips the same gate.) +ROOT = Path(__file__).resolve().parent.parent LEAN_FILE = ROOT / "proofs" / "lean4" / "Trinity" / "TernaryInference.lean" diff --git a/scripts/gen_w384_lean.py b/scripts/gen_w384_lean.py index e7eac57ba3..b107ccda30 100644 --- a/scripts/gen_w384_lean.py +++ b/scripts/gen_w384_lean.py @@ -3,7 +3,13 @@ from pathlib import Path -ROOT = Path("/Users/playra/t27") +# The repository root, derived from where this file sits, not from the +# machine it was written on. This was an absolute path into one +# developer's home directory, so it could run for exactly one person -- +# and the secret-scan gate rejects that path, which is how it was found. +# (The old literal is deliberately not quoted here: a comment naming it +# trips the same gate.) +ROOT = Path(__file__).resolve().parent.parent LEAN_FILE = ROOT / "proofs" / "lean4" / "Trinity" / "TernaryInference.lean" diff --git a/scripts/gen_w385_lean.py b/scripts/gen_w385_lean.py index c340de4cfd..b2b5988694 100644 --- a/scripts/gen_w385_lean.py +++ b/scripts/gen_w385_lean.py @@ -3,7 +3,13 @@ from pathlib import Path -ROOT = Path("/Users/playra/t27") +# The repository root, derived from where this file sits, not from the +# machine it was written on. This was an absolute path into one +# developer's home directory, so it could run for exactly one person -- +# and the secret-scan gate rejects that path, which is how it was found. +# (The old literal is deliberately not quoted here: a comment naming it +# trips the same gate.) +ROOT = Path(__file__).resolve().parent.parent LEAN_FILE = ROOT / "proofs" / "lean4" / "Trinity" / "TernaryInference.lean" diff --git a/scripts/gen_w386_lean.py b/scripts/gen_w386_lean.py index a72e3b45ec..de6a1a46ae 100644 --- a/scripts/gen_w386_lean.py +++ b/scripts/gen_w386_lean.py @@ -3,7 +3,13 @@ from pathlib import Path -ROOT = Path("/Users/playra/t27") +# The repository root, derived from where this file sits, not from the +# machine it was written on. This was an absolute path into one +# developer's home directory, so it could run for exactly one person -- +# and the secret-scan gate rejects that path, which is how it was found. +# (The old literal is deliberately not quoted here: a comment naming it +# trips the same gate.) +ROOT = Path(__file__).resolve().parent.parent LEAN_FILE = ROOT / "proofs" / "lean4" / "Trinity" / "TernaryInference.lean" diff --git a/scripts/gen_w387_lean.py b/scripts/gen_w387_lean.py index c8fcb29850..8da2a68350 100644 --- a/scripts/gen_w387_lean.py +++ b/scripts/gen_w387_lean.py @@ -3,7 +3,13 @@ from pathlib import Path -ROOT = Path("/Users/playra/t27") +# The repository root, derived from where this file sits, not from the +# machine it was written on. This was an absolute path into one +# developer's home directory, so it could run for exactly one person -- +# and the secret-scan gate rejects that path, which is how it was found. +# (The old literal is deliberately not quoted here: a comment naming it +# trips the same gate.) +ROOT = Path(__file__).resolve().parent.parent LEAN_FILE = ROOT / "proofs" / "lean4" / "Trinity" / "TernaryInference.lean" diff --git a/scripts/gen_w388_lean.py b/scripts/gen_w388_lean.py index acdaafec32..8d191b05f9 100644 --- a/scripts/gen_w388_lean.py +++ b/scripts/gen_w388_lean.py @@ -3,7 +3,13 @@ from pathlib import Path -ROOT = Path("/Users/playra/t27") +# The repository root, derived from where this file sits, not from the +# machine it was written on. This was an absolute path into one +# developer's home directory, so it could run for exactly one person -- +# and the secret-scan gate rejects that path, which is how it was found. +# (The old literal is deliberately not quoted here: a comment naming it +# trips the same gate.) +ROOT = Path(__file__).resolve().parent.parent LEAN_FILE = ROOT / "proofs" / "lean4" / "Trinity" / "TernaryInference.lean" diff --git a/scripts/gen_w389_lean.py b/scripts/gen_w389_lean.py index 2f6119fcb1..cac9e8dd11 100644 --- a/scripts/gen_w389_lean.py +++ b/scripts/gen_w389_lean.py @@ -3,7 +3,13 @@ from pathlib import Path -ROOT = Path("/Users/playra/t27") +# The repository root, derived from where this file sits, not from the +# machine it was written on. This was an absolute path into one +# developer's home directory, so it could run for exactly one person -- +# and the secret-scan gate rejects that path, which is how it was found. +# (The old literal is deliberately not quoted here: a comment naming it +# trips the same gate.) +ROOT = Path(__file__).resolve().parent.parent LEAN_FILE = ROOT / "proofs" / "lean4" / "Trinity" / "TernaryInference.lean" diff --git a/scripts/gen_w390_lean.py b/scripts/gen_w390_lean.py index 617e5e2f25..3d46cee776 100644 --- a/scripts/gen_w390_lean.py +++ b/scripts/gen_w390_lean.py @@ -3,7 +3,13 @@ from pathlib import Path -ROOT = Path("/Users/playra/t27") +# The repository root, derived from where this file sits, not from the +# machine it was written on. This was an absolute path into one +# developer's home directory, so it could run for exactly one person -- +# and the secret-scan gate rejects that path, which is how it was found. +# (The old literal is deliberately not quoted here: a comment naming it +# trips the same gate.) +ROOT = Path(__file__).resolve().parent.parent LEAN_FILE = ROOT / "proofs" / "lean4" / "Trinity" / "TernaryInference.lean" diff --git a/scripts/gen_w391_lean.py b/scripts/gen_w391_lean.py index 7988899605..ee6806dd88 100755 --- a/scripts/gen_w391_lean.py +++ b/scripts/gen_w391_lean.py @@ -3,7 +3,13 @@ from pathlib import Path -ROOT = Path("/Users/playra/t27") +# The repository root, derived from where this file sits, not from the +# machine it was written on. This was an absolute path into one +# developer's home directory, so it could run for exactly one person -- +# and the secret-scan gate rejects that path, which is how it was found. +# (The old literal is deliberately not quoted here: a comment naming it +# trips the same gate.) +ROOT = Path(__file__).resolve().parent.parent LEAN_FILE = ROOT / "proofs" / "lean4" / "Trinity" / "TernaryInference.lean" diff --git a/scripts/gen_w392_lean.py b/scripts/gen_w392_lean.py index bc8cda1572..2aabf3132f 100644 --- a/scripts/gen_w392_lean.py +++ b/scripts/gen_w392_lean.py @@ -3,7 +3,13 @@ from pathlib import Path -ROOT = Path("/Users/playra/t27") +# The repository root, derived from where this file sits, not from the +# machine it was written on. This was an absolute path into one +# developer's home directory, so it could run for exactly one person -- +# and the secret-scan gate rejects that path, which is how it was found. +# (The old literal is deliberately not quoted here: a comment naming it +# trips the same gate.) +ROOT = Path(__file__).resolve().parent.parent LEAN_FILE = ROOT / "proofs" / "lean4" / "Trinity" / "TernaryInference.lean" diff --git a/scripts/overnight_research_agent.py b/scripts/overnight_research_agent.py index 2ee3cbfccd..3b346961fa 100755 --- a/scripts/overnight_research_agent.py +++ b/scripts/overnight_research_agent.py @@ -19,7 +19,10 @@ E = math.e # ============ PATHS ============ -REPO_ROOT = "/Users/playra/t27" +# From this file's location, not from the machine it was written on: this +# was an absolute path into one developer's home directory and could +# therefore run for exactly one person. +REPO_ROOT = os.path.dirname(os.path.dirname(os.path.abspath(__file__))) LOG_FILE = os.path.join(REPO_ROOT, "overnight_errors.log") PROGRESS_FILE = os.path.join(REPO_ROOT, "OVERNIGHT_PROGRESS.md") diff --git a/scripts/pslq_bff.py b/scripts/pslq_bff.py index e27e537bf4..99e4e66d86 100755 --- a/scripts/pslq_bff.py +++ b/scripts/pslq_bff.py @@ -10,6 +10,9 @@ import math from pathlib import Path +# Repository root from this file's location, not from one machine. +ROOT = Path(__file__).resolve().parent.parent + # Trinity constants for PSLQ PHI = (1 + math.sqrt(5)) / 2 # Golden ratio PI = math.pi @@ -146,7 +149,7 @@ def main(): results.append(result6) # Save all results - output_dir = Path("/Users/playra/t27/scripts/output") + output_dir = Path(str(ROOT / "scripts/output")) output_dir.mkdir(parents=True, exist_ok=True) output_file = output_dir / "pslq_bff_results.json" diff --git a/scripts/pslq_ramanujan_api.py b/scripts/pslq_ramanujan_api.py index b56c3098af..bd7fc3bc6e 100644 --- a/scripts/pslq_ramanujan_api.py +++ b/scripts/pslq_ramanujan_api.py @@ -12,6 +12,9 @@ import math from pathlib import Path +# Repository root from this file's location, not from one machine. +ROOT = Path(__file__).resolve().parent.parent + # Trinity constants for PSLQ PHI = (1 + math.sqrt(5)) / 2 # Golden ratio PI = math.pi @@ -161,7 +164,7 @@ def test_pslq(vector, description): def save_results(results): """Save PSLQ results to JSON file for analysis.""" - output_dir = Path("/Users/playra/t27/scripts/output") + output_dir = Path(str(ROOT / "scripts/output")) output_dir.mkdir(parents=True, exist_ok=True) output_file = output_dir / "pslq_ramanujan_results.json" diff --git a/scripts/run_v51_multiple.sh b/scripts/run_v51_multiple.sh index 2e3f31cb83..3252e30c4e 100755 --- a/scripts/run_v51_multiple.sh +++ b/scripts/run_v51_multiple.sh @@ -1,10 +1,12 @@ #!/bin/bash +# Repository root from this script's location, not from one machine. +ROOT="$(cd "$(dirname "${BASH_SOURCE[0]}")/.." && pwd)" # Запустить v51 N=10 раз для получения >1000 формул echo "Running v51 multiple times..." for i in {1..10}; do echo "Run $i/10" - python3 /Users/playra/t27/scripts/ultra_engine_v51.py --all --threshold 0.05 --quiet + python3 "$ROOT"/scripts/ultra_engine_v51.py --all --threshold 0.05 --quiet echo "" done echo "All runs completed!" -chmod +x /Users/playra/t27/scripts/run_v51_multiple.sh +chmod +x "$ROOT"/scripts/run_v51_multiple.sh diff --git a/scripts/unified_search_all.py b/scripts/unified_search_all.py index b49e24b410..f22ca8df26 100644 --- a/scripts/unified_search_all.py +++ b/scripts/unified_search_all.py @@ -10,6 +10,9 @@ from datetime import datetime from pathlib import Path +# Repository root from this file's location, not from one machine. +ROOT = Path(__file__).resolve().parent.parent + def run_method(name, script, args): """Run a search method""" print(f"\n{'='*70}") @@ -43,21 +46,21 @@ def main(): # Method 1: v6.5 ABSOLUTE (CPU) results.append(run_method( "v6.5 ABSOLUTE (NumPy + 8-core)", - "/Users/playra/t27/scripts/ultra_engine_v65_absolute.py", + str(ROOT / "scripts/ultra_engine_v65_absolute.py"), [] )) # Method 2: Chimera Search (max_pow=7, threshold=0.01) results.append(run_method( "Chimera Search (Rust, 3375 basis)", - "/Users/playra/t27/target/release/t27c", + str(ROOT / "target/release/t27c"), ["formula", "chimera-search", "--max-pow", "7", "--threshold", "0.01"] )) # Method 3: Chimera Search (max_pow=7, threshold=0.03) results.append(run_method( "Chimera Search (Rust, 3375 basis, wider)", - "/Users/playra/t27/target/release/t27c", + str(ROOT / "target/release/t27c"), ["formula", "chimera-search", "--max-pow", "7", "--threshold", "0.03"] )) diff --git a/scripts/verify_all_152.py b/scripts/verify_all_152.py index 4c693e2a14..da38e2d871 100755 --- a/scripts/verify_all_152.py +++ b/scripts/verify_all_152.py @@ -101,7 +101,7 @@ print(f"SHA256 seal: {sha256_seal}") import os -seal_dir = "/Users/playra/t27/research/seals" +seal_dir = str(ROOT / "research/seals") os.makedirs(seal_dir, exist_ok=True) seal_file = os.path.join(seal_dir, "all_152_v0.2.sha") with open(seal_file, "w") as f: diff --git a/tools/check_now_entry_shape.py b/tools/check_now_entry_shape.py new file mode 100644 index 0000000000..c00b646be7 --- /dev/null +++ b/tools/check_now_entry_shape.py @@ -0,0 +1,213 @@ +#!/usr/bin/env python3 +"""The docs/now/ entry a PR adds must SAY something. + +WHY THIS EXISTS +--------------- +`t27-master-protection` requires four status checks, and one of them, `check`, +was this: + + - name: Check freshness + run: | + # Add freshness check logic here in future + echo "Checking repository freshness..." + +A required gate that echoes a string. It passed every pull request it ever ran +on, and its green meant nothing. The ruleset is not this file's to edit -- so +the job keeps its required name and is given something real to do instead. + +WHAT IT CHECKS, AND WHAT IT DELIBERATELY DOES NOT +------------------------------------------------- +NOW Sync Gate already requires that an entry was ADDED. It does not read it. +So the two are complementary and neither is redundant: + + NOW Sync Gate -> "you wrote one" + this -> "what you wrote says something" + +Checked, per entry added by the pull request: + + * the filename is `YYYY-MM-DD-.md` + * the first line is `# NOW -- (YYYY-MM-DD)` + * the date in that heading matches the date in the filename -- an entry + dated one day and filed under another sorts wrong in a log whose whole + job is chronology + * there is a `## ` section heading + * there is at least one `- ` bullet, and the bullets are not placeholders + +NOT checked: whether the content is TRUE. No gate can do that, and pretending +otherwise would be the same defect one level up. + +ZERO ENTRIES IS A FAILURE, NOT A PASS +------------------------------------- +If the pull request adds no entry, this exits 1 rather than passing quietly. +NOW Sync Gate should have caught that first; if it did not, two gates are +wrong at once and that is worth hearing about. A check that reports success +over an empty input set is the shape this file was written to replace. +""" + +import os +import pathlib +import re +import subprocess +import sys +import tempfile + +ROOT = pathlib.Path(__file__).resolve().parent.parent + +FILENAME = re.compile(r"^(\d{4}-\d{2}-\d{2})-[a-z0-9][a-z0-9-]*\.md$") +HEADING = re.compile(r"^# NOW -- (.+) \((\d{4}-\d{2}-\d{2})\)\s*$") +PLACEHOLDER = re.compile(r"^(tbd|todo|wip|n/?a|\.\.\.|-+)$", re.I) + + +def added_now_entries(base, head): + """Files under docs/now/ that this PR adds. README.md is not an entry.""" + r = subprocess.run( + ["git", "diff", "--name-only", "--diff-filter=A", f"{base}...{head}", "--", "docs/now/"], + capture_output=True, + text=True, + cwd=ROOT, + ) + if r.returncode != 0: + return None + return [ + p for p in r.stdout.split("\n") if p.endswith(".md") and not p.endswith("README.md") + ] + + +def check_entry(path, text): + """Every complaint about one entry. Empty list means it is well formed.""" + bad = [] + name = pathlib.PurePosixPath(path).name + + m_name = FILENAME.match(name) + if not m_name: + bad.append(f"filename is not YYYY-MM-DD-<slug>.md: {name}") + + lines = text.splitlines() + if not lines: + bad.append("the file is empty") + return bad + + m_head = HEADING.match(lines[0]) + if not m_head: + bad.append(f"first line is not `# NOW -- <title> (YYYY-MM-DD)`: {lines[0][:70]!r}") + elif m_name and m_head.group(2) != m_name.group(1): + bad.append( + f"heading is dated {m_head.group(2)} but the filename says {m_name.group(1)} " + "-- a log whose job is chronology cannot have the two disagree" + ) + + if not any(l.startswith("## ") for l in lines): + bad.append("no `## ` section heading") + + bullets = [l[2:].strip() for l in lines if l.startswith("- ")] + if not bullets: + bad.append("no `- ` bullets: the entry states nothing") + else: + empty = [b for b in bullets if len(b) < 12 or PLACEHOLDER.match(b)] + if len(empty) == len(bullets): + bad.append(f"every bullet is a placeholder or too short to say anything: {bullets}") + + return bad + + +def self_check(): + """Break it on purpose. A gate nobody has seen fail is not a gate.""" + good = ( + "# NOW -- A real entry about a real thing (2026-08-28)\n\n" + "## A real entry about a real thing (Refs #1)\n\n" + "- something specific happened and here is what it was\n" + ) + cases = [ + ("well formed", "2026-08-28-a-real-entry.md", good, 0), + ( + "heading date disagrees with filename", + "2026-08-27-a-real-entry.md", + good, + 1, + ), + ( + "no bullets", + "2026-08-28-a-real-entry.md", + "# NOW -- Title (2026-08-28)\n\n## Title\n", + 1, + ), + ( + "placeholder bullets", + "2026-08-28-a-real-entry.md", + "# NOW -- Title (2026-08-28)\n\n## Title\n\n- TBD\n- ...\n", + 1, + ), + ( + "wrong first line", + "2026-08-28-a-real-entry.md", + "# Some other heading\n\n## Title\n\n- a bullet that is long enough\n", + 1, + ), + ("empty file", "2026-08-28-a-real-entry.md", "", 1), + ] + failures = 0 + for label, name, text, want in cases: + got = 1 if check_entry(f"docs/now/{name}", text) else 0 + ok = got == want + print(f" {label:<38} {'ok' if ok else 'CONTROL FAILED'}" + f"{'' if ok else f' (wanted {want}, got {got})'}") + if not ok: + failures += 1 + if failures: + print(f"\nFAIL: {failures} control(s) did not behave as stated.") + return 1 + print("\nOK: every control behaves as stated.") + return 0 + + +def main(): + if "--self-check" in sys.argv: + return self_check() + + base = os.environ.get("PR_BASE_SHA", "") + head = os.environ.get("PR_HEAD_SHA", "HEAD") + if not base: + print("check_now_entry_shape: PR_BASE_SHA is unset, so the set of entries this") + print(" change adds cannot be computed. Reporting nothing rather than a pass") + print(" this run did not earn -- set PR_BASE_SHA and PR_HEAD_SHA.") + return 2 + + entries = added_now_entries(base, head) + if entries is None: + print(f"FAIL: `git diff {base}...{head}` failed -- the range is wrong, not the tree") + return 1 + + if not entries: + print("FAIL: this change adds no docs/now/ entry.") + print(" NOW Sync Gate should have caught that first. Two gates disagreeing") + print(" about the same requirement is worth hearing about, so this one") + print(" refuses rather than passing over an empty set.") + return 1 + + bad = 0 + for path in entries: + full = ROOT / path + try: + text = full.read_text() + except OSError as e: + print(f"FAIL {path}: cannot read it ({e})") + bad += 1 + continue + problems = check_entry(path, text) + if problems: + bad += 1 + print(f"FAIL {path}") + for p in problems: + print(f" {p}") + else: + print(f"ok {path}") + + if bad: + print(f"\nFAIL: {bad} of {len(entries)} entr(y/ies) do not say anything checkable.") + return 1 + print(f"\nOK: {len(entries)} entr(y/ies) added, each well formed.") + return 0 + + +if __name__ == "__main__": + sys.exit(main())