ci(AGLib): refresh workflow actions for Node 24

[AxelDlv00]

Contributor : contributor 🧑‍💻 🚫

Profile: contributor (contributor)
GitHub account: @AxelDlv00
Engine: codex
Model: gpt-5.6-sol
Effort: ultra

🔧 Scope

This is a focused CI follow-up for issue #1. The accepted bootstrap workflow
still pinned actions/checkout and actions/cache revisions whose action
definitions use the Node 20 runtime. The exact-head review of the bootstrap
recorded that deprecation as a non-blocking caveat and requested a focused pin
refresh.

The workflow now uses the released Node 24 revisions:

• actions/checkout v5.1.0 at fbc6f3992d24b796d5a048ff273f7fcc4a7b6c09
• actions/cache v5.1.0 at caa296126883cff596d87d8935842f9db880ef25

The palimpsest/aglib push and pull-request triggers, lake-build job,
manifest-keyed dependency cache, rotating build cache, uncached fallback, and
protected-branch-only cache saves are unchanged. No Lean declarations, package
pins, or source imports are changed.

Part of #1

🧪 Validation

• Re-fetched origin immediately before publication; protected head was
  24993eb0fedf22b3d0aef510e28920c11c956cfa.
• Parsed .github/workflows/lean-ci.yml as YAML and checked its triggers, job,
  action pins, cache conditions, and protected save guards.
• Confirmed both action SHAs resolve to their public release tags and their
  action.yml files declare node24.
• Confirmed the direct protected-to-head diff contains only this workflow file;
  git diff --check is clean and the non-workflow tree is unchanged.
• No local lake build, lake update, or cache download was run; protected CI
  remains the authoritative full-package check.

📚 References

• actions/checkout v5 runtime notes
• actions/cache v5 runtime notes
• GitHub Node 20 deprecation timeline
• Prior bootstrap review caveat

[AxelDlv00]

Reviewer : mathematical-correctness 📐 ✅

Profile: mathematical-correctness (reviewer)
GitHub account: @AxelDlv00
Engine: codex
Model: gpt-5.6-sol
Effort: ultra
Decision: approved ✅
Head: 619b330

🔍 Coverage

Reviewed pull 5 at exact head 619b3307851238820a184bb92c6e8038be6b624a against base 24993eb0fedf22b3d0aef510e28920c11c956cfa, using issue 1's CI acceptance criteria, the PR record, and the complete changes.diff. The patch changes only .github/workflows/lean-ci.yml: one checkout pin and the four cache restore/save pins. It adds no Lean declaration, proof, hypothesis, import, package pin, or mathematical claim.

✅ Verified

• The required push and pull_request filters for palimpsest/aglib remain at lines 5–9, and the lake-build job still runs lake build AGLib from AGLib/ at lines 92–95. The Lean toolchain action and all build commands are unchanged, so the candidate mathematical content being checked is unchanged.
• The dependency and build cache paths, manifest/toolchain fingerprint, weekly key, restore prefix, cache-hit conditions, and protected-branch-only save guards at lines 38–117 are unchanged. Replacing the action references therefore does not alter which artifacts can affect the build or when they can be published.
• actions/checkout SHA fbc6f3992d24b796d5a048ff273f7fcc4a7b6c09 and actions/cache SHA caa296126883cff596d87d8935842f9db880ef25 resolve to their v5.1.0 tags. Their action.yml files retain the existing entry points and inputs; the manifest change is only the Node runtime (node20 to node24).
• The immutable diff contains no non-workflow changes. There are consequently no statements, degenerate cases, hidden hypotheses, or proof directions whose mathematical truth could have changed in this head.

🧪 Validation

• Confirmed review.json's head equals PALIMPSEST_EXPECTED_HEAD; the forge record reports pull 5 at the same head and no existing PR comments.
• Checked the exact base/head diff and found only the five intended uses: substitutions; a recursive comparison excluding the workflow was empty.
• Independently checked both release tags with git ls-remote and inspected old/new action.yml manifests. No local Lake build or cache download was run, in accordance with the review-context policy; protected CI remains the authoritative build evidence.
• A mathlib pull-request precedent search was not warranted: this is a workflow-only maintenance patch with no Lean API or mathematical design change.

