Repository navigation
proofs: make all modules pass the strict flag set - #45
Merged
Merged
Conversation
Fixes the sites the strict-flag survey found: - Kripke.Residual.Is: list all nine constructor pairs instead of ending in a catch-all. The values are unchanged. - EchoBridge.≤G-trans: put the top≤ clause first, so the case tree splits on the second argument before the first. - ProofTransportExample.checkPayload: put the ImpossibleClaim clause first, for the same reason. Each function computes the same values on constructor arguments; the changes only make every clause hold definitionally. Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01MF5GeeBBDF6sUzr6pZTjWV
Contributor
|
No actionable comments were generated in the recent review.
 |
| Layer / File(s) | Summary |
|---|---|
Pattern clause adjustments src/EpistemicTypes/EchoBridge.agda, src/EpistemicTypes/Kripke/Residual.agda, src/EpistemicTypes/ProofTransportExample.agda |
≤G-trans uses a catch-all clause for a second proof of top≤. Is uses explicit clauses for false cases. checkPayload places ImpossibleClaim before the ArtifactIsTrue cases. The described results remain unchanged. |
Priority:
Estimated code review effort: 1 (Trivial) | ~3 minutes
Change: Refactor
Merge Risk: 
039c0
-
The clause changes preserve the inspected behavior, with no actionable merge-blocking risk identified.
Pre-merge checks: 
-
Check name Status Explanation Title check The title clearly identifies the main change: updating proofs so all modules pass the strict flag set. Description check The description directly explains the three clause changes, the strict Agda flags, and the reported verification results. 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.
- 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.
![coderabbitai[bot]](https://avatars.githubusercontent.com/in/347564?s=60&v=4){kind=small}
hyperpolymath
enabled auto-merge (squash)
October 26, 2026 22:27
Contributor
|
Add Carrot credits or activate Agent usage billing to use Autofix |
hyperpolymath
disabled auto-merge
October 27, 2026 00:09
hyperpolymath
added a commit
that referenced
this pull request
Oct 27, 2026
## Summary #45 made the code compatible with the strict Agda flag set. This PR declares the flags in the files. `--cubical-compatible` is coinfective: a module that declares it may only import modules that also declare it. So choreographic-types cannot adopt the strict set while the epistemic-types modules it imports lack the flag. - **All 22 source modules and all 13 rejection fixtures:** the `OPTIONS` pragma gains `--cubical-compatible --exact-split --no-sized-types --no-guardedness`, keeping `--safe --without-K`. - **`tests/check-proofs.sh` and `tests/check-rejections.sh`:** both now also pass `-W noUnsupportedIndexedMatch`. - Under `--cubical-compatible`, Agda emits an `UnsupportedIndexedMatch` warning at 23 clauses that match on indexed constructors. It means those functions would not compute on Cubical transports. - That is irrelevant under `--without-K`. The estate strict set silences it, as agda-stdlib's own library file does. - Both scripts run with `-W error`, so without the flag the warning would be fatal. - Sites: - `Applications/IntegerModel`: 3 - `Applications/SortedRow`: 2 - `ContinuityExamples`: 1 - `EchoBridge`: 2 - `Examples`: 1 - `Kripke/Belief`: 1 - `Kripke/Dependence`: 1 - `Kripke/Residual`: 1 - `ProofTransport`: 6 - `ReadConsistency`: 2 - `SurrealBridge`: 3 - **`tests/integration/CanonicalEcho.agda` is unchanged.** It imports echo-types at pin `46cd1a3`, whose modules do not yet declare the flag. A file without the flag may still import ones that have it, so it keeps building. Add the flag after the pin moves to an echo-types commit that carries hyperpolymath/echo-types#357's change. ## Verification (Agda 2.6.3 locally; CI checks the pinned 2.6.4.3) - `tests/check-proofs.sh`: PASS, 22 source modules. - `tests/check-rejections.sh`: PASS, all 13 rejected for the expected type mismatch. - `CanonicalEcho.agda`, built against echo-types `46cd1a3` exactly as the workflow does: compiles. --- _Generated by [Claude Code](https://claude.ai/code/session_01MF5GeeBBDF6sUzr6pZTjWV)_ 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
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
This PR fixes the three
--exact-splitsites that failed the strict Agda flag set. These are clause splits and reorderings only. No theorem statements change.The strict set:
OPTIONSpragma:--safe --without-K --cubical-compatible --exact-split --no-sized-types --no-guardedness.--double-check -W error -W noUnsupportedIndexedMatch.Kripke/Residual.agda(Is)Is b b = ⊤; Is _ _ = ⊥.EchoBridge.agda(≤G-trans)_ top≤clause first.ProofTransportExample.agda(checkPayload)_ ImpossibleClaim _clause first.Verification
agda --no-libraries -i src src/EpistemicTypes/All.agdaexits 0.The repo pins Agda 2.6.4.3, so this PR's CI run is the check on the real toolchain. The clause shapes involved behave the same way under
--exact-splitin both versions.Generated by Claude Code