chore(deps): bump github/codeql-action from 4.38.0 to 4.38.1 in the actions group - #326
Merged
Merged
Conversation
Bumps the actions group with 1 update: [github/codeql-action](https://github.com/github/codeql-action). Updates `github/codeql-action` from 4.38.0 to 4.38.1 - [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.1) --- updated-dependencies: - dependency-name: github/codeql-action dependency-version: 4.38.1 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
dependabot
Bot
added
dependencies
|
Important Review skippedBot user detected. To trigger a single review, invoke the ⚙️ Run configurationConfiguration used: Organization UI Review profile: ASSERTIVE Plan: Advanced Run ID: 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
Sep 26, 2026
hyperpolymath
deleted the
dependabot/github_actions/actions-71fcf20ecc
branch
September 26, 2026 20:45
arena-ai-coding-agent Bot
pushed a commit
that referenced
this pull request
Sep 27, 2026
Workflows have failed at creation with `startup_failure` since 2026-09-26. Root cause: cd9aa40 (dependabot, #326) bumped github/codeql-action 4.38.0 -> 4.38.1 in codeql.yml (+2 -2) and hypatia-scan.yml (+1 -1), but did not regenerate .github/workflows/actions.lock, which still pinned 4.38.0 in three places. The lockfile no longer validates against the workflows, so the lockfile gate rejects the runs before any job starts. This is the same failure mode, and the same fix, as 9c4b72b (the last green main commit): "Workflows fail at creation with `The lockfile could not be validated. Regenerate it by running gh actions-lock`." Scope: version strings only. * workflows: map — github/codeql-action@v4.38.0 -> v4.38.1 for codeql.yml and hypatia-scan.yml (the refs those files actually use). * dependencies: entry regenerated for 4.38.1. The commit hash is the PEELED tag commit, which is the convention the existing entry already follows (v4.38.0^{} = b96794f015dfd88f77b49b1c93e0fa7110f94c63, exactly the hash previously recorded). v4.38.1^{} = 1c5b675653bb5c22dbe9b12b556ec555138e09fd, resolved via `git ls-remote --tags https://github.com/github/codeql-action`. owner_id 9919 / repo_id 259445878 are unchanged — same repository. Relation to the existing convention is unchanged: the lock records the repo-level ref (github/codeql-action@v4.38.1) while the workflow files reference sub-paths (github/codeql-action/init@v4.38.1) — the lock normalised that the same way for 4.38.0. NOTE: regenerated by hand, not by `gh actions-lock` — the extension's release binary is not reachable from the environment this was prepared in. It is byte-faithful to the tool's convention (verified against the pre-existing 4.38.0 entry) but a maintainer run of `gh actions-lock` should be preferred if anything looks off. Because the failure mode is startup_failure, this could not be tested locally — it will only be confirmed by whether runs now start. Co-authored-by: arena-agent <297053741+arena-agent@users.noreply.github.com>
hyperpolymath
pushed a commit
that referenced
this pull request
Sep 27, 2026
…rBundle (#328) Reopens `main` for business: CI `Agda` has been red since 2026-09-26. ## Status | | | |---|---| | Last green on `main` | `9c4b72b5`, 2026-09-21T12:20 | | Red since | 2026-09-26T18:35 (three consecutive failing runs) | | Failing jobs | `cold-check` (Agda typecheck, exit 42) and `check` (kernel-guard, exit 1) | Both failures are real defects, not infrastructure. Two independent causes. ## Failure 1 — `kernel-guard.sh` classification drift (fixed, verified locally) `scripts/kernel-guard.sh` check B requires every `proofs/agda/Echo*.agda` to be named in `docs/echo-types/echo-kernel-note.adoc`. Three modules added by #325 and #327 were never classified: ``` kernel-guard: FAIL: unclassified Echo* module(s) — add to docs/echo-types/echo-kernel-note.adoc (and MAP.adoc tag): EchoBitNarrowingNumeric EchoExampleBitNarrowing EchoHaplotypeCollapsing ``` All three are **Tier 2** (each depends on a Tier-2 module — `EchoExampleBitNarrowing` on `EchoExampleTruncation`, `EchoBitNarrowingNumeric` on both of those, `EchoHaplotypeCollapsing` on `EchoAggregation` + `EchoNoSectionGeneric`). Check A (the funext-free certificate) **already passed** and still passes: `Echo` and `EchoKernel` are stdlib-only, no postulates, no escape pragmas, no funext imports. That certificate is intact. Verified locally — the guard is pure POSIX shell and needs no Agda: ``` kernel-guard: PASS — funext-free certificate enforced; classification in sync. EXIT=0 ``` ## Failure 2 — a missing invariant in `FiberBundle` (fixed, **awaits CI**) `EchoHaplotypeCollapsing.agda` did not typecheck. The defect is in `bundle-fiber-echoes`: ```agda record FiberBundle : Set where field haplotype : Haplotype representative : Clone fiber : List Clone -- no link to `haplotype` bundle-fiber-echoes : (b : FiberBundle) → List (HaploFiber (FiberBundle.haplotype b)) bundle-fiber-echoes b = map (λ c → c , refl) (FiberBundle.fiber b) ``` `HaploFiber h = Echo collapse h = Σ Clone (λ c → collapse c ≡ h)`, so the lambda demands `refl : collapse c ≡ FiberBundle.haplotype b` for an **arbitrary** `c` taken from `fiber b`. Those terms are not judgementally equal. Expected message: ``` collapse c != FiberBundle.haplotype b of type Haplotype when checking that the expression refl has type collapse c ≡ FiberBundle.haplotype b ``` This is **not a typo — the record is missing an invariant**, and the invariant is already documented one layer up. `docs/echo-types/applications/haplotype-collapsing.adoc`: > Nickel contracts enforce: > * `count == length clones` > * **every `clones[i].haplotype_id == haplotype_id`** The Nickel schema had the contract; the Agda record did not — then the module tried to *prove* a consequence of an invariant it never carried. **Fix:** make the invariant structural rather than re-imposed at the use site. ```agda record FiberBundle : Set where field haplotype : Haplotype representative : HaploFiber haplotype fiber : List (HaploFiber haplotype) ``` `bundle-fiber-echoes` becomes the field projection and needs no proof; `example-bundle` supplies genuine echoes. `example-count = refl` and `clone-count-aggregation` were checked against their definitions and are correct as they stood. Also drops the now-unused `map` / `length` imports. This is the same lesson as the Ephapax `region_shrink` falsity, arriving from the opposite direction: there, an invariant kept in a per-use side-condition produced a *false* lemma; here, an invariant kept out of the carrier produced an *unprovable* one. **This half is reasoned, not machine-verified.** No Agda toolchain is reachable in the environment this was prepared in (GitHub release assets are network-blocked and Agda is not installable from source there), so the fix could not be typechecked locally. **It needs this PR's `Agda` run to confirm.** If the error differs from the prediction above, the reasoning has a hole and the diagnostic is wrong — please paste the actual output rather than merging. ## Side findings (not fixed here) 1. **`EchoBitNarrowingNumeric` and `EchoExampleBitNarrowing` are unreachable from every CI target.** The cold-check compiles only `All.agda`, `Smoke.agda`, `characteristic/All.agda`, `examples/All.agda` and `EchoImageFactorizationPropCubical.agda`. Neither module is imported by any of them, so both are **never typechecked by CI** — they only tripped a grep. #325's own message notes they were recovered "from unpushed commits". These are currently unverified. 2. **`docs/echo-types/MAP.adoc`** names `EchoHaplotypeCollapsing` but neither bit-narrowing module. `kernel-guard.sh` only checks the kernel note, so this is not a gate failure — but it is drift, and adding entries needs an editorial call on placement. ## Note on this branch This branch comes from a structural audit of the six-repo estate (`echo-types`, `ephapax`, `affinescript`, `systemet`, `anytype`, `panoply`) rather than from the usual issue flow, hence the `arena/` name and the absence of a linked issue. Only the two fixes above are in scope. Happy to re-cut against an issue, or to drop this and hand the diagnosis over as an issue instead. Worth recording that the gate itself worked exactly as designed: because `All.agda` and `Smoke.agda` were both wired to the new module, `main` went red the moment an unprovable lemma landed. That is the strongest argument for the existing methodology — the gap is in the repair loop, not the check. --- # Second fix: `main`'s CodeQL and Hypatia workflows never start (`6044971`) Investigating why this PR's checks came back `startup_failure` turned up a **separate, pre-existing breakage on `main`** — one that has nothing to do with this branch. ## Evidence On `main`, at commit `1f677531`, pushed by `hyperpolymath`, event `push`, same run batch: ``` 2026-09-27T01:55:43 Agda actor=hyperpolymath -> ran (conclusion: failure) 2026-09-27T01:55:44 CodeQL Security Analysis actor=hyperpolymath -> startup_failure 2026-09-27T01:55:45 Hypatia Security Scan actor=hyperpolymath -> startup_failure ``` Same actor, same commit, same event. The lockfile validation is therefore **per-workflow**, and exactly the two workflows whose lock entries are stale are the two that never start. The same pair has startup-failed on every event since 2026-09-26, including human pushes to `main`. ## Cause `cd9aa401` (dependabot, #326, 2026-09-26) changed `.github/workflows/codeql.yml` (+2 −2) and `.github/workflows/hypatia-scan.yml` (+1 −1), bumping `github/codeql-action` **4.38.0 → 4.38.1** — but did not regenerate `.github/workflows/actions.lock`, which still pinned 4.38.0 in three places. The lockfile no longer validates against the workflows, so the gate rejects the runs before any job is created. This is the same failure mode, and the same fix, as `9c4b72b5` — the last green `main` commit, whose message reads: *"Workflows fail at creation with `The lockfile could not be validated. Regenerate it by running gh actions-lock`"*. ## Fix Version strings only — 2 `workflows:` refs plus the `dependencies:` entry, resolved to 4.38.1. The `commit:` hash is the **peeled** tag commit, which is the convention the existing entry already follows: `v4.38.0^{} = b96794f0…` is byte-for-byte the hash previously recorded. `v4.38.1^{} = 1c5b6756…`, from `git ls-remote --tags https://github.com/github/codeql-action`. `owner_id`/`repo_id` are unchanged (same repository). The lock's existing habit of recording the repo-level ref while the workflows use sub-paths (`github/codeql-action@v4.38.1` vs `github/codeql-action/init@v4.38.1`) is preserved exactly. **Caveat:** regenerated by hand, not by `gh actions-lock` — the extension's release binary is unreachable from the environment this was prepared in. It is faithful to the tool's convention (checked against the pre-existing 4.38.0 entry), but a maintainer run of `gh actions-lock` should be preferred if anything looks off. Because the symptom is `startup_failure`, it cannot be tested locally — it is confirmed only by whether CodeQL/Hypatia next start. --- #⚠️ This PR's own checks did not run — they need a human trigger Every workflow on this branch came back `startup_failure`, including `Agda`. The reason is the **triggering actor**, not the content: ``` arena/01a0e040-echo-types actor=hyperpolymath -> Agda RAN arena/01a0e508-echo-types actor=arena-ai-coding-agent[bot] -> Agda startup_failure ``` Both are `pull_request` events on `arena/*` branches. When the trigger is the `arena-ai-coding-agent[bot]` App, no workflow is created at all. `gh run rerun` is refused with *"its workflow file may be broken"*. **To get CI to verify the Agda fix, close and reopen this PR as a human**, or push any commit to the branch. Everything below is unverified until that happens. --------- Co-authored-by: arena-agent <agent@arena.ai> Co-authored-by: arena-agent <297053741+arena-agent@users.noreply.github.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 1 update: github/codeql-action.
Updates
github/codeql-actionfrom 4.38.0 to 4.38.1Release notes
Sourced from github/codeql-action's releases.
Changelog
Sourced from github/codeql-action's changelog.
Commits
1c5b675Merge pull request #4152 from github/update-v4.38.1-a65b83a73a97cdcaAdd changelog entry for #4146cc6c691Update changelog for v4.38.1a65b83aMerge pull request #4146 from github/henrymercer/per-language-bundles-pr07fa87dClarify the latest-nightly eligibility exceptionf18f353Describe the bundle URL resolverecec9b5Share per-language telemetry fields without renaming79fe3a1Move download telemetry into the status-report directoryead1f7dRename the platform module549d498Simplify per-language platform eligibility checksDependabot 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