Repository navigation
ci: re-pin standards reusables to metadatastician@e064539 - #284
Conversation
The five standards reusables (governance, hypatia-scan, mirror, scorecard, secret-scanner) were pinned to hyperpolymath/standards at da2c748, where all five failed at startup on every push, so the required `scan / gitleaks` check never reported. Re-pin to metadatastician/standards@e064539, the commit panll runs green (hyperpolymath/panll#171). governance.yml and mirror.yml grant `actions: read`, which both reusables declare at workflow level at e064539. Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01Y6FD63UrriRBHqmhhEca9t
|
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 55 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. |
`secrets: inherit` hands every repository secret to the callee. The mirror reusable at e064539 declares seven forge keys, so pass those by name; the secret-scanner reusable declares none, so pass none. SonarCloud rated the re-pin's new code C for security on the inherited secrets. The secret-scanner comment now says what the reusable asks for at e064539 (contents: read only). Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01Y6FD63UrriRBHqmhhEca9t
|
|
This PR is blocked, and the change that unblocks it is a repository setting, not code. On both commits (a6bc805, b6857bb), Secret Scanner, Governance and Hypatia Security Scan end in
The likely cause: typed-wasm's Actions allowed-actions setting does not yet admit For context, Generated by Claude Code |
Codex Review Summary: ❌ FailedThis comment shows the latest Codex review activity on this pull request.
ℹ️ About Codex in GitHubYour team has set up Codex to review pull requests in this repo. Reviews are triggered when you
Codex reacts with 👀 while any review is running, comments if it has suggestions, and reacts with 👍 once all reviews finish with no findings. |
|
You have reached your Codex usage limits for code reviews. You can see your limits in the Codex usage dashboard. |
…285) ## Summary The kernel-proofs gate re-checks the sibling repositories' Agda proofs (resource-algebra, occupancy-types, choreographic-types' K-CUT slice) and checks the kernel transcription table. It ran them on Ubuntu 24.04's Agda 2.6.3. Each sibling pins Agda 2.6.4.3 in its own CI, so this gate checked their proofs on a different prover. The gate's own Agda checks also ran without `--cubical-compatible`, the canonical theory invocation in PROOF-POLICY §2.1 (`metadatastician/standards`, `3-practice/PROOF-POLICY.adoc`). ## Changes - **`.github/workflows/contract-gate.yml`** (`kernel-proofs` job): - Runs in `debian:trixie-slim` with `agda-bin=2.6.4.3-1+b2`, and asserts the version, as the siblings' `proofs.yml` do. - Idris2 0.8.0 is still built from source at its pinned commit. Debian names the Chez binary `chezscheme`, so the build uses whichever of `chezscheme` and `scheme` exists. - **`tools/check-kernel-proofs.sh`:** - Requires Agda 2.6.4.3 (the whole version line); `ALLOW_ANY_AGDA=1` still overrides. - Its own Agda checks (choreographic-types' KCut slice and rejects, the transcription table, the negative controls) run under `--safe --without-K --cubical-compatible`. - Sets `LC_ALL=C.UTF-8`. Without a UTF-8 locale, Agda stops with exit 42 on the Unicode warnings `--cubical-compatible` prints. - **`CHANGELOG.adoc`:** entry added. Not changed: the sibling pins. The siblings' own scripts run at those pins with their own flags. resource-algebra#19 and occupancy-types#18 move those scripts to the canonical flags. A later re-pin here picks them up, together with the stale `af95728` citations. ## RSR Quality Checklist ### Required - [x] Tests pass (see Testing) - [x] No banned language patterns - [x] No banned functions (`believe_me`, `unsafeCoerce`, `Obj.magic`, `Admitted`, `sorry`) - [x] SPDX license headers present on all new/modified source files - [x] No secrets, credentials, or `.env` files included ### As Applicable - [x] `CHANGELOG` updated ## Testing This environment cannot reach the Debian archive or Docker Hub, so it has no Agda 2.6.4.3. What I could check locally: - **Under the new flags on 2.6.3:** `ALLOW_ANY_AGDA=1 bash tools/check-kernel-proofs.sh` gives `OK: kernel proofs — build, 13 rejection(s), table, and 4 negative control row(s)`. - **Version guard:** without the override, the gate refuses 2.6.3: `FAIL: Agda 2.6.4.3 required ...`. - **`yq`** parses the workflow. The run that counts is this PR's `Grade kernel proofs (Idris2 0.8.0 + Agda)` job, which is the first run on 2.6.4.3. CI note: `scan / gitleaks` and the governance, Hypatia and mirror workflows fail on main too, until #284 lands. --- _Generated by [Claude Code](https://claude.ai/code/session_01Y6FD63UrriRBHqmhhEca9t)_ Signed-off-by: Jonathan D.A. Jewell <6759885+hyperpolymath@users.noreply.github.com> Co-authored-by: Claude <noreply@anthropic.com>
Summary
typed-wasm's five standards workflows call reusable workflows pinned to
hyperpolymath/standards@da2c748. At that pin all five fail at startup on every push, before any job runs. So the requiredscan / gitleakscheck never reports, and governance, Hypatia, mirror and Scorecard are red onmain.This PR re-pins them to
metadatastician/standards@e064539, the commit panll already runs green (hyperpolymath/panll#171).Changes
governance,hypatia-scan,mirror,scorecardandsecret-scannermove fromhyperpolymath/standards@da2c748tometadatastician/standards@e064539. GitHub redirects the old org name; PROOF-POLICY §8.6 confirms both names are the same repository.governance.ymlandmirror.ymlnow grantactions: read, which both reusables declare at workflow level ate064539.workflow_callinterface at both pins. The new inputs are all optional, and no job asks for a permission its caller does not grant. Scorecard and Hypatia already granted what they need. secret-scanner's job needs onlycontents: read.CHANGELOG.adocgets an entry.Not changed: triggers and secrets handling stay as they were (Hypatia still runs on
pull_request, mirror still usessecrets: inherit).RSR Quality Checklist
Required
believe_me,unsafeCoerce,Obj.magic,Admitted,sorry).envfiles includedAs Applicable
CHANGELOGupdatedTesting
yqparses all five edited workflows.scan / gitleaksshould now report.Generated by Claude Code