Repository navigation
chore(deps): bump the actions group with 2 updates - #34
Merged
Merged
Conversation
Bumps the actions group with 2 updates: [leanprover/lean-action](https://github.com/leanprover/lean-action) and [github/codeql-action](https://github.com/github/codeql-action). Updates `leanprover/lean-action` from 1.6.0 to 1.6.1 - [Release notes](https://github.com/leanprover/lean-action/releases) - [Changelog](https://github.com/leanprover/lean-action/blob/main/CHANGELOG.md) - [Commits](leanprover/lean-action@v1.6.0...v1.6.1) Updates `github/codeql-action` from 4.38.0 to 4.38.2 - [Release notes](https://github.com/github/codeql-action/releases) - [Changelog](https://github.com/github/codeql-action/blob/main/CHANGELOG.md) - [Commits](github/codeql-action@v4.38.0...v4.38.2) --- updated-dependencies: - dependency-name: leanprover/lean-action dependency-version: 1.6.1 dependency-type: direct:production update-type: version-update:semver-patch dependency-group: actions - dependency-name: github/codeql-action dependency-version: 4.38.2 dependency-type: direct:production update-type: version-update:semver-patch dependency-group: actions ... Signed-off-by: dependabot[bot] <support@github.com>
dependabot
Bot
added
dependencies
|
Important Review skippedBot user detected. To trigger a single review, invoke the ⚙️ Run configuration
You can disable this status message by setting the Use the checkbox below for a quick retry:
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
approved these changes
Oct 8, 2026
hyperpolymath
added a commit
that referenced
this pull request
Oct 14, 2026
) **Stack 2/3 for MRC-01 (rung 3).** Stack 1/3, the toolchain move to v4.34.0, merged as #36. Next: `…-docs` (correspondence table, falsifier, STATE/ROADMAP), stacked on this branch. ## `Marches/Cut.lean` (new) A **cut** of the region DAG is a set of regions closed under predecessors: every region that can cross into the cut is in it. This is classical downward closure. It is *not* choreographic-types' party-indexed `Consistent`, which is a merge condition at choices; the next PR in the stack records that as a falsifier finding. | Theorem | Says | |---|---| | `Cut.edge_crosses_past` | In an acyclic graph every edge `r → r'` leaves the principal cut `↓r`. | | `Cut.path_back_crosses_no_cut` | Negative: an edge on a cycle crosses no cut. `Acyclic` is load-bearing. | | `DiscSys.trace_cross_crosses_cut` | **Every crossing in a well-typed composite trace crosses a cut** that holds the trace's start and not its end. | | `DiscSys.trace_mem_back`, `trace_inside` | A trace that ends in a cut was inside it all along, and fired every label inside it. | | `DiscSys.no_reentry` | A trace that leaves a cut never re-enters it. This is `no_back_cross` lifted from one interface to every cut. | | `DiscSys.composeCut` | **Prefix-closure: `compose` restricted to a cut prefix is a `Discipline`.** | | `composeCut_trace_embed` / `composeCut_trace_reflect` | Its traces are exactly the composite's traces that end in the prefix: the frontier's future is irrelevant to the prefix. | | `trace_cross_crosses_cut`, `trace_stays_in_B` | The same results for the two-region `Interface` of `Compose.lean`, read as the 2-node DAG `Reassembly.boolUp`. | | `CutExhibit.*` | A concrete `twoTropical` trace that instantiates the theorems, plus a negative control on a self-loop. | ## `Marches/Tropical.lean`: the grade at the crossing `TropicalGrade` reads `TropicalNat` as a (min,+) grade: `alt = min`, `seq = +`, `one = 0`. - K-4 laws: `seq_unitl` (`𝟙 ⊗ x = x`) and `alt_idem` (`x ⊕ x = x`). - S-3 inside marches: `better_reverses_altLe`. `better` runs **with** cost, while the ⊕-induced order runs **against** it, as in resource-algebra's Loss and opposite to its MaxPlus. `altLe_one` puts `𝟙` at the top, as Loss's `fin 0`. `s3_witness` uses the same numbers as resource-algebra's S-3 (`2 ≼ 1`). - The Agda side is not imported or re-declared. `altLe` is marches' own order, and the doc comment says so. ## Evidence (local, Lean v4.34.0) ``` $ rm -rf .lake && lake build Build completed successfully (15 jobs). $ grep -rnw sorry Marches/ Marches.lean ; echo $? 1 $ lake env lean Marches/BadGadget.lean [(false, false), (true, true), (false, false), (true, true)] ``` `#print axioms` over all 45 declarations added in `Cut.lean` and `TropicalGrade`: every one reports `does not depend on any axioms`. I re-proved three grade lemmas that had picked up `propext` through core `Nat` lemmas, to match the existing kernel, which is also axiom-free. `grep -ni converg Marches/Cut.lean` → only the delimitation line (45). ## CI: two red checks that are not this PR's - **`CI` (the `lake build` + no-sorries job) ends in `startup_failure`.** This has happened on every run since the Dependabot bump #34 (runs 78–81, including on `main`). That bump moved `ci.yml` to `leanprover/lean-action@v1.6.1` and `codeql.yml` to `codeql-action@v4.38.2`, but `.github/workflows/actions.lock` still pins `@v1.6.0` / `@v4.38.0`. The lockfile is enforced at startup ("Using locked action versions from the workflow's lockfile"). Fix: re-run `gh actions-lock` on `main`, as #25 did. I have not hand-edited the machine-generated lockfile. Until that lands, the local gate output above is the build evidence. - **`estate-audit` fails at the Required Files Gate.** This is red on `main` since at least run 41 (1 Oct). Reproduced locally against `cicd-suite@5a10b72`: the gate runs under `bash -e -o pipefail`, and for this repo's comment-only `.github/CODEOWNERS`, `functional_lines=$(grep -vE '^\s*(#|//|;|$)' "$f" | wc -l)` selects no lines. `grep` exits 1, pipefail fails the assignment, and the step exits with no `::error::`. That is the very case the gate's "Rule 1" means to allow. The fix belongs in hyperpolymath/cicd-suite, e.g. `{ grep -vE … "$f" || true; } | wc -l`. ## Status rows New README rows are PROVEN by `lake build`, and "conditional" where they consume `Acyclic`. No cross-prover claim is made in this PR. Rung 3 stays OPEN. 🤖 Generated with [Claude Code](https://claude.com/claude-code) https://claude.ai/code/session_01VTeVWDEJgdYKsUNr4uhnXX --- _Generated by [Claude Code](https://claude.ai/code/session_01VTeVWDEJgdYKsUNr4uhnXX)_ Co-authored-by: Claude <noreply@anthropic.com>
This was referenced Oct 14, 2026
hyperpolymath
added a commit
that referenced
this pull request
Oct 14, 2026
…tes (#38) **Stack 3/3 for MRC-01 (rung 3).** 1/3 merged as #36 (toolchain) and 2/3 as #37 (`Marches/Cut.lean` + K-4 laws). This branch was cut from #37's head before its squash. `main` has since been merged in, without rewriting history. The squash tree is byte-identical to that head, so the diff against `main` is only this PR's docs and shell glue, plus one Lean comment (the `Tropical.lean` seam note). ## What - **`docs/kcut-correspondence.adoc`**: marches' Lean names paired with choreographic-types' Agda names, at pinned commits. It is a table, not a link. Every pairing is **ASSUMED (port-and-reprove)**, in resource-algebra's M-2 idiom. Rows KC-1…KC-8 cover cuts, downward closure, K-5 (`cut-projectable`), K-2 (`proj-cut`), the K-4 laws, the S-3/W-4 direction, and M-2. - **`scripts/fetch-siblings.sh`**: clones the siblings at their pins into `_build/dependencies` (now git-ignored), using the choreographic-types pattern. Pins: choreographic-types `edb784a`, resource-algebra `cf9235c`, tropical-types `e172f8a`. - **`scripts/check-correspondence.sh`**: the mechanical part. It checks that every Lean name cited exists in this build (`#check`), that every Agda name exists at its pin, and that every pin appears in the table. Negative control: a fabricated Lean name and a fabricated Agda name go through the same checks and must be refused. It checks **names, not meanings**. - **`FALSIFIERS.adoc` F6**: "the correspondence is nominal." It **fires on one proposed row**. At `edb784a`, Agda's `Consistent p c` (`Projection.agda:89`) is a party-indexed merge condition at choices, and marches has no parties. So MRC-01's `Acyclic ↔ Consistent` pairing is withdrawn (KC-3, status OPEN). F6 stays open, narrowed. - **`Marches/Tropical.lean` seam note**: now points at resource-algebra M-2, and records where `TropicalAdapterPath.lean` actually lives (below). - **`ROADMAP.adoc` rung 3**: now a gated table. 3a–3c are met; 3d (TropicalAdapterPath import), 3e (echo-types bridge) and 3f (postern) are OPEN, so the rung stays OPEN and there is no tag. - **`STATE.adoc`**: records the session. **`README`** gets one ASSUMED row and a note on the check script; **`LIMITATIONS`** gets one bullet; **`ARCHITECTURE`** lists `docs/` and `scripts/`. ## Citation corrections found while reading the pins - T-2's `receiver-knows` / `sender-knows` are in `src/Choreographic/Instances.agda` (lines 172 and 177), not `Transport.agda`. `Transport.agda` holds the generic `knows-local-cut`. - `TropicalAdapterPath.lean` is in **hyperpolymath/tropical-types**. Its lake package is named `tropical-resource-typing`, which is the name the ROADMAP used. It is pinned to Lean **v4.13.0**, so expect friction when 3d imports it into v4.34.0. - marches' `TropicalNat` is min-plus, so it sits with `Loss`, not `MaxPlus`. It is not one of M-2's two (max-plus) objects (KC-8). ## Evidence (this head) ``` $ lake build Build completed successfully (15 jobs). $ grep -rnw sorry Marches/ Marches.lean ; echo $? 1 $ lake env lean Marches/BadGadget.lean [(false, false), (true, true), (false, false), (true, true)] $ scripts/check-correspondence.sh choreographic-types at edb784a resource-algebra at cf9235c tropical-types at e172f8a PASS: 15 Lean names and 16 sibling names exist at the pins; both negative controls refused $ shellcheck scripts/*.sh # clean $ grep -ni converg Marches/Cut.lean docs/kcut-correspondence.adoc scripts/*.sh Marches/Cut.lean:45: not protocol convergence; agda-routing owns that ground (LIMITATIONS.adoc). docs/kcut-correspondence.adoc:20:Delimitation: nothing here is a convergence claim; agda-routing owns that ``` Mutation test: I renamed one Lean name, one Agda name and one pin in the doc. The script printed `MISSING (Lean)`, `MISSING (sibling)` and `PIN NOT IN TABLE`, then `FAIL` with exit 1. Restoring the doc gives `PASS` again. ## postern Not reachable from this account on 2026-10-14 (`add_repo`: not found or no access; no `list_repos` match). No cross-issue was filed. The MRC-01 import plan is kept in the correspondence doc, ready to file. ## CI The same two pre-existing red checks as on `main` apply here, and neither is caused by this PR: - `CI` ends in `startup_failure`: `actions.lock` has drifted since #34. The fix is `gh actions-lock`, as in #25. - `estate-audit` fails because of a cicd-suite pipefail bug on a comment-only CODEOWNERS. The full diagnosis is in #37. `check-correspondence.sh` needs network access, so it is not wired into CI here. 🤖 Generated with [Claude Code](https://claude.com/claude-code) https://claude.ai/code/session_01VTeVWDEJgdYKsUNr4uhnXX --- _Generated by [Claude Code](https://claude.ai/code/session_01VTeVWDEJgdYKsUNr4uhnXX)_ --------- Co-authored-by: Claude <noreply@anthropic.com>
This was referenced Oct 14, 2026
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
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.
Bumps the actions group with 2 updates: leanprover/lean-action and github/codeql-action.
Updates
leanprover/lean-actionfrom 1.6.0 to 1.6.1Release notes
Sourced from leanprover/lean-action's releases.
Changelog
Sourced from leanprover/lean-action's changelog.
Commits
f061402chore: pin actions to commit SHAs (#193)96e0613chore: finalize v1.6.0 release (#188)Updates
github/codeql-actionfrom 4.38.0 to 4.38.2Release notes
Sourced from github/codeql-action's releases.
Changelog
Sourced from github/codeql-action's changelog.
Commits
2892aa5Merge pull request #4168 from github/update-v4.38.2-a6ef2c96f8ad03a3Trigger workflows98af865Update changelog for v4.38.2a6ef2c9Merge pull request #4156 from github/mario-campos/fix-validate-cmd1ef28a1Merge pull request #4166 from github/dependabot/github_actions/dot-github/wor...26cb08bMerge pull request #4163 from github/mbg/fix-getCommitOid-stubsf035ce3Merge pull request #4165 from github/dependabot/npm_and_yarn/npm-minor-8eaed9...5e4e255Rebuildb13f5f4Bump ruby/setup-rubyc87fe57RebuildDependabot will resolve any conflicts with this PR as long as you don't alter it yourself. You can also trigger a rebase manually by commenting
@dependabot rebase.Dependabot commands and options
You can trigger Dependabot actions by commenting on this PR:
@dependabot rebasewill rebase this PR@dependabot recreatewill recreate this PR, overwriting any edits that have been made to it@dependabot show <dependency name> ignore conditionswill show all of the ignore conditions of the specified dependency@dependabot ignore <dependency name> major versionwill close this group update PR and stop Dependabot creating any more for the specific dependency's major version (unless you unignore this specific dependency's major version or upgrade to it yourself)@dependabot ignore <dependency name> minor versionwill close this group update PR and stop Dependabot creating any more for the specific dependency's minor version (unless you unignore this specific dependency's minor version or upgrade to it yourself)@dependabot ignore <dependency name>will close this group update PR and stop Dependabot creating any more for the specific dependency (unless you unignore this specific dependency or upgrade to it yourself)@dependabot unignore <dependency name>will remove all of the ignore conditions of the specified dependency@dependabot unignore <dependency name> <ignore condition>will remove the ignore condition of the specified dependency and ignore conditions