From 996e80c2636d63a2a1045c2ac47d023363566565 Mon Sep 17 00:00:00 2001 From: "Jonathan D.A. Jewell" <6759885+hyperpolymath@users.noreply.github.com> Date: Mon, 27 Jul 2026 18:37:16 +0100 Subject: [PATCH] fix(ci): make the secret scanner and the Lean proof gate actually run MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit Both workflows were rejected by Actions before a runner was ever allocated, so neither gate has produced a single result in this repo. Two independent parse faults, one per file. secret-scanner.yml — the job key `scan:` sat at column 0, a sibling of `jobs:` rather than a child, so `jobs:` parsed as null and Actions refused the file. This is valid YAML but invalid Actions, which is why YAML-based linting never flagged it: a `yaml.safe_load` sweep of all 22 workflows in this repo passes it. The practical consequence is that the job-level `permissions:` block added in #124 was attached to a key Actions ignores, so that fix has been inert and **gitleaks has never executed here**. The reusable pin is untouched. lean-proofs.yml — three `- name:` values contain an unquoted ": ", e.g. "(§7.1 not-regular: DFA + pigeonhole)". An unquoted YAML scalar may not contain ": ", so the file failed to parse at line 60. Quoted all three. Worth stating plainly, because it inverts the usual failure mode in this estate: lean-proofs.yml is an *honest* gate. It installs the pinned Lean toolchain and runs `lean ` with no `|| true`. It is not a fake gate that passes when it shouldn't — it is a real gate that has never run. The proofs behind it are green (verified locally: 6 Lean under pinned 4.30.0 and 3 Coq under 8.20.1 all pass, with zero sorry, Admitted, axiom or Parameter), so nothing has rotted; the guard was simply switched off. Verification: all 22 workflow files now pass a structural check that mirrors what Actions requires — parses as a mapping, has a trigger, and `jobs` is a non-empty mapping whose every job has `steps` or `uses`. Both faults produce the same signature and are worth recognising: the run is listed by file path instead of workflow name, and `gh run view --log-failed` returns "log not found". `gh pr checks` shows nothing at all, because a parse-rejected workflow creates no check run. Co-Authored-By: Claude Opus 5 --- .github/workflows/lean-proofs.yml | 6 +++--- .github/workflows/secret-scanner.yml | 2 +- 2 files changed, 4 insertions(+), 4 deletions(-) diff --git a/.github/workflows/lean-proofs.yml b/.github/workflows/lean-proofs.yml index d1f66b8..0ad0707 100644 --- a/.github/workflows/lean-proofs.yml +++ b/.github/workflows/lean-proofs.yml @@ -57,19 +57,19 @@ jobs: lean docs/proofs/verification/WokeGrammarStructure.lean echo "✅ WokeGrammarStructure.lean verified" - - name: Verify WokeGrammarRegular.lean (§7.1 not-regular: DFA + pigeonhole) + - name: "Verify WokeGrammarRegular.lean (§7.1 not-regular: DFA + pigeonhole)" run: | set -euo pipefail lean docs/proofs/verification/WokeGrammarRegular.lean echo "✅ WokeGrammarRegular.lean verified" - - name: Verify WokeGrammarCFL.lean (§7.3 CFL closure: union/concat/star) + - name: "Verify WokeGrammarCFL.lean (§7.3 CFL closure: union/concat/star)" run: | set -euo pipefail lean docs/proofs/verification/WokeGrammarCFL.lean echo "✅ WokeGrammarCFL.lean verified" - - name: Verify WokeGrammarPumping.lean (§7.3 non-closure: pumping foundation) + - name: "Verify WokeGrammarPumping.lean (§7.3 non-closure: pumping foundation)" run: | set -euo pipefail lean docs/proofs/verification/WokeGrammarPumping.lean diff --git a/.github/workflows/secret-scanner.yml b/.github/workflows/secret-scanner.yml index 664f803..6c8ddaf 100644 --- a/.github/workflows/secret-scanner.yml +++ b/.github/workflows/secret-scanner.yml @@ -10,7 +10,7 @@ concurrency: permissions: contents: read jobs: -scan: + scan: # The reusable's gitleaks job requests pull-requests: write (PR summary # comment) and actions: read (workflow-run metadata) at job level; the # caller must grant at least that or the run startup-fails.