fix(ci): run the Kernel Admitted gate under bash, not the container dash - #3397
Merged
Conversation
… dash Refs #3396 The step declares no shell key and neither does the job, so it inherits the coqorg/coq container default of `sh -e` -- dash -- while its body uses four bash-only constructs: VFILES=(), VFILES+=(...), ${#VFILES[@]} and `done < <(...)`. Dash rejects the first of them with a syntax error before opening any file. Measured on the body extracted verbatim from this workflow, against the nine .v files coq/_CoqProject names, materialised from master: dash clean exit 2 Syntax error: "(" unexpected dash planted exit 2 Syntax error: "(" unexpected bash clean exit 0 reading 9 file(s) named by coq/_CoqProject bash planted exit 1 reading 9 file(s) named by coq/_CoqProject Identical under dash in both states: the gate carried no information. The bash rows are the positive control -- they show the probe can separate the two states, so the dash rows are a finding and not a broken probe. Note that macOS /bin/sh is bash 3.2 and accepts arrays, so it cannot serve as the control here; /bin/dash was used. The class was enumerated rather than assumed: of 50 workflow files, 4 use a container, and this is the only step in any of them that combines a container with a bash-only construct. The `<<<` in rings-rust.yml sits in the `discover` job, which runs on ubuntu-latest with no container and so already gets bash. The body is unchanged. `set -eu` is kept -- Actions invokes a bash step with -eo pipefail already, and the dash rationale that originally chose it no longer applies, so the comment saying so is corrected in place. Co-Authored-By: Claude Opus 5 <noreply@anthropic.com>
gHashTag
enabled auto-merge (squash)
September 7, 2026 16:21
Contributor
|
📓 NotebookLM Notebook linked to this PR
This notebook contains session context, decisions, and artifacts for this work. |
Contributor
This was referenced Sep 7, 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.
Closes #3396
The Kernel PHI
Admittedgate could not fail for the reason it exists, and could not pass for that reason either: under the container shell it died on syntax before reading a single file.The defect
The step declares no
shell:key and neither does the job, so it inherits thecoqorg/coqcontainer defaultsh -e— dash. Its body uses four bash-only constructs:The step comment already stated the constraint — "the step shell is
sh -e-- dash" — and the code below it violated it.Measured
Body extracted verbatim from the workflow (89 lines; the extractor refuses if the result does not contain
VFILES, so a silent empty extract cannot masquerade as a passing probe — it did exactly that on the first attempt and was caught). Run against a tree holding the 9.vfilescoq/_CoqProjectnames, materialised from master.Syntax error: "(" unexpectedAdmitted.planted incoq/Kernel/Trit.vSyntax error: "(" unexpectedreading 9 file(s) named by coq/_CoqProjectAdmitted.plantedreading 9 file(s) named by coq/_CoqProjectUnder the CI shell the gate returned the same thing in both states — it carried no information. The bash rows are the positive control: they show the probe can separate the two states, so the dash rows are a finding rather than a broken probe.
macOS
/bin/shis bash 3.2 and accepts arrays, so it passes this body and proves nothing./bin/dashwas used. That trap is now recorded in the workflow comment.Class enumerated, not assumed
Of 50 workflow files, 4 use a container (
coq-kernel,coq-proofs,rings-rust,vivado-synth). This is the only step in any of them that combines a container with a bash-only construct. The<<<inrings-rust.ymlis in thediscoverjob, which runs onubuntu-latestwith no container and already gets bash.Scope
One
shell: bashkey. The gate body is unchanged, and the other 7 steps in the job keep no shell key.set -euis kept — Actions invokes a bash step asbash --noprofile --norc -eo pipefail {0}, so pipefail is already on; the dash rationale that originally choseset -euis gone with the shell, and the comment saying so is corrected in place rather than left to mislead.Not fixed here
The meta-gate written to protect this gate extracts the body correctly and then runs it through
subprocess.run(["bash", "-c", body])— a different shell from CI. It passes 13/13 on the body dash refuses. That is the larger half and is left in #3396 as context; a guard that does not use the shell it guards will keep certifying bodies CI cannot run.