ci: repair the two workflows whose failure was in the workflow - #3324
Merged
Conversation
Refs #3316 Two of the four remaining FIXes from the never-green triage. The third is withdrawn: see below. coq-proofs.yml -- never passed. `options: --user root` runs the container as root, but the coqorg image initialises opam for the `coq` user under /home/coq/.opam, so OPAMROOT defaults to /root/.opam and opam reports itself uninitialised: [WARNING] Running as root is not recommended [ERROR] Opam has not been initialised, please run `opam init' ##[error]Process completed with exit code 50. OPAMROOT now points at the root the image actually built, and each step re-enters the switch, because a new step is a new shell. `--user root` stays: checkout writes into a workspace root owns. Its `pull_request:` paths did not list this file although `push:` did, so a PR repairing this workflow could not run it and any repair shipped unverified. That is presumably how it stayed broken. Added, and it is what lets this PR check its own fix. brain-seal-refresh.yml -- the `Commit brain seals` step runs `git push` to master. The branch ruleset refuses that, so all three runs of this workflow (2026-04-07, 2026-06-01, 2026-08-28) end: remote: error: GH013: Repository rule violations found ! [remote rejected] master -> master and only that step ever failed; aggregation, schema validation and artifact upload passed every time. Removed rather than worked around -- pushing to master is what the ruleset exists to prevent, and refreshing the seals on master needs a PR, which is a different change. `permissions` drops from `contents: write` to `contents: read`, since nothing left needs write. What the job now reports is whether the seals still validate against BRAIN_SEAL_SCHEMA, which is the signal the permanent red was burying. lean-proofs.yml -- WITHDRAWN from the FIX list; my earlier diagnosis of it was wrong. 8571 of 8574 targets build. The two that fail are marked in the source: -- LEFT FAILING, DELIBERATELY. H4Lagrangian.lean:73 -- LEFT FAILING, DELIBERATELY, AND THIS IS THE ONLY ONE. H4Lagrangian.lean:108 `norm_num` does not evaluate `Real.pi`, `Real.exp` or `Real.sqrt`. The job is red because it is telling the truth, and the workflow's own header says that outcome is the finding. Nothing to fix here.
Contributor
Contributor
|
📓 NotebookLM Notebook linked to this PR
This notebook contains session context, decisions, and artifacts for this work. |
This was referenced Sep 5, 2026
gHashTag
added a commit
that referenced
this pull request
Sep 5, 2026
…have (#3326) Refs #3316 #3324 fixed OPAMROOT and the job got further: opam now updates both repositories and reaches the solver. It then fails on a second, independent defect that was invisible until the first was repaired: [ERROR] Package conflict! * Missing dependency: - coq-interval = 4.9.0 -> coq < 8.19~ No solution found, exiting The image is coqorg/coq:8.19-ocaml-4.14-flambda. The pin asks for a package that requires a Coq older than the one it runs on, so it could never have installed. The dependency is real and is not droppable: 7 of the 13 compiled files `Require Import Interval.Tactic` (Bounds_Masses, Bounds_Mixing, Bounds_Gauge, Bounds_LeptonMasses, Bounds_QuarkMasses, Unitarity, ConsistencyChecks). Only the version can move. Left unpinned on purpose rather than pinned to a guess. No version of coq-interval has been observed resolving against Coq 8.19 in this job, because the job has never run far enough to try. `opam list --installed coq-interval` now prints what the solver chose; that reading is what a pin should be restored from, in a commit that can cite it. This PR runs the workflow on itself -- #3324 added this file to the `pull_request` paths for exactly this reason. Co-authored-by: lab <lab@example.com>
This was referenced Sep 5, 2026
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
1 participant
Add this suggestion to a batch that can be applied as a single commit.This suggestion is invalid because no changes were made to the code.Suggestions cannot be applied while the pull request is closed.Suggestions cannot be applied while viewing a subset of changes.Only one suggestion per line can be applied in a batch.Add this suggestion to a batch that can be applied as a single commit.Applying suggestions on deleted lines is not supported.You must change the existing code in this line in order to create a valid suggestion.Outdated suggestions cannot be applied.This suggestion has been applied or marked resolved.Suggestions cannot be applied from pending reviews.Suggestions cannot be applied on multi-line comments.Suggestions cannot be applied while the pull request is queued to merge.Suggestion cannot be applied right now. Please check back later.
Refs #3316
Two of the four remaining FIXes from the never-green triage. A third is
withdrawn — my diagnosis of it was wrong.
coq-proofs.yml— never passed, and could not verify its own repairoptions: --user rootruns the container as root, but the coqorg imageinitialises opam for the
coquser under/home/coq/.opam. As rootOPAMROOTdefaults to
/root/.opam, which does not exist:OPAMROOTnow points at the root the image actually built, and each stepre-enters the switch, because a new step is a new shell.
--user rootstays —checkout writes into a workspace root owns.
Separately:
push:listed this workflow file in its paths andpull_request:did not, so a PR repairing this workflow could not run it, and any repair
shipped unverified. That is presumably how it stayed broken since August. Added
— and it is what lets this PR check its own fix.
brain-seal-refresh.yml— a step that cannot succeedCommit brain sealsrunsgit pushto master. The branch ruleset refuses that,so all three runs ever (2026-04-07, 2026-06-01, 2026-08-28) end:
and only that step ever failed — aggregation, schema validation and artifact
upload passed every time. Removed rather than worked around: pushing to master is
what the ruleset exists to prevent, and refreshing seals on master needs a PR,
which is a different change.
permissionsdropscontents: write→read.What the job now reports is whether the seals still validate against
BRAIN_SEAL_SCHEMA— the signal the permanent red was burying.lean-proofs.yml— withdrawn, I was wrong8571 of 8574 targets build. The two that fail are marked in the source:
norm_numdoes not evaluateReal.pi,Real.exporReal.sqrt. The job is redbecause it is telling the truth, and the workflow's own header already says that
outcome is the finding. Nothing to fix in the workflow. Closing the two goals is
real analysis, not configuration.