💬 Decision

Approve for mathematical correctness. The exact head leaves AGLib's mathematical content and the semantics of its build validation unchanged.

[AxelDlv00]

Reviewer : maths-lean-correspondence 🌉 ✅

Profile: maths-lean-correspondence (reviewer)
GitHub account: @AxelDlv00
Engine: codex
Model: gpt-5.6-sol
Effort: ultra
Decision: approved ✅
Head: 619b330

🔍 Coverage

I reviewed pull request #5 at exact head 619b3307851238820a184bb92c6e8038be6b624a against base 24993eb0fedf22b3d0aef510e28920c11c956cfa, within the maths–Lean correspondence dimension. Issue #1 calls for the protected-branch Lean CI workflow; this follow-up's exact patch contains only .github/workflows/lean-ci.yml. The changed positions are the checkout pin at line 25 and the four cache restore/save pins at lines 69, 77, 103, and 114.

There are no changed Lean declarations or logically significant Lean helpers to inventory. The unchanged public entry points (AGLib/AGLib.lean and AGLib/AGLib/Basic.lean) retain their existing imports and bootstrap documentation, so the mathematical API surface is unchanged.

✅ Verified

• actions/checkout@fbc6f3992d24b796d5a048ff273f7fcc4a7b6c09 is the v5.1.0 release. Its upstream manifest declares runs: using: node24; the workflow's fetch depth, credential policy, and checkout role are unchanged.
• All four cache references use caa296126883cff596d87d8935842f9db880ef25, the v5.1.0 release. The upstream restore and save manifests both declare the Node 24 runtime. Paths, keys, restore prefixes, cache-hit conditions, and protected-branch-only save guards are unchanged.
• The workflow still targets pushes and pull requests for palimpsest/aglib (lines 5–9), installs the same pinned Lean action (line 31), and runs lake build AGLib in the same package directory (lines 92–95). Updating action runtimes therefore cannot strengthen, weaken, reverse, or make vacuous any Lean proposition.
• No changed prose is a declaration docstring or mathematical claim. There are no new typeclass assumptions, coercions, definition references, imports, or proof mechanisms whose interpretation needs correspondence review.

🧪 Validation

• Parsed both base and head workflow files as YAML and checked that the triggers, job set, Lean-action pin, build command, cache paths, and save predicates are preserved.
• Confirmed the exact diff has one changed file and only the stated action-SHA substitutions; pin occurrence counts are one checkout and four cache references on each side, with no trailing-whitespace errors.
• The controller log reports the protected lake-build status as still pending (waiting-on-ci); I did not claim a green build. This read-only review did not run Lake or LSP, consistent with the job policy.
• A mathlib PR precedent search is not applicable here: this is routine CI maintenance with no Lean API, naming, statement, or proof-design choice under review.

📚 References

The release identity and runtime claims were checked against the upstream checkout v5.1.0 release, checkout action manifest, cache v5.1.0 release, and the cache restore and save manifests.

💬 Decision

Approve. At this exact head I found no maths–Lean correspondence issue; the Lean statements and their imports are untouched. The pending protected CI result remains the repository's independent acceptance gate.

[AxelDlv00]

Reviewer : lean-quality 🧪 ✅

Profile: lean-quality (reviewer)
GitHub account: @AxelDlv00
Engine: codex
Model: gpt-5.6-sol
Effort: ultra
Decision: approved ✅
Head: 619b330

🔍 Coverage

I reviewed pull #5 at exact head 619b3307851238820a184bb92c6e8038be6b624a against base 24993eb0fedf22b3d0aef510e28920c11c956cfa, using the bootstrap issue, the repository roadmap, the PR record, and the immutable changes.diff. The change is one focused CI follow-up: .github/workflows/lean-ci.yml only, with substitutions at lines 25, 69, 77, 103, and 114. There are no changed Lean declarations, imports, package pins, docstrings, proofs, or logically significant helpers to inventory.

✅ Verified

• The checkout reference at .github/workflows/lean-ci.yml:25 changes from the old Node 20 action revision to actions/checkout v5.1.0 at fbc6f3992d24b796d5a048ff273f7fcc4a7b6c09. The pinned manifest keeps the same entry points and inputs; fetch-depth: 1 and persist-credentials: false are unchanged. The new manifest uses node24.
• The two restore references and two save references at lines 69, 77, 103, and 114 consistently change to actions/cache v5.1.0 at caa296126883cff596d87d8935842f9db880ef25. The root, restore, and save manifests retain the same paths, entry points, inputs, and cache-hit output shape; their only manifest change is node20 to node24. No old SHA remains and no mixed cache versions were introduced.
• The workflow contract is preserved: push and pull_request still target palimpsest/aglib; the lake-build job still runs lake build AGLib in AGLib/; the manifest/toolchain fingerprint and weekly build key are unchanged; cache restore remains conditional on endpoint availability; and both save steps remain restricted to protected-branch pushes and cache misses. Pull requests therefore still cannot publish either cache.
• I also checked the unchanged leanprover/lean-action reference. Its pinned manifest is a composite action, so it does not leave a hidden Node 20 action runtime behind this refresh.
• The v5 actions require runner version 2.327.1 or newer. This workflow selects GitHub-hosted ubuntu-latest, and the exact-head run successfully executed checkout, toolchain installation, and the build. The new checkout behavior around unsafe target checkouts is irrelevant here because the workflow uses pull_request, not pull_request_target, and supplies no unsafe-checkout input.

🧪 Validation

• Parsed the base, head, and source workflow files as YAML. Their triggers and job set are identical, with one checkout reference and two restore plus two save references on each side.
• Normalizing the two old SHAs in the base file to the two new SHAs produces the head file byte-for-byte. git diff --check is clean, and the base/head file inventories and all non-workflow content match.
• Independently resolved both new SHAs with git ls-remote and inspected the exact upstream manifests. The exact-head lake-build status is successful in 2 minutes. That run reports the cache restore/save steps skipped because no Actions cache endpoint was available, followed by a successful uncached artifact download and Build AGLib; cache-action execution is therefore supported by the manifest checks rather than claimed from that run.
• I did not run Lake, LSP, or cache downloads in this immutable reviewer context. This is workflow-only maintenance, so no changed-file Lean timing or mathlib pull-request precedent search is applicable.

📚 References consulted

• actions/checkout v5.1.0 release and the pinned checkout manifest.
• actions/cache v5.1.0 release, the pinned restore manifest, and the pinned save manifest.
• The prior bootstrap review caveat, which requested this focused Node 24 pin refresh while preserving the bounded cache policy.

💬 Decision

Approve for lean quality. The exact head is a coherent, pinned workflow maintenance change with no library-code quality debt or altered CI/cache contract. The separate Palimpsest review-panel status remains pending until the full reviewer panel responds; the required lake-build check itself is green for this head.

[AxelDlv00]

Reviewer : architecture 🏗️ ✅

Profile: architecture (architecture)
GitHub account: @AxelDlv00
Engine: codex
Model: gpt-5.6-sol
Effort: ultra
Decision: approved ✅
Head: 619b330

🔍 Coverage

I reviewed issue #1's CI follow-up at exact head 619b3307851238820a184bb92c6e8038be6b624a against base 24993eb0fedf22b3d0aef510e28920c11c956cfa. The change inventory is one repository-owned file, .github/workflows/lean-ci.yml, with exactly five action-reference substitutions (checkout once, cache restore twice, and cache save twice). There are no Lean declarations, package pins, imports, roadmap nodes, or public APIs in this patch.

The architectural claim to check is therefore narrow: refresh the action runtimes while preserving issue #1's lake-build merge gate, bounded cache topology, and protected-branch publication boundary.

✅ Verified

• The roadmap keeps infrastructure maintenance separate from mathematical API work (AGLib/ROADMAP.md:79-88). This PR honors that boundary and leaves the Foundations-to-Universal-Constructions dependency route, downward-only imports, and the public surface unchanged.
• actions/checkout resolves to the v5.1.0 release commit fbc6f3992d24b796d5a048ff273f7fcc4a7b6c09; its v5.1.0 manifest uses node24 and retains the inputs used here (fetch-depth and persist-credentials). The release's unsafe-PR-checkout default concerns pull_request_target/workflow_run; this workflow uses pull_request and still disables credential persistence, so the trust boundary is unchanged.
• actions/cache resolves to v5.1.0 commit caa296126883cff596d87d8935842f9db880ef25. The restore manifest uses node24 and retains its cache-hit output plus path/key/restore-key inputs; the save manifest uses node24 and retains its path/key inputs. They are applied to the same two restore and two protected save steps.
• A base/head structural comparison found only those five uses changes. Branch filters, the lake-build job/check name, ubuntu-latest runner, Lean action and its cache-disable settings, manifest-derived keys, uncached fallback, build command, and exact protected-ref/cache-miss guards are byte-for-byte unchanged. In particular, use-github-cache: false means the Lean action's optional nested GitHub cache path is not active here.
• The resulting workflow still has one authoritative build path for cache hits, cache misses, and absent cache endpoints. Updating action implementations does not alter AGLib's Lean dependency graph or foreclose a canonical future API route.

🧪 Validation

• review.json, the forge pull record, and the latest pull metadata agree on the expected head and base; the pull remains open. The current pull comments include three independent approvals already recorded for the other review dimensions.
• git ls-remote matched both new immutable SHAs to their stated v5.1.0 release tags, and the upstream action.yml files were inspected directly. YAML structure and substitution counts were checked, and git diff --check is clean.
• The live exact-head lake-build job is successful. It reports the cache restore/save steps skipped because no Actions cache endpoint was available, then completes the uncached artifact download and Build AGLib; an earlier controller poll said pending, so I use this newer job result. I did not run lake build, lake update, cache downloads, or LSP in this read-only review.
• No mathlib pull-request precedent search was needed: this maintenance diff introduces no Lean API, naming, import, theorem, or proof-architecture choice.

📚 References

• AGLib roadmap
• actions/checkout v5.1.0 release and pinned checkout manifest
• actions/cache v5.1.0 release, pinned restore manifest, and pinned save manifest

💬 Decision

✅ Approve for the architecture dimension at this exact head. The patch is a coherent, isolated infrastructure update that advances the repository's CI maintenance without changing the roadmap route or public library architecture. The protected lake-build check is green for this head; the remaining panel labels and maintainer merge decision are separate workflow gates.

[AxelDlv00]

Maintainer : maintainer-adviser 🧭 ✅

Profile: maintainer-adviser (maintainer,contributor)
GitHub account: @AxelDlv00
Engine: codex
Model: gpt-5.6-sol
Effort: ultra
Head: 619b330

✅ Merge result

PR #5 was squash-merged into palimpsest/aglib from the reviewed head
619b3307851238820a184bb92c6e8038be6b624a, producing merge commit
d2f81c65c5a7aa92982991994a00a4fc8f65edf6.

🧪 Gate validation

• The required exact-head lake-build status passed.
• Current-head approvals are recorded for mathematical correctness,
  maths–Lean correspondence, Lean quality, and architecture.
• The accepted diff remains limited to the Node 24 action-pin refresh in
  .github/workflows/lean-ci.yml; no Lean declarations or package sources
  changed.

💬 Issue routing

Issue #1 remains open because this PR is marked Part of #1; the repository
workflow returns a merged focused increment to the contributor queue for the
next roadmap pull request.