diff --git a/.github/workflows/gate-topology.yml b/.github/workflows/gate-topology.yml index 7f51fa6b76..651df39014 100644 --- a/.github/workflows/gate-topology.yml +++ b/.github/workflows/gate-topology.yml @@ -30,7 +30,9 @@ jobs: run: python3 -m pip install --quiet pyyaml - name: Merge-critical workflows must not filter pull_request by branch - run: python3 scripts/ci/check_pr_branch_filters.py + run: | + python3 scripts/ci/check_pr_branch_filters.py --self-test + python3 scripts/ci/check_pr_branch_filters.py # A gate that does not fire is one way to get a green that means nothing; # a gate that fires and describes itself as deeper than it is, is another. diff --git a/.github/workflows/untrusted-input-gate.yml b/.github/workflows/untrusted-input-gate.yml index ef3dcc0a61..2a31d1f477 100644 --- a/.github/workflows/untrusted-input-gate.yml +++ b/.github/workflows/untrusted-input-gate.yml @@ -37,6 +37,9 @@ jobs: steps: - uses: actions/checkout@v6 + - name: Install pyyaml for structural workflow extraction + run: python3 -m pip install --quiet pyyaml + - name: The Admitted gate reads every file _CoqProject names, or says it could not # #3063. grep answers 0 matched / 1 no match / 2 cannot open, and an # `if` merges the last two. Runs here rather than in coq-kernel.yml so diff --git a/docs/now/2026-09-12-restore-topology-and-admitted-ci.md b/docs/now/2026-09-12-restore-topology-and-admitted-ci.md new file mode 100644 index 0000000000..454bd0c431 --- /dev/null +++ b/docs/now/2026-09-12-restore-topology-and-admitted-ci.md @@ -0,0 +1,10 @@ +# NOW -- Restore topology and Admitted CI (2026-09-12) + +## Two existing CI failures (Refs #3574) + +- Classify Gate Topology and Untrusted Input Gate as merge-critical in the topology checker and lower the unclassified ceiling from 27 to 26. This changes checker coverage, not GitHub branch protection. +- Exercise the topology checker against disposable positive and negative workflow trees, including branch filters, missing or malformed classified guards, and growth beyond the unclassified ceiling. +- Extract the named Admitted step structurally from workflow YAML, require its explicit Bash shell and a unique non-empty body, and execute existing file-population fixtures with GitHub's strict Bash flags. +- Declare PyYAML in Untrusted Input Gate and test extraction across comments, key ordering, indentation, and invalid or ambiguous step definitions. +- The explicit PyYAML installation adds one runner-shell step: shell census `run: steps` moves 248 to 249 and `the runner does` moves 227 to 228. Update the shell ledger with this intentional population change; no step is removed or hidden. +- Validation: all local Gate Topology commands and all 11 Untrusted Input Gate check steps pass. Hosted CI is to be verified on the separate PR; no Coq production step, compiler behavior, specification, or branch-protection setting changes. diff --git a/scripts/ci/check_pr_branch_filters.py b/scripts/ci/check_pr_branch_filters.py index 7393938f22..734ba7c7d2 100755 --- a/scripts/ci/check_pr_branch_filters.py +++ b/scripts/ci/check_pr_branch_filters.py @@ -43,7 +43,10 @@ """ import glob import os +from pathlib import Path +import subprocess import sys +import tempfile try: import yaml @@ -80,6 +83,10 @@ "corpus-ratchet.yml", "withdrawn-live-gate.yml", "harness-scratch.yml", + # These checks guard CI topology and untrusted workflow inputs themselves. + # Omitting them would let a branch filter hide either on a stacked PR. + "gate-topology.yml", + "untrusted-input-gate.yml", ) # The two lists above are a partition ONLY of the files they name. Everything @@ -97,7 +104,9 @@ # commit that discovers them and a gate that is red on the day it lands teaches # everyone to ignore red. It moves DOWN only: classify a file and lower this in # the same commit, so the next unclassified workflow cannot hide in the slack. -MAX_UNCLASSIFIED = 27 +# Classifying the two guards above takes the live population from 28 to 26. +# Lower the old ceiling (27), rather than raising it to bless the regression. +MAX_UNCLASSIFIED = 26 # Not merge-critical, and each exclusion is stated with its reason so that a # future reader can disagree with the reason rather than guess at the omission. @@ -284,5 +293,52 @@ def main(): return 0 +def self_test(): + """Exercise the real checker on disposable workflow trees, not this repo.""" + script = str(Path(__file__).resolve()) + clean = "on:\n pull_request:\njobs: {}\n" + failures = [] + + def probe(label, edits, expected, diagnostic): + with tempfile.TemporaryDirectory(prefix="gate-topology-") as root: + workflows = Path(root) / ".github/workflows" + workflows.mkdir(parents=True) + for name in MERGE_CRITICAL: + (workflows / name).write_text(clean) + for name, content in edits.items(): + path = workflows / name + if content is None: + path.unlink() + else: + path.write_text(content) + result = subprocess.run( + [sys.executable, script], cwd=root, capture_output=True, text=True, + timeout=30, + ) + ok = result.returncode == expected and diagnostic in result.stdout + print(f"{'ok' if ok else 'FAIL'}: {label}") + if not ok: + failures.append(label) + print(result.stdout + result.stderr) + + probe("clean classified tree passes", {}, 0, "CLEAN:") + for name in ("gate-topology.yml", "untrusted-input-gate.yml"): + for key in FILTER_KEYS: + probe( + f"{name} rejects pull_request.{key}", + {name: f"on:\n pull_request:\n {key}: [master]\njobs: {{}}\n"}, + 1, f"pull_request.{key}", + ) + probe("missing classified guard fails", {"untrusted-input-gate.yml": None}, + 1, "MISSING") + probe("malformed classified guard fails", {"gate-topology.yml": "on: [\n"}, + 1, "UNPARSEABLE MERGE-CRITICAL") + at_ceiling = {f"unclassified-{i}.yml": clean for i in range(MAX_UNCLASSIFIED)} + probe("existing debt at ceiling passes", at_ceiling, 0, "CLEAN:") + probe("one new unclassified workflow fails", + {**at_ceiling, "one-too-many.yml": clean}, 1, "UNCLASSIFIED ROSE") + return 1 if failures else 0 + + if __name__ == "__main__": - sys.exit(main()) + sys.exit(self_test() if "--self-test" in sys.argv else main()) diff --git a/scripts/ci/test_admitted_gate_reads_every_named_file.py b/scripts/ci/test_admitted_gate_reads_every_named_file.py index 765d9e8369..67462ac267 100644 --- a/scripts/ci/test_admitted_gate_reads_every_named_file.py +++ b/scripts/ci/test_admitted_gate_reads_every_named_file.py @@ -15,13 +15,14 @@ """ import os -import re import shutil import subprocess import sys import tempfile from pathlib import Path +import yaml + REPO = Path(__file__).resolve().parents[2] WF = REPO / ".github/workflows/coq-kernel.yml" STEP = "Verify Kernel PHI layer has no Admitted" @@ -34,12 +35,79 @@ def check(name, ok, detail=""): FAILURES.append(f"{name}: {detail}") -def step_body(): - y = WF.read_text() - m = re.search(rf"- name: {re.escape(STEP)}\n run: \|\n(.*?)(?=\n - |\n\Z)", y, re.S) - if not m: - return None - return "\n".join(l[10:] if l.startswith(" " * 10) else l for l in m.group(1).split("\n")) +def step_body(text=None): + """Read the actual build step, independent of YAML formatting. + + The old regex required `name` immediately followed by `run`. Adding the + required `shell: bash` and its explanation broke extraction. Do not loosen + a regex across step boundaries: parse YAML and require one unambiguous step. + """ + doc = yaml.safe_load(WF.read_text() if text is None else text) + if not isinstance(doc, dict): + raise ValueError("workflow must be a mapping") + jobs = doc.get("jobs") + build = jobs.get("build") if isinstance(jobs, dict) else None + steps = build.get("steps") if isinstance(build, dict) else None + if not isinstance(steps, list): + raise ValueError("build.steps must be a list") + matches = [s for s in steps if isinstance(s, dict) and s.get("name") == STEP] + if len(matches) != 1: + raise ValueError(f"expected exactly one build step named {STEP!r}, got {len(matches)}") + step = matches[0] + # The Coq container defaults to sh (dash), which cannot run these arrays. + # Running the fixture in bash must not hide a missing workflow shell key. + if step.get("shell") != "bash": + raise ValueError("the Admitted step must explicitly declare shell: bash") + body = step.get("run") + if not isinstance(body, str) or not body.strip(): + raise ValueError("the Admitted step must contain a non-empty run string") + return body + + +def extractor_tests(): + fixture = ( + "jobs:\n build:\n steps:\n" + f" - name: '{STEP}'\n" + " # An explanation between name and run must be harmless.\n" + " shell: bash\n" + " run: |\n" + " printf 'fixture\\n'\n" + " - name: Unrelated sibling\n" + " run: echo not-the-gate\n" + ) + check("comments, quoted names and shell do not hide the body", + step_body(fixture) == "printf 'fixture\\n'\n") + # A different indentation, key order and block style denote the same step. + reordered = {"jobs": {"build": {"steps": [ + {"run": "echo fixture\n", "shell": "bash", "name": STEP}, + ]}}} + check("key order and indentation do not select another body", + step_body(yaml.safe_dump(reordered, indent=4, sort_keys=False)) == "echo fixture\n") + step = {"name": STEP, "shell": "bash", "run": "echo fixture"} + for label, steps in ( + ("missing step", []), + ("duplicate step", [step, step]), + ("missing shell", [{"name": STEP, "run": "echo fixture"}]), + ("wrong shell", [{**step, "shell": "sh"}]), + ("empty body", [{**step, "run": ""}]), + ("non-string body", [{**step, "run": ["echo fixture"]}]), + ): + rejected = False + try: + step_body(yaml.safe_dump({"jobs": {"build": {"steps": steps}}})) + except ValueError: + rejected = True + check(f"extractor refuses {label}", rejected) + for label, text in ( + ("malformed YAML", "jobs: ["), + ("missing build job", yaml.safe_dump({"jobs": {"other": {"steps": [step]}}})), + ): + rejected = False + try: + step_body(text) + except (ValueError, yaml.YAMLError): + rejected = True + check(f"extractor refuses {label}", rejected) # The gate's operand list. Named here rather than taken from `files`, because the @@ -69,7 +137,10 @@ def arm(body, files, named=OPERANDS): for f, c in files.items(): with open(os.path.join(d, "coq/Kernel", f), "w") as fh: fh.write(c) - r = subprocess.run(["bash", "-c", body], capture_output=True, text=True, cwd=d) + r = subprocess.run( + ["bash", "--noprofile", "--norc", "-eo", "pipefail", "-c", body], + capture_output=True, text=True, cwd=d, timeout=30, + ) return r.returncode, r.stdout + r.stderr finally: shutil.rmtree(d, ignore_errors=True) @@ -80,12 +151,14 @@ def arm(body, files, named=OPERANDS): def main(): - body = step_body() - check("the step body was found in the workflow", body is not None, - f"no step named {STEP!r} with a literal run block -- this test would assert nothing") - if body is None: - print("\nFAILED:\n - extractor") + FAILURES.clear() + extractor_tests() + try: + body = step_body() + except (OSError, ValueError, yaml.YAMLError) as error: + print(f"\nFAILED:\n - extractor: {error}") return 1 + check("the unique bash step body was found in the workflow", True) rc, out = arm(body, {"Phi.v": CLEAN, "PhiFloat.v": CLEAN}) check("both files present and clean passes", rc == 0 and "OK: no Admitted" in out, f"rc={rc} out={out!r}") diff --git a/tools/census/shell.txt b/tools/census/shell.txt index 24c6e40091..0febd77dd9 100644 --- a/tools/census/shell.txt +++ b/tools/census/shell.txt @@ -2,10 +2,10 @@ WHICH INTERPRETER EACH GATE STEP IS HANDED TO, AND WHO SAYS SO workflow files read 51 jobs 72 - run: steps 248 + run: steps 249 who names the shell: - the runner does 227 no container, so bash -eo pipefail + the runner does 228 no container, so bash -eo pipefail a `shell:` key does 6 NOBODY 15 a container and no `shell:` key