Repository navigation
ci: weekly track-latest for the Lean toolchain and sibling pins - #42
Merged
hyperpolymath merged 3 commits intoOct 14, 2026
Merged
Conversation
The maintainer wants every pin kept up to date and checked against the latest version, through reviewed PRs, never silently. - track-lean.yml: weekly, tries the newest stable Lean (a vX.Y.Z tag of leanprover/lean4) and runs the three CLAUDE.md gates. Green opens a PR (lean-toolchain, README, a STATE entry with the gate output verbatim). Red opens an issue with the failing output. - track-siblings.yml: weekly, runs scripts/check-correspondence.sh against each sibling's HEAD. Green makes one re-pin commit per sibling (fetch-siblings.sh and the doc's pin table together, re-checked) in one PR. A missing name opens an issue and leaves the pin unchanged. Names only; F6 still needs the sibling diff read. - Neither workflow has `uses:`; Lean comes from elan's installer. Dry runs of the same logic here: - Lean v4.35.0: Build completed successfully (15 jobs); sorry grep empty; #eval orbit unchanged. The first run will open a v4.35.0 PR. - choreographic-types edb784a->ec08c7a and resource-algebra cf9235c->638dd3e both PASS; tropical-types is current. The Lean headers now say "pinned in scripts/fetch-siblings.sh" instead of naming a SHA, so a re-pin leaves no stale SHA in prose. ROADMAP 3d records the decision: depend on tropical-types and track latest. Gates: lake build -> Build completed successfully (15 jobs); grep -rnw sorry empty; #eval orbit unchanged; check-correspondence.sh PASS; actionlint 1.7.7 with shellcheck clean. Rung: 3 (3d decision recorded; rung stays OPEN) Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01VTeVWDEJgdYKsUNr4uhnXX
|
Warning Review limit reachedYou've used all free OSS reviews for now. Wait for the free limit to reset to keep reviewing this public repository. Next included review available in 19 minutes. View limit details
Thanks for using CodeRabbit! It's free for OSS, and your support helps us grow. If you like it, consider giving us a shout-out. Comment |
hyperpolymath
marked this pull request as ready for review
October 14, 2026 08:44
hyperpolymath
added this pull request to stack #43
October 14, 2026 08:48
Owner
Author
|
Neither red check here is caused by this PR. Both are also red on
Generated by Claude Code |
hyperpolymath
added a commit
that referenced
this pull request
Oct 14, 2026
## One root cause behind both red checks `.github/workflows/actions.lock` drifted. It does this in two ways: | Check | Why it fails | Evidence | |---|---|---| | `CI` → `startup_failure` (no check run at all) | Dependabot (#34) bumped `ci.yml` to `leanprover/lean-action@v1.6.1` and `codeql.yml` to `github/codeql-action@v4.38.2`, but the lock still names `v1.6.0` / `v4.38.0`. | Every `CI` run since #34 (runs 78–81) | | `estate-audit` → silent exit 1 | The lock pins `hyperpolymath/cicd-suite@main` to `5a10b72`. That is before hyperpolymath/cicd-suite#32 (`fa71ac2`, 22 Sept) fixed the Required Files Gate's `grep -v … \| wc -l` under `-e -o pipefail` on a comment-only CODEOWNERS. | Reproduced locally at `5a10b72`. Upstream `main` now uses `grep -cvE … \|\| true`. | So the upstream gate bug is **already fixed**, and nothing needs filing on cicd-suite. marches just needs its lock advanced. **Why Dependabot keeps causing this.** dependabot-core can rewrite `actions.lock`, but only behind a server-side experiment (`Experiments.enabled?(:github_actions_lockfile)` in `github_actions/file_fetcher.rb`). That isn't something `dependabot.yml` can enable, so every Actions bump will drift the lock again until GitHub rolls it out. ## The fix: relock remotely, automatically New `.github/workflows/actions-lock.yml` runs the official extension, `github/gh-actions-lock` (pinned **v0.2.0**, the latest release, 12 Oct), on GitHub's runners: - **When:** - On every push to `main` that changes a workflow, so a merged Dependabot bump is relocked within minutes. - Weekly on Monday, after Dependabot, so branch pins like `cicd-suite@main` track latest. - On demand. - **What:** `gh actions-lock --relock --no-narrow --no-migrate-local-actions`, scoped to two groups: - the workflows the lock already tracks; - every workflow with no `uses:`, which is recorded as `[]` with nothing to rewrite. A workflow that has refs but isn't tracked yet, i.e. the estate's canonical `secret-scanner.yml` caller, is never onboarded automatically, because v0.2.0 may turn its SHA ref into a tag. - **Guard:** a run that would change anything but `actions.lock` is refused, the same assert as #25. Otherwise it opens or updates a lockfile-only PR from `ci/relock-actions`. - **No `uses:`**, so it runs precisely when the lock is stale. This follows `labels.yml`. - **Token:** it falls back to `GITHUB_TOKEN`. Two repo settings matter: 1. **Settings → Actions → General → "Allow GitHub Actions to create and approve pull requests"** must be on, or `gh pr create` fails. 2. A PR opened with `GITHUB_TOKEN` does not trigger CI. Adding one secret, **`AUTOMATION_TOKEN`** (a fine-grained token on this repo with Contents, Issues, Pull requests and Workflows set to read/write), makes CI run on the bots' PRs. It also covers the case where GitHub refuses a `GITHUB_TOKEN` write under `.github/workflows/`. The track-latest workflows in #42 share it. **Merging this starts the first relock automatically**, because it's a push to `main` that touches a workflow. I'll watch that run and the PR it opens. ## Checks ``` $ actionlint -shellcheck=$(which shellcheck) .github/workflows/actions-lock.yml # v1.7.7 (clean) ``` The run itself can only be exercised on GitHub. This sandbox can't reach the GitHub API, which is why the relock has to run remotely in the first place. The scope computation was dry-run locally and picks `actions-lock.yml`, `ci.yml`, `codeql.yml`, `label-triage.yml`, `labels.yml`, `main-estate-audit.yml` and `pages.yml`. This PR's own `CI` and `estate-audit` will still be red, for the reasons above. The relock PR fixes both. 🤖 Generated with [Claude Code](https://claude.com/claude-code) https://claude.ai/code/session_01VTeVWDEJgdYKsUNr4uhnXX --------- Co-authored-by: Claude <noreply@anthropic.com>
hyperpolymath
added a commit
that referenced
this pull request
Oct 14, 2026
…n copy (#44) Not a rung (CI). This is the marches half of hyperpolymath/cicd-suite#50. ## Why `estate-audit` failed after 8s - The 26-step copy of cicd-suite's workflow held here was frozen by `actions.lock` at `cicd-suite@5a10b72`. That commit predates cicd-suite #32, which fixed the Required Files Gate. - All 26 gates ran in one job, so the first failure masked the rest. - `prat` and `semantic-audit` were stubs that could not fail. ## What changes - **`.github/workflows/main-estate-audit.yml`** is now a ten-line caller of cicd-suite's reusable audit, pinned at a full SHA. It reports five checks (`estate / governance`, `hygiene`, `manifests`, `languages`, `advisory`), and each runs every gate even after one fails. The stubs are gone. - **`.github/workflows/actions.lock`:** the caller is de-onboarded by cicd-suite's `scripts/deonboard-estate-audit.sh`. This removes its entry and the three dependencies only it reached (`cicd-suite@main`, `deed-ecosystem@f9d999b`, `k9-ecosystem@2155aa2`), and adds nothing. Onboarded, a cross-repo reusable call startup-fails with zero jobs under `sha_pinning_required`. The relock workflow in #41 scopes itself to tracked workflows plus those with no `uses:`, so it leaves the caller out. - **`.github/workflows/track-estate-audit.yml`** (new, no `uses:`): each week it opens a PR that moves the pin to cicd-suite HEAD, and that PR's own audit run is the check. If someone has pushed a commit to its branch, it leaves the branch alone rather than force-pushing over it. It needs `AUTOMATION_TOKEN`, the same secret #41 and #42 use, with Pull requests and Workflows set to write. - **STATE.adoc** entry. ## Merge order The pin is `afa28ff`, the head of cicd-suite#50, so this PR's pull_request run exercises the cross-repo call for real. **Merge cicd-suite#50 first.** I will then re-pin this PR to #50's merge commit before it leaves draft. cicd-suite's current `main` (`4f54042`) is also callable, since it has had `workflow_call` since cicd-suite #7. However, it is the old single-job, 26-step audit. Until #50 merges, the weekly bot would propose moving back to it. ## Verification - **On this PR:** all five `estate / *` checks are green against cicd-suite #50. - **Lint:** actionlint 1.7.7 is clean on both workflows. - **Lean gates:** - `lake build` → `Build completed successfully (15 jobs).` - `grep -rnw sorry` is empty. - `#eval orbit` prints `[(false, false), (true, true), (false, false), (true, true)]`. - No Lean file changed. - **Local harness:** cicd-suite's 24 composite gates at `1aa6bfb` were run as composite steps (`bash -e -o pipefail`) against this branch, and all 24 exit 0. Negative control: with the gates at `5a10b72`, required-files fails, which reproduces the original failure. ## Expected red, not caused by this PR `CI` and `CodeQL` end in `startup_failure` on main too. Dependabot (#34) bumped `lean-action` and `codeql-action` without relocking, so the lock drifted. The fix is #41's relock workflow, which takes effect after #41 merges. 🤖 Generated with [Claude Code](https://claude.com/claude-code) https://claude.ai/code/session_01VTeVWDEJgdYKsUNr4uhnXX --------- Co-authored-by: Claude <noreply@anthropic.com>
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
2 participants
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.
Stacked on #41 (the
actions.lockrelock). This implements the maintainer's choice that every pin stay up to date and checked against latest. Changes always arrive as reviewed PRs, never as silent pushes.What
track-lean.ymlvX.Y.Ztag of leanprover/lean4) and runs the three CLAUDE.md gateslean-toolchainand README, plus a STATE entry with the gate output verbatimtrack-siblings.ymlscripts/check-correspondence.shagainst each sibling's HEAD (choreographic-types, resource-algebra, tropical-types)fetch-siblings.shand the doc's pin table together, re-checked), all in one PRNeither workflow has
uses:steps. Lean comes from elan's installer, so the lock never blocks them, and #41's relock records them as[]. Both useAUTOMATION_TOKENif it's set, otherwiseGITHUB_TOKEN(see #41).Names only. The sibling re-pin PR says so explicitly: whether a re-pinned name still means the same thing is falsifier F6, so the linked sibling diff must be read before merging.
What the first runs will do
I dry-ran the same logic here:
Build completed successfully (15 jobs)., thesorrygrep is empty and#eval orbitis unchanged, so the first run opens a v4.35.0 PR.edb784a→ec08c7a:PASS. resource-algebracf9235c→638dd3e:PASS. tropical-types is already current. So the first run opens a re-pin PR with two commits.Also in this PR
Cut.leanandTropical.leannow say "pinned in scripts/fetch-siblings.sh" instead of naming a SHA, so a re-pin leaves no stale SHA in prose. The dated history in STATE and FALSIFIERS is left alone.Checks (this head)
The shellcheck suppressions are line-level and annotated. They cover SC2016 (Markdown backticks in printf formats are intended) and SC2153 (
ORBITcomes from the jobenv:).CIandestate-auditstay red until #41's first relock PR lands, for the reasons given in #41.🤖 Generated with Claude Code
https://claude.ai/code/session_01VTeVWDEJgdYKsUNr4uhnXX
Generated by Claude Code