ci: repair the two workflows whose failure was in the workflow

.github/workflows/brain-seal-refresh.yml

@@ -8,8 +8,10 @@ on:
       - 'scripts/aggregate-experience.sh'
   workflow_dispatch:
 
+# `contents: read` since the step that needed write was removed below. The
+# artifact upload does not need it, and checkout needs only read.
 permissions:
-  contents: write
+  contents: read
 
 jobs:
   refresh-brain-seals:
@@ -45,16 +47,18 @@ jobs:
           name: brain-seals
           path: .trinity/seals/brain_*.json
 
-      - name: Commit brain seals
-        env:
-          GH_TOKEN: ${{ github.token }}
-        run: |
-          git config --local user.email "t27-bot@trinity.ai"
-          git config --local user.name "T27 Autonomous Agent"
-          git add .trinity/seals/brain_*.json
-          if git diff --staged --quiet; then
-            echo "No brain seal changes to commit"
-            exit 0
-          fi
-          git commit -m "chore: refresh brain seals from experience aggregation (Refs #1440)"
-          git push
+# The `Commit brain seals` step was removed here. It ran `git push` to master,
+# and the branch ruleset refuses that: every run since this workflow was added
+# ends `remote: error: GH013: Repository rule violations found` and
+# `! [remote rejected] master -> master`. Three runs, 2026-04-07, 2026-06-01 and
+# 2026-08-28, all red at that step and only that step -- the aggregation, the
+# schema validation and the artifact upload all passed every time.
+#
+# So the job never told anyone anything except that it could not push, and the
+# one signal it does carry -- do the seals still validate against
+# BRAIN_SEAL_SCHEMA -- was buried under a permanent red. The seals are kept as
+# an artifact, which is what the upload step above is for.
+#
+# Refreshing them ON master is a separate question with a separate answer: it
+# needs a PR, because pushing to master is exactly what the ruleset exists to
+# prevent. Not done here, and not worked around.

.github/workflows/coq-proofs.yml

@@ -8,6 +8,10 @@ on:
   pull_request:
     paths:
       - 'proofs/trinity/**.v'
+      # This file. Without it a PR that repairs this workflow cannot run it, so
+      # the repair ships unverified -- which is how it stayed broken. The `push:`
+      # block above already lists it; the two triggers disagreed.
+      - '.github/workflows/coq-proofs.yml'
   workflow_dispatch:
 
 jobs:
@@ -16,6 +20,19 @@ jobs:
     container:
       image: coqorg/coq:8.19-ocaml-4.14-flambda
       options: --user root
+    # `--user root` is why every run of this job has failed. The image
+    # initialises opam for the `coq` user under /home/coq/.opam; as root, OPAMROOT
+    # defaults to /root/.opam, which does not exist. The log says so exactly:
+    #
+    #     [WARNING] Running as root is not recommended
+    #     [ERROR] Opam has not been initialised, please run `opam init'
+    #     ##[error]Process completed with exit code 50.
+    #
+    # Pointing OPAMROOT at the root the image actually built is the whole fix.
+    # `--user root` stays: checkout writes into a workspace root owns.
+    env:
+      OPAMROOT: /home/coq/.opam
+      OPAMYES: "1"
     steps:
       - name: Checkout repository
         uses: actions/checkout@v6
@@ -24,9 +41,15 @@ jobs:
         run: |
           opam update
           opam install -y coq-interval.4.9.0
+          # Prove the switch is really there before anything depends on it.
+          eval $(opam env)
+          coqc --version
 
       - name: Compile Proofs
         run: |
+          # A new step is a new shell, so the switch has to be re-entered; without
+          # this, coqc is either absent or the wrong one.
+          eval $(opam env)
           cd proofs/trinity
           echo "Compiling Coq proof files..."
           # Compile in dependency order

docs/now/2026-09-06-two-workflows-that-could-not-have-passed-and-one-that-is-rig.md

@@ -0,0 +1,8 @@
+# NOW -- two workflows that could not have passed, and one that is right to be red (2026-09-06)
+
+## two workflows that could not have passed, and one that is right to be red (Refs #3316)
+
+- coq-proofs has never passed: options --user root makes OPAMROOT default to /root/.opam while the image initialises opam under /home/coq/.opam. The log says it exactly -- Opam has not been initialised, exit code 50. Setting OPAMROOT and re-entering the switch in each step is the whole fix.
+- coq-proofs also could not verify its own repair: push: lists the workflow file, pull_request: did not, so a PR that fixes it would not run it. Added, which is what lets this PR check itself.
+- brain-seal-refresh fails at Commit brain seals, which runs git push to master and is refused by the ruleset -- GH013, remote rejected, on all three runs since 2026-04-07. The step is removed rather than worked around; the seals were already kept as an artifact, and the schema validation it was burying is the signal worth having.
+- lean-proofs is NOT a workflow defect and my earlier diagnosis of it was wrong. 8571 of 8574 targets build; the two failures are marked LEFT FAILING, DELIBERATELY in H4Lagrangian.lean at 73 and 108, because norm_num does not evaluate Real.pi, Real.exp or Real.sqrt. The job is reporting the truth.