Repository navigation
ci(agda): typecheck the experimental echo-additive tree standalone - #343
Merged
Merged
Conversation
Adds a lane (warm and cold) that typechecks every module under proofs/agda/experimental/echo-additive/ on its own. Nothing is added to All.agda or Smoke.agda, so the shipped closure and its claims are unchanged (D-2026-06-14-R1 firewall; R-2026-05-18 stands). A consumer that vendors Grade.agda (choreographic-types) now learns here when an edit breaks it. Verified locally under Agda 2.6.3 / stdlib v2.3 / absolute-zero f486c29: all seven modules exit 0; check-guardrails.sh passes. Co-Authored-By: Claude Sonnet 5.5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01MF5GeeBBDF6sUzr6pZTjWV
🔍 Hypatia Security ScanFindings: 52 issues detected
View findings[
{
"reason": "Required file missing",
"type": "missing",
"file": "0-AI-MANIFEST.a2ml",
"level": "epi",
"action": "create",
"rule_module": "root_hygiene",
"severity": "high",
"evidence": [
{
"span": {
"file": "0-AI-MANIFEST.a2ml",
"end_line": 0,
"start_line": 0
},
"rule": "root_hygiene/missing",
"observations": 1,
"rule_version": "0.1.0"
}
],
"support": {
"kind": "pattern"
}
},
{
"reason": "Invalid .github/workflows/actions.lock: {:line, 4, {:unsupported_version, \"v0.0.3\"}}. Regenerate and verify it with gh actions-lock.",
"type": "invalid_actions_lock",
"file": ".github/workflows/actions.lock",
"level": "epi",
"action": "regenerate",
"rule_module": "workflow_audit",
"severity": "high",
"evidence": [
{
"span": {
"file": ".github/workflows/actions.lock",
"end_line": 0,
"start_line": 0
},
"rule": "workflow_audit/invalid_actions_lock",
"observations": 1,
"rule_version": "0.1.0"
}
],
"support": {
"kind": "pattern"
}
},
{
"reason": "Job `triage` in label-triage.yml has no `timeout-minutes:` declaration. Default is 6 hours — a stuck codeload fetch or runner hang can burn budget. Add `timeout-minutes: 10` (or proportional).",
"type": "missing_timeout_minutes",
"file": ".github/workflows/label-triage.yml",
"level": "epi",
"action": "flag",
"rule_module": "workflow_audit",
"severity": "medium",
"recipe_id": "recipe-add-workflow-timeout-minutes",
"job": "triage",
"evidence": [
{
"span": {
"file": ".github/workflows/label-triage.yml",
"end_line": 0,
"start_line": 0
},
"rule": "workflow_audit/missing_timeout_minutes",
"observations": 1,
"rule_version": "0.1.0"
}
],
"support": {
"kind": "pattern"
}
},
{
"reason": "Job `sync` in labels.yml has no `timeout-minutes:` declaration. Default is 6 hours — a stuck codeload fetch or runner hang can burn budget. Add `timeout-minutes: 10` (or proportional).",
"type": "missing_timeout_minutes",
"file": ".github/workflows/labels.yml",
"level": "epi",
"action": "flag",
"rule_module": "workflow_audit",
"severity": "medium",
"recipe_id": "recipe-add-workflow-timeout-minutes",
"job": "sync",
"evidence": [
{
"span": {
"file": ".github/workflows/labels.yml",
"end_line": 0,
"start_line": 0
},
"rule": "workflow_audit/missing_timeout_minutes",
"observations": 1,
"rule_version": "0.1.0"
}
],
"support": {
"kind": "pattern"
}
},
{
"line": 39,
"reason": "job in .github/workflows/labels.yml references `secrets.*` but does not install `step-security/harden-runner` — review outbound-egress monitoring",
"type": "RE001",
"file": ".github/workflows/labels.yml",
"level": "epi",
"action": "report",
"rule_module": "research_extensions",
"severity": "medium",
"evidence": [
{
"span": {
"file": ".github/workflows/labels.yml",
"end_line": 39,
"start_line": 39
},
"rule": "research_extensions/RE001",
"observations": 1,
"rule_version": "0.1.0"
}
],
"support": {
"kind": "pattern"
}
},
{
"line": 53,
"reason": "job in .github/workflows/label-triage.yml references `secrets.*` but does not install `step-security/harden-runner` — review outbound-egress monitoring",
"type": "RE001",
"file": ".github/workflows/label-triage.yml",
"level": "epi",
"action": "report",
"rule_module": "research_extensions",
"severity": "medium",
"evidence": [
{
"span": {
"file": ".github/workflows/label-triage.yml",
"end_line": 53,
"start_line": 53
},
"rule": "research_extensions/RE001",
"observations": 1,
"rule_version": "0.1.0"
}
],
"support": {
"kind": "pattern"
}
},
{
"line": 87,
"reason": "job in .github/workflows/hypatia-scan.yml references `secrets.*` but does not install `step-security/harden-runner` — review outbound-egress monitoring",
"type": "RE001",
"file": ".github/workflows/hypatia-scan.yml",
"level": "epi",
"action": "report",
"rule_module": "research_extensions",
"severity": "medium",
"evidence": [
{
"span": {
"file": ".github/workflows/hypatia-scan.yml",
"end_line": 87,
"start_line": 87
},
"rule": "research_extensions/RE001",
"observations": 1,
"rule_version": "0.1.0"
}
],
"support": {
"kind": "pattern"
}
},
{
"line": 46,
"reason": "job in .github/workflows/push-email-notify.yml references `secrets.*` but does not install `step-security/harden-runner` — review outbound-egress monitoring",
"type": "RE001",
"file": ".github/workflows/push-email-notify.yml",
"level": "epi",
"action": "report",
"rule_module": "research_extensions",
"severity": "medium",
"evidence": [
{
"span": {
"file": ".github/workflows/push-email-notify.yml",
"end_line": 46,
"start_line": 46
},
"rule": "research_extensions/RE001",
"observations": 1,
"rule_version": "0.1.0"
}
],
"support": {
"kind": "pattern"
}
},
{
"line": null,
"reason": "actions.lock failed closed: {:line, 4, {:unsupported_version, \"v0.0.3\"}}",
"type": "invalid_actions_lock",
"file": ".github/workflows/actions.lock",
"level": "epi",
"action": "regenerate",
"rule_module": "workflow_hardening",
"severity": "high",
"evidence": [
{
"span": {
"file": ".github/workflows/actions.lock",
"end_line": 0,
"start_line": 0
},
"rule": "workflow_hardening/invalid_actions_lock",
"observations": 1,
"rule_version": "0.1.0"
}
],
"support": {
"kind": "pattern"
}
},
{
"line": 34,
"reason": "workflow .github/workflows/labels.yml:34 job `sync` has no `timeout-minutes:` — defaults to 360 min on hang",
"type": "WH006",
"file": ".github/workflows/labels.yml",
"level": "epi",
"action": "report",
"rule_module": "workflow_hardening",
"severity": "medium",
"evidence": [
{
"span": {
"file": ".github/workflows/labels.yml",
"end_line": 34,
"start_line": 34
},
"rule": "workflow_hardening/WH006",
"observations": 1,
"rule_version": "0.1.0"
}
],
"support": {
"kind": "pattern"
}
}
]Powered by Hypatia Neurosymbolic CI/CD Intelligence |
hyperpolymath
marked this pull request as ready for review
October 19, 2026 17:05
Owner
Author
|
Two kinds of red here, neither caused by this diff (it only adds a loop to
I have not widened this PR to fix either. Neither exists as a PR yet; I can open them as separate PRs if wanted. Generated by Claude Code |
Codex Review SummaryThis 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. |
![chatgpt-codex-connector[bot]](https://avatars.githubusercontent.com/in/1144995?s=60&v=4){kind=small}
There was a problem hiding this comment.
💡 Codex Review
Here are some automated review suggestions for this pull request.
Reviewed commit: 5d91cdf2b4
ℹ️ About Codex in GitHub
Your team has set up Codex to review pull requests in this repo. Reviews are triggered when you
- Open a pull request for review
- Mark a draft as ready
- Comment "@codex review".
If Codex has suggestions, it will comment; otherwise it will react with 👍.
Codex can also answer questions or update the PR. Try commenting "@codex address that feedback".
Codex review on #343: the cold lane started a fresh Agda process per module with --ignore-interfaces, rebuilding the standard library seven times inside the job's 30-minute cap. proofs/agda/experimental/echo-additive/All.agda imports the seven modules; both the warm and cold steps now check that one root. Cold, locally: exit 0 in 95 s. Not imported by the shipped All.agda or Smoke.agda. Co-Authored-By: Claude Sonnet 5.5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01MF5GeeBBDF6sUzr6pZTjWV
|
You have reached your Codex usage limits for code reviews. You can see your limits in the Codex usage dashboard. |
🔍 Hypatia Security ScanFindings: 52 issues detected
View findings[
{
"reason": "Required file missing",
"type": "missing",
"file": "0-AI-MANIFEST.a2ml",
"level": "epi",
"action": "create",
"rule_module": "root_hygiene",
"severity": "high",
"evidence": [
{
"span": {
"file": "0-AI-MANIFEST.a2ml",
"end_line": 0,
"start_line": 0
},
"rule": "root_hygiene/missing",
"observations": 1,
"rule_version": "0.1.0"
}
],
"support": {
"kind": "pattern"
}
},
{
"reason": "Invalid .github/workflows/actions.lock: {:line, 4, {:unsupported_version, \"v0.0.3\"}}. Regenerate and verify it with gh actions-lock.",
"type": "invalid_actions_lock",
"file": ".github/workflows/actions.lock",
"level": "epi",
"action": "regenerate",
"rule_module": "workflow_audit",
"severity": "high",
"evidence": [
{
"span": {
"file": ".github/workflows/actions.lock",
"end_line": 0,
"start_line": 0
},
"rule": "workflow_audit/invalid_actions_lock",
"observations": 1,
"rule_version": "0.1.0"
}
],
"support": {
"kind": "pattern"
}
},
{
"reason": "Job `triage` in label-triage.yml has no `timeout-minutes:` declaration. Default is 6 hours — a stuck codeload fetch or runner hang can burn budget. Add `timeout-minutes: 10` (or proportional).",
"type": "missing_timeout_minutes",
"file": ".github/workflows/label-triage.yml",
"level": "epi",
"action": "flag",
"rule_module": "workflow_audit",
"severity": "medium",
"recipe_id": "recipe-add-workflow-timeout-minutes",
"job": "triage",
"evidence": [
{
"span": {
"file": ".github/workflows/label-triage.yml",
"end_line": 0,
"start_line": 0
},
"rule": "workflow_audit/missing_timeout_minutes",
"observations": 1,
"rule_version": "0.1.0"
}
],
"support": {
"kind": "pattern"
}
},
{
"reason": "Job `sync` in labels.yml has no `timeout-minutes:` declaration. Default is 6 hours — a stuck codeload fetch or runner hang can burn budget. Add `timeout-minutes: 10` (or proportional).",
"type": "missing_timeout_minutes",
"file": ".github/workflows/labels.yml",
"level": "epi",
"action": "flag",
"rule_module": "workflow_audit",
"severity": "medium",
"recipe_id": "recipe-add-workflow-timeout-minutes",
"job": "sync",
"evidence": [
{
"span": {
"file": ".github/workflows/labels.yml",
"end_line": 0,
"start_line": 0
},
"rule": "workflow_audit/missing_timeout_minutes",
"observations": 1,
"rule_version": "0.1.0"
}
],
"support": {
"kind": "pattern"
}
},
{
"line": 39,
"reason": "job in .github/workflows/labels.yml references `secrets.*` but does not install `step-security/harden-runner` — review outbound-egress monitoring",
"type": "RE001",
"file": ".github/workflows/labels.yml",
"level": "epi",
"action": "report",
"rule_module": "research_extensions",
"severity": "medium",
"evidence": [
{
"span": {
"file": ".github/workflows/labels.yml",
"end_line": 39,
"start_line": 39
},
"rule": "research_extensions/RE001",
"observations": 1,
"rule_version": "0.1.0"
}
],
"support": {
"kind": "pattern"
}
},
{
"line": 53,
"reason": "job in .github/workflows/label-triage.yml references `secrets.*` but does not install `step-security/harden-runner` — review outbound-egress monitoring",
"type": "RE001",
"file": ".github/workflows/label-triage.yml",
"level": "epi",
"action": "report",
"rule_module": "research_extensions",
"severity": "medium",
"evidence": [
{
"span": {
"file": ".github/workflows/label-triage.yml",
"end_line": 53,
"start_line": 53
},
"rule": "research_extensions/RE001",
"observations": 1,
"rule_version": "0.1.0"
}
],
"support": {
"kind": "pattern"
}
},
{
"line": 87,
"reason": "job in .github/workflows/hypatia-scan.yml references `secrets.*` but does not install `step-security/harden-runner` — review outbound-egress monitoring",
"type": "RE001",
"file": ".github/workflows/hypatia-scan.yml",
"level": "epi",
"action": "report",
"rule_module": "research_extensions",
"severity": "medium",
"evidence": [
{
"span": {
"file": ".github/workflows/hypatia-scan.yml",
"end_line": 87,
"start_line": 87
},
"rule": "research_extensions/RE001",
"observations": 1,
"rule_version": "0.1.0"
}
],
"support": {
"kind": "pattern"
}
},
{
"line": 46,
"reason": "job in .github/workflows/push-email-notify.yml references `secrets.*` but does not install `step-security/harden-runner` — review outbound-egress monitoring",
"type": "RE001",
"file": ".github/workflows/push-email-notify.yml",
"level": "epi",
"action": "report",
"rule_module": "research_extensions",
"severity": "medium",
"evidence": [
{
"span": {
"file": ".github/workflows/push-email-notify.yml",
"end_line": 46,
"start_line": 46
},
"rule": "research_extensions/RE001",
"observations": 1,
"rule_version": "0.1.0"
}
],
"support": {
"kind": "pattern"
}
},
{
"line": null,
"reason": "actions.lock failed closed: {:line, 4, {:unsupported_version, \"v0.0.3\"}}",
"type": "invalid_actions_lock",
"file": ".github/workflows/actions.lock",
"level": "epi",
"action": "regenerate",
"rule_module": "workflow_hardening",
"severity": "high",
"evidence": [
{
"span": {
"file": ".github/workflows/actions.lock",
"end_line": 0,
"start_line": 0
},
"rule": "workflow_hardening/invalid_actions_lock",
"observations": 1,
"rule_version": "0.1.0"
}
],
"support": {
"kind": "pattern"
}
},
{
"line": 34,
"reason": "workflow .github/workflows/labels.yml:34 job `sync` has no `timeout-minutes:` — defaults to 360 min on hang",
"type": "WH006",
"file": ".github/workflows/labels.yml",
"level": "epi",
"action": "report",
"rule_module": "workflow_hardening",
"severity": "medium",
"evidence": [
{
"span": {
"file": ".github/workflows/labels.yml",
"end_line": 34,
"start_line": 34
},
"rule": "workflow_hardening/WH006",
"observations": 1,
"rule_version": "0.1.0"
}
],
"support": {
"kind": "pattern"
}
}
]Powered by Hypatia Neurosymbolic CI/CD Intelligence |
Contributor
|
Important Review skippedReview was skipped as selected files did not have any reviewable changes. ⚙️ Run configuration
You can disable this status message by setting the Use the checkbox below for a quick retry:
No actionable comments were generated in the recent review. 🎉 ℹ️ Recent review info
📜 Recent review details
📝 Summary
Merge Risk: 🟡 Moderate · up to
|
| Check name | Status | Explanation |
|---|---|---|
| Title check |  |
The title clearly and concisely describes the main change: adding standalone CI type-checking for the experimental echo-additive Agda tree. |
| Description check | |
The description directly explains the CI changes, scope, authorisation gate, validation, and known unrelated failures. |
| Docstring Coverage | |
No functions found in the changed files to evaluate docstring coverage. Skipping docstring coverage check. Docstring coverage is scoped to functions touched by this diff. Analyzed 0 functions across 0… |
| Linked Issues check | |
Check skipped because no linked issues were found for this pull request. |
| Out of Scope Changes check | |
Check skipped because no linked issues were found for this pull request. |
Full details: Docstring Coverage
-
Explanation
No functions found in the changed files to evaluate docstring coverage. Skipping docstring coverage check. Docstring coverage is scoped to functions touched by this diff. Analyzed 0 functions across 0 files. (2 skipped: 2 unsupported.)
- Autofix · Keep fixing CodeRabbit findings and required CI, and resolving merge conflicts
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 @coderabbitai help to get the list of available commands.
hyperpolymath
enabled auto-merge (squash)
October 19, 2026 17:24
![coderabbitai[bot]](https://avatars.githubusercontent.com/in/347564?s=60&v=4){kind=small}
Contributor
|
Add Carrot credits or activate Agent usage billing to use Autofix |
Owner
Author
|
@coderabbitai please do not attempt CI fixes, autofix, or edits to Two checks are red, neither caused by this PR: Review comments are welcome; automated pushes and "fix CI" suggestions are not. Generated by Claude Code |
Contributor
|
Tip For best results, initiate chat on the files or code changes. @hyperpolymath Thanks for the guidance. The failure attribution was incorrect: the failures you describe are pre-existing, not caused by this PR. I will keep my involvement on this PR to review comments. I will not trigger CI fixes, autofix, automated pushes, or edits to ✏️ Learnings added
You are interacting with an AI system. |
hyperpolymath
added a commit
that referenced
this pull request
Oct 19, 2026
#344) ## Summary GitHub's lock enforcement refuses a record for a tagged action whose `ref` repeats the SHA, in the called repository's lock at the pinned commit. The standards pins here (`fad242d`, `84355587`) fail that check, so `governance`, `secret-scanner`, `scorecard` and `mirror` startup-fail with no jobs. Standards `75bd5994` records tags in its own lock. Same fix as choreographic-types #34. ## Changes - Repin the four standards callers to `75bd5994470661a099df562d6d5ad2fe744dbd66`. - Record the standards edge in `actions.lock` (one `dependencies:` record with the matching `uses:` list, plus the actions it reaches at their release tags, copied from standards' own lock at that commit). Before, these four workflows had empty lock entries. - Bring the `smtp-notify-action` record to v0.5.0 (commit `c1c9fa07`, the peeled tag), which `push-email-notify.yml` already uses; the lock still said v0.3.0. ## Testing `check-lock-sync.sh` and `check-action-pinning.js` from affinescript-libraries, run here: lock in sync, transitively closed, all refs pinned. On main the same sync check reports the three missing/stale records above. The real test is those four jobs creating jobs on this PR; I have not seen that yet. Not touched: the `check` job failure on #343 (unclassified `EchoFidelity` kernel-guard module) is separate. --- _Generated by [Claude Code](https://claude.ai/code/session_01MF5GeeBBDF6sUzr6pZTjWV)_ Co-authored-by: Claude <noreply@anthropic.com>
hyperpolymath
disabled auto-merge
October 19, 2026 19:01
|
You have reached your Codex usage limits for code reviews. You can see your limits in the Codex usage dashboard. |
🔍 Hypatia Security ScanFindings: 52 issues detected
View findings[
{
"reason": "Required file missing",
"type": "missing",
"file": "0-AI-MANIFEST.a2ml",
"level": "epi",
"action": "create",
"rule_module": "root_hygiene",
"severity": "high",
"evidence": [
{
"span": {
"file": "0-AI-MANIFEST.a2ml",
"end_line": 0,
"start_line": 0
},
"rule": "root_hygiene/missing",
"observations": 1,
"rule_version": "0.1.0"
}
],
"support": {
"kind": "pattern"
}
},
{
"reason": "Invalid .github/workflows/actions.lock: {:line, 4, {:unsupported_version, \"v0.0.3\"}}. Regenerate and verify it with gh actions-lock.",
"type": "invalid_actions_lock",
"file": ".github/workflows/actions.lock",
"level": "epi",
"action": "regenerate",
"rule_module": "workflow_audit",
"severity": "high",
"evidence": [
{
"span": {
"file": ".github/workflows/actions.lock",
"end_line": 0,
"start_line": 0
},
"rule": "workflow_audit/invalid_actions_lock",
"observations": 1,
"rule_version": "0.1.0"
}
],
"support": {
"kind": "pattern"
}
},
{
"reason": "Job `triage` in label-triage.yml has no `timeout-minutes:` declaration. Default is 6 hours — a stuck codeload fetch or runner hang can burn budget. Add `timeout-minutes: 10` (or proportional).",
"type": "missing_timeout_minutes",
"file": ".github/workflows/label-triage.yml",
"level": "epi",
"action": "flag",
"rule_module": "workflow_audit",
"severity": "medium",
"recipe_id": "recipe-add-workflow-timeout-minutes",
"job": "triage",
"evidence": [
{
"span": {
"file": ".github/workflows/label-triage.yml",
"end_line": 0,
"start_line": 0
},
"rule": "workflow_audit/missing_timeout_minutes",
"observations": 1,
"rule_version": "0.1.0"
}
],
"support": {
"kind": "pattern"
}
},
{
"reason": "Job `sync` in labels.yml has no `timeout-minutes:` declaration. Default is 6 hours — a stuck codeload fetch or runner hang can burn budget. Add `timeout-minutes: 10` (or proportional).",
"type": "missing_timeout_minutes",
"file": ".github/workflows/labels.yml",
"level": "epi",
"action": "flag",
"rule_module": "workflow_audit",
"severity": "medium",
"recipe_id": "recipe-add-workflow-timeout-minutes",
"job": "sync",
"evidence": [
{
"span": {
"file": ".github/workflows/labels.yml",
"end_line": 0,
"start_line": 0
},
"rule": "workflow_audit/missing_timeout_minutes",
"observations": 1,
"rule_version": "0.1.0"
}
],
"support": {
"kind": "pattern"
}
},
{
"line": 39,
"reason": "job in .github/workflows/labels.yml references `secrets.*` but does not install `step-security/harden-runner` — review outbound-egress monitoring",
"type": "RE001",
"file": ".github/workflows/labels.yml",
"level": "epi",
"action": "report",
"rule_module": "research_extensions",
"severity": "medium",
"evidence": [
{
"span": {
"file": ".github/workflows/labels.yml",
"end_line": 39,
"start_line": 39
},
"rule": "research_extensions/RE001",
"observations": 1,
"rule_version": "0.1.0"
}
],
"support": {
"kind": "pattern"
}
},
{
"line": 53,
"reason": "job in .github/workflows/label-triage.yml references `secrets.*` but does not install `step-security/harden-runner` — review outbound-egress monitoring",
"type": "RE001",
"file": ".github/workflows/label-triage.yml",
"level": "epi",
"action": "report",
"rule_module": "research_extensions",
"severity": "medium",
"evidence": [
{
"span": {
"file": ".github/workflows/label-triage.yml",
"end_line": 53,
"start_line": 53
},
"rule": "research_extensions/RE001",
"observations": 1,
"rule_version": "0.1.0"
}
],
"support": {
"kind": "pattern"
}
},
{
"line": 87,
"reason": "job in .github/workflows/hypatia-scan.yml references `secrets.*` but does not install `step-security/harden-runner` — review outbound-egress monitoring",
"type": "RE001",
"file": ".github/workflows/hypatia-scan.yml",
"level": "epi",
"action": "report",
"rule_module": "research_extensions",
"severity": "medium",
"evidence": [
{
"span": {
"file": ".github/workflows/hypatia-scan.yml",
"end_line": 87,
"start_line": 87
},
"rule": "research_extensions/RE001",
"observations": 1,
"rule_version": "0.1.0"
}
],
"support": {
"kind": "pattern"
}
},
{
"line": 46,
"reason": "job in .github/workflows/push-email-notify.yml references `secrets.*` but does not install `step-security/harden-runner` — review outbound-egress monitoring",
"type": "RE001",
"file": ".github/workflows/push-email-notify.yml",
"level": "epi",
"action": "report",
"rule_module": "research_extensions",
"severity": "medium",
"evidence": [
{
"span": {
"file": ".github/workflows/push-email-notify.yml",
"end_line": 46,
"start_line": 46
},
"rule": "research_extensions/RE001",
"observations": 1,
"rule_version": "0.1.0"
}
],
"support": {
"kind": "pattern"
}
},
{
"line": null,
"reason": "actions.lock failed closed: {:line, 4, {:unsupported_version, \"v0.0.3\"}}",
"type": "invalid_actions_lock",
"file": ".github/workflows/actions.lock",
"level": "epi",
"action": "regenerate",
"rule_module": "workflow_hardening",
"severity": "high",
"evidence": [
{
"span": {
"file": ".github/workflows/actions.lock",
"end_line": 0,
"start_line": 0
},
"rule": "workflow_hardening/invalid_actions_lock",
"observations": 1,
"rule_version": "0.1.0"
}
],
"support": {
"kind": "pattern"
}
},
{
"line": 34,
"reason": "workflow .github/workflows/labels.yml:34 job `sync` has no `timeout-minutes:` — defaults to 360 min on hang",
"type": "WH006",
"file": ".github/workflows/labels.yml",
"level": "epi",
"action": "report",
"rule_module": "workflow_hardening",
"severity": "medium",
"evidence": [
{
"span": {
"file": ".github/workflows/labels.yml",
"end_line": 34,
"start_line": 34
},
"rule": "workflow_hardening/WH006",
"observations": 1,
"rule_version": "0.1.0"
}
],
"support": {
"kind": "pattern"
}
}
]Powered by Hypatia Neurosymbolic CI/CD Intelligence |
|
You have reached your Codex usage limits for code reviews. You can see your limits in the Codex usage dashboard. |
🔍 Hypatia Security ScanFindings: 47 issues detected
View findings[
{
"reason": "Required file missing",
"type": "missing",
"file": "0-AI-MANIFEST.a2ml",
"level": "epi",
"action": "create",
"rule_module": "root_hygiene",
"severity": "high",
"evidence": [
{
"span": {
"file": "0-AI-MANIFEST.a2ml",
"end_line": 0,
"start_line": 0
},
"rule": "root_hygiene/missing",
"observations": 1,
"rule_version": "0.1.0"
}
],
"support": {
"kind": "pattern"
}
},
{
"reason": "Job `triage` in label-triage.yml has no `timeout-minutes:` declaration. Default is 6 hours — a stuck codeload fetch or runner hang can burn budget. Add `timeout-minutes: 10` (or proportional).",
"type": "missing_timeout_minutes",
"file": ".github/workflows/label-triage.yml",
"level": "epi",
"action": "flag",
"rule_module": "workflow_audit",
"severity": "medium",
"recipe_id": "recipe-add-workflow-timeout-minutes",
"job": "triage",
"evidence": [
{
"span": {
"file": ".github/workflows/label-triage.yml",
"end_line": 0,
"start_line": 0
},
"rule": "workflow_audit/missing_timeout_minutes",
"observations": 1,
"rule_version": "0.1.0"
}
],
"support": {
"kind": "pattern"
}
},
{
"reason": "Job `sync` in labels.yml has no `timeout-minutes:` declaration. Default is 6 hours — a stuck codeload fetch or runner hang can burn budget. Add `timeout-minutes: 10` (or proportional).",
"type": "missing_timeout_minutes",
"file": ".github/workflows/labels.yml",
"level": "epi",
"action": "flag",
"rule_module": "workflow_audit",
"severity": "medium",
"recipe_id": "recipe-add-workflow-timeout-minutes",
"job": "sync",
"evidence": [
{
"span": {
"file": ".github/workflows/labels.yml",
"end_line": 0,
"start_line": 0
},
"rule": "workflow_audit/missing_timeout_minutes",
"observations": 1,
"rule_version": "0.1.0"
}
],
"support": {
"kind": "pattern"
}
},
{
"line": 39,
"reason": "job in .github/workflows/labels.yml references `secrets.*` but does not install `step-security/harden-runner` — review outbound-egress monitoring",
"type": "RE001",
"file": ".github/workflows/labels.yml",
"level": "epi",
"action": "report",
"rule_module": "research_extensions",
"severity": "medium",
"evidence": [
{
"span": {
"file": ".github/workflows/labels.yml",
"end_line": 39,
"start_line": 39
},
"rule": "research_extensions/RE001",
"observations": 1,
"rule_version": "0.1.0"
}
],
"support": {
"kind": "pattern"
}
},
{
"line": 53,
"reason": "job in .github/workflows/label-triage.yml references `secrets.*` but does not install `step-security/harden-runner` — review outbound-egress monitoring",
"type": "RE001",
"file": ".github/workflows/label-triage.yml",
"level": "epi",
"action": "report",
"rule_module": "research_extensions",
"severity": "medium",
"evidence": [
{
"span": {
"file": ".github/workflows/label-triage.yml",
"end_line": 53,
"start_line": 53
},
"rule": "research_extensions/RE001",
"observations": 1,
"rule_version": "0.1.0"
}
],
"support": {
"kind": "pattern"
}
},
{
"line": 87,
"reason": "job in .github/workflows/hypatia-scan.yml references `secrets.*` but does not install `step-security/harden-runner` — review outbound-egress monitoring",
"type": "RE001",
"file": ".github/workflows/hypatia-scan.yml",
"level": "epi",
"action": "report",
"rule_module": "research_extensions",
"severity": "medium",
"evidence": [
{
"span": {
"file": ".github/workflows/hypatia-scan.yml",
"end_line": 87,
"start_line": 87
},
"rule": "research_extensions/RE001",
"observations": 1,
"rule_version": "0.1.0"
}
],
"support": {
"kind": "pattern"
}
},
{
"line": 46,
"reason": "job in .github/workflows/push-email-notify.yml references `secrets.*` but does not install `step-security/harden-runner` — review outbound-egress monitoring",
"type": "RE001",
"file": ".github/workflows/push-email-notify.yml",
"level": "epi",
"action": "report",
"rule_module": "research_extensions",
"severity": "medium",
"evidence": [
{
"span": {
"file": ".github/workflows/push-email-notify.yml",
"end_line": 46,
"start_line": 46
},
"rule": "research_extensions/RE001",
"observations": 1,
"rule_version": "0.1.0"
}
],
"support": {
"kind": "pattern"
}
},
{
"line": 34,
"reason": "workflow .github/workflows/labels.yml:34 job `sync` has no `timeout-minutes:` — defaults to 360 min on hang",
"type": "WH006",
"file": ".github/workflows/labels.yml",
"level": "epi",
"action": "report",
"rule_module": "workflow_hardening",
"severity": "medium",
"evidence": [
{
"span": {
"file": ".github/workflows/labels.yml",
"end_line": 34,
"start_line": 34
},
"rule": "workflow_hardening/WH006",
"observations": 1,
"rule_version": "0.1.0"
}
],
"support": {
"kind": "pattern"
}
},
{
"line": 48,
"reason": "workflow .github/workflows/label-triage.yml:48 job `triage` has no `timeout-minutes:` — defaults to 360 min on hang",
"type": "WH006",
"file": ".github/workflows/label-triage.yml",
"level": "epi",
"action": "report",
"rule_module": "workflow_hardening",
"severity": "medium",
"evidence": [
{
"span": {
"file": ".github/workflows/label-triage.yml",
"end_line": 48,
"start_line": 48
},
"rule": "workflow_hardening/WH006",
"observations": 1,
"rule_version": "0.1.0"
}
],
"support": {
"kind": "pattern"
}
},
{
"line": 19,
"reason": "workflow .github/workflows/mirror.yml:19 uses `secrets: inherit` — forwards every caller secret to the reusable workflow",
"type": "WH008",
"file": ".github/workflows/mirror.yml",
"level": "epi",
"action": "report",
"rule_module": "workflow_hardening",
"severity": "medium",
"evidence": [
{
"span": {
"file": ".github/workflows/mirror.yml",
"end_line": 19,
"start_line": 19
},
"rule": "workflow_hardening/WH008",
"observations": 1,
"rule_version": "0.1.0"
}
],
"support": {
"kind": "pattern"
}
}
]Powered by Hypatia Neurosymbolic CI/CD Intelligence |
hyperpolymath
enabled auto-merge (squash)
October 19, 2026 22:16
|
You have reached your Codex usage limits for code reviews. You can see your limits in the Codex usage dashboard. |
🔍 Hypatia Security ScanFindings: 47 issues detected
View findings[
{
"reason": "Required file missing",
"type": "missing",
"file": "0-AI-MANIFEST.a2ml",
"level": "epi",
"action": "create",
"rule_module": "root_hygiene",
"severity": "high",
"evidence": [
{
"span": {
"file": "0-AI-MANIFEST.a2ml",
"end_line": 0,
"start_line": 0
},
"rule": "root_hygiene/missing",
"observations": 1,
"rule_version": "0.1.0"
}
],
"support": {
"kind": "pattern"
}
},
{
"reason": "Job `triage` in label-triage.yml has no `timeout-minutes:` declaration. Default is 6 hours — a stuck codeload fetch or runner hang can burn budget. Add `timeout-minutes: 10` (or proportional).",
"type": "missing_timeout_minutes",
"file": ".github/workflows/label-triage.yml",
"level": "epi",
"action": "flag",
"rule_module": "workflow_audit",
"severity": "medium",
"recipe_id": "recipe-add-workflow-timeout-minutes",
"job": "triage",
"evidence": [
{
"span": {
"file": ".github/workflows/label-triage.yml",
"end_line": 0,
"start_line": 0
},
"rule": "workflow_audit/missing_timeout_minutes",
"observations": 1,
"rule_version": "0.1.0"
}
],
"support": {
"kind": "pattern"
}
},
{
"reason": "Job `sync` in labels.yml has no `timeout-minutes:` declaration. Default is 6 hours — a stuck codeload fetch or runner hang can burn budget. Add `timeout-minutes: 10` (or proportional).",
"type": "missing_timeout_minutes",
"file": ".github/workflows/labels.yml",
"level": "epi",
"action": "flag",
"rule_module": "workflow_audit",
"severity": "medium",
"recipe_id": "recipe-add-workflow-timeout-minutes",
"job": "sync",
"evidence": [
{
"span": {
"file": ".github/workflows/labels.yml",
"end_line": 0,
"start_line": 0
},
"rule": "workflow_audit/missing_timeout_minutes",
"observations": 1,
"rule_version": "0.1.0"
}
],
"support": {
"kind": "pattern"
}
},
{
"line": 39,
"reason": "job in .github/workflows/labels.yml references `secrets.*` but does not install `step-security/harden-runner` — review outbound-egress monitoring",
"type": "RE001",
"file": ".github/workflows/labels.yml",
"level": "epi",
"action": "report",
"rule_module": "research_extensions",
"severity": "medium",
"evidence": [
{
"span": {
"file": ".github/workflows/labels.yml",
"end_line": 39,
"start_line": 39
},
"rule": "research_extensions/RE001",
"observations": 1,
"rule_version": "0.1.0"
}
],
"support": {
"kind": "pattern"
}
},
{
"line": 53,
"reason": "job in .github/workflows/label-triage.yml references `secrets.*` but does not install `step-security/harden-runner` — review outbound-egress monitoring",
"type": "RE001",
"file": ".github/workflows/label-triage.yml",
"level": "epi",
"action": "report",
"rule_module": "research_extensions",
"severity": "medium",
"evidence": [
{
"span": {
"file": ".github/workflows/label-triage.yml",
"end_line": 53,
"start_line": 53
},
"rule": "research_extensions/RE001",
"observations": 1,
"rule_version": "0.1.0"
}
],
"support": {
"kind": "pattern"
}
},
{
"line": 87,
"reason": "job in .github/workflows/hypatia-scan.yml references `secrets.*` but does not install `step-security/harden-runner` — review outbound-egress monitoring",
"type": "RE001",
"file": ".github/workflows/hypatia-scan.yml",
"level": "epi",
"action": "report",
"rule_module": "research_extensions",
"severity": "medium",
"evidence": [
{
"span": {
"file": ".github/workflows/hypatia-scan.yml",
"end_line": 87,
"start_line": 87
},
"rule": "research_extensions/RE001",
"observations": 1,
"rule_version": "0.1.0"
}
],
"support": {
"kind": "pattern"
}
},
{
"line": 46,
"reason": "job in .github/workflows/push-email-notify.yml references `secrets.*` but does not install `step-security/harden-runner` — review outbound-egress monitoring",
"type": "RE001",
"file": ".github/workflows/push-email-notify.yml",
"level": "epi",
"action": "report",
"rule_module": "research_extensions",
"severity": "medium",
"evidence": [
{
"span": {
"file": ".github/workflows/push-email-notify.yml",
"end_line": 46,
"start_line": 46
},
"rule": "research_extensions/RE001",
"observations": 1,
"rule_version": "0.1.0"
}
],
"support": {
"kind": "pattern"
}
},
{
"line": 34,
"reason": "workflow .github/workflows/labels.yml:34 job `sync` has no `timeout-minutes:` — defaults to 360 min on hang",
"type": "WH006",
"file": ".github/workflows/labels.yml",
"level": "epi",
"action": "report",
"rule_module": "workflow_hardening",
"severity": "medium",
"evidence": [
{
"span": {
"file": ".github/workflows/labels.yml",
"end_line": 34,
"start_line": 34
},
"rule": "workflow_hardening/WH006",
"observations": 1,
"rule_version": "0.1.0"
}
],
"support": {
"kind": "pattern"
}
},
{
"line": 48,
"reason": "workflow .github/workflows/label-triage.yml:48 job `triage` has no `timeout-minutes:` — defaults to 360 min on hang",
"type": "WH006",
"file": ".github/workflows/label-triage.yml",
"level": "epi",
"action": "report",
"rule_module": "workflow_hardening",
"severity": "medium",
"evidence": [
{
"span": {
"file": ".github/workflows/label-triage.yml",
"end_line": 48,
"start_line": 48
},
"rule": "workflow_hardening/WH006",
"observations": 1,
"rule_version": "0.1.0"
}
],
"support": {
"kind": "pattern"
}
},
{
"line": 19,
"reason": "workflow .github/workflows/mirror.yml:19 uses `secrets: inherit` — forwards every caller secret to the reusable workflow",
"type": "WH008",
"file": ".github/workflows/mirror.yml",
"level": "epi",
"action": "report",
"rule_module": "workflow_hardening",
"severity": "medium",
"evidence": [
{
"span": {
"file": ".github/workflows/mirror.yml",
"end_line": 19,
"start_line": 19
},
"rule": "workflow_hardening/WH008",
"observations": 1,
"rule_version": "0.1.0"
}
],
"support": {
"kind": "pattern"
}
}
]Powered by Hypatia Neurosymbolic CI/CD Intelligence |
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.
Summary
Adds a CI lane (in both
checkandcold-check) that typechecks every module underproofs/agda/experimental/echo-additive/on its own.Nothing is wired into the shipped closure.
All.agdaandSmoke.agdaare untouched, nothing in shipped code imports fromexperimental/, and the retraction R-2026-05-18 stands. The lane adds no claim; it only makes a break visible here.Why
choreographic-typesvendorsexperimental/echo-additive/Grade.agda(the ℕ∪{∞} grade dioid, "PROVEN-but-UNWIRED"). Today no echo-types CI job compiles that tree, so an edit that breaks it is found by a consumer, not by echo-types.Gate — needs the author's call before merge
experimental/echo-additive/DECISIONS.adoc(D-2026-06-14-R1) says nothing fromexperimental/goes tomainwithout the terminating condition and the author's explicit authorization. STATE.adoc records the terminating-condition half as met (R2–R4, 2026-06-15). I am treating this lane as covered by that gate and not merging it; it is a draft for the author to accept, change or close. If the author would rather keep the tree out of CI entirely, closing this PR loses nothing.What changed
.github/workflows/agda.yml: one step incheckand one incold-checkthat loops overproofs/agda/experimental/echo-additive/*.agda(a glob, so new experimental modules are included automatically). No newuses:, soactions.lockis unaffected.How has this been verified?
Locally with Agda 2.6.3, stdlib v2.3, absolute-zero
f486c29(the CI pin):Grade,VarianceGate,GradedCarrier,GradedCarrierFaithful,GradedMonad,GradedComonad,GradedAdjunction. Each declares--safe --without-K; none has apostulatedeclaration.bash tools/check-guardrails.sh proofs/agdapasses (210 modules).Cost: the first module pays for building stdlib interfaces on a cold run; the others take about 5 s each warm.
Generated by Claude Code