docs(skill): ci-gates 598 — a gate and its guard must run the same shell - #3398
Merged
Conversation
…hell Refs #3396 Records the coq-kernel Admitted defect as a rule rather than an incident. The step inherited the coqorg/coq container's `sh -e` (dash) and used four bash-only constructs, so it exited 2 before opening any file -- the same exit on a clean tree and on one with an `Admitted.` planted. A constant is not a verdict. Four things the section makes reusable: - A guard must invoke its subject the way the runner will. The meta-gate written to protect this step extracted the body correctly and then ran it through `bash -c`, and passed 13/13 on a body dash refuses. - `sh` is a role, not a program. On macOS /bin/sh is bash 3.2 and accepts arrays, so it is a false-negative control; ask `/bin/sh -c 'echo $BASH_VERSION'` before treating sh as evidence of POSIX-compatibility. - A comparison table needs at least one row where the instrument moves. The first attempt produced four cells of exit 0 because the extractor silently returned an empty body; it was caught by making the extractor refuse, not by reading the table. - Enumerate the class: 4 of 50 workflows use a container, and only this step combined one with a bash-only construct. Append-only: the file's first 17402 lines are byte-identical to master. The duplicate section numbers 546/547/548 are pre-existing on master and are left alone. Co-Authored-By: Claude Opus 5 <noreply@anthropic.com>
Contributor
|
📓 NotebookLM Notebook linked to this PR
This notebook contains session context, decisions, and artifacts for this work. |
Contributor
Refs #3396 The CI gate requires every PR to add a docs/now/ entry; the local pre-commit hook only requires that a recent entry exists somewhere in the tree, so it passed on a change that adds none. The gate's own message names the divergence. Co-Authored-By: Claude Opus 5 <noreply@anthropic.com>
Contributor
|
📓 NotebookLM Notebook linked to this PR
This notebook contains session context, decisions, and artifacts for this work. |
Contributor
PR DashboardGenerated at: 2026-09-07 16:30:38 UTC
Summary
Seal Status
|
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 #3396
Turns the
coq-kernelAdmitteddefect (fixed in #3397) into a rule other gates can be checked against, rather than leaving it as one incident.What the section records
The step inherited the
coqorg/coqcontainer defaultsh -e— dash — and used four bash-only constructs, so it exited 2 before opening any file: the same exit on a clean tree and on one with anAdmitted.planted. A constant is not a verdict.Four reusable rules come out of it:
subprocess.run(["bash","-c",body])— a different shell from CI. It passes 13/13 on the body dash refuses. The extraction was the careful part; the invocation was the assumption.shis a role, not a program. The obvious control — run the body undersh— is a false negative on macOS, where/bin/shis bash 3.2 and accepts arrays. Ask/bin/sh -c "echo $BASH_VERSION"before treatingshas evidence of POSIX-compatibility; use/bin/dashagainst a Debian-family container.exit 2under dash reads as a broken probe rather than a finding. The first attempt at this measurement produced four cells ofexit 0because the extractor had silently returned an empty body — caught by making the extractor refuse (assert "VFILES" in body), not by reading the plausible table.<<<inrings-rust.ymlis in a container-less job.It also records that
Coq kernelis not among the four required contexts, so #3397 auto-merged on the required four while the Coq run was still in progress — the merge gate can say nothing about a change to a non-required workflow.Shape of the change
Append-only. Verified mechanically before committing: the first 916,851 characters of the file are byte-identical to
origin/master, fenced-code-block lines are unchanged at 347, and section numbers go 559 → 560 with598unique.Pre-existing, not touched
Section numbers 546, 547, 548 each appear twice, and the duplicate set is identical on
origin/masterbefore this change — the collision is not introduced here. Left alone rather than silently renumbered; filed separately so a renumber can be reviewed on its own.