You signed in with another tab or window. Reload to refresh your session.You signed out in another tab or window. Reload to refresh your session.You switched accounts on another tab or window. Reload to refresh your session.Dismiss alert
docs: qualify external repo paths to clear structural_drift (SD022)
Hypatia structural_drift flagged `src/idris2/` and `src/aggregate/` in the
trope-integration design as dangling references "surviving a directory rename".
Both are deliberately *external*: the trope-checker repo's Idris2 core and the
panic-attack repo's aggregate module. Reword as unambiguously external (drop the
bare `src/<dir>/` form) so the heuristic no longer reads them as internal
error-lang tree paths. No substantive content change.
Co-Authored-By: Claude Opus 4.8 <noreply@anthropic.com>
Claude-Session: https://claude.ai/code/session_0195yA45jSSP7YDPwJSpw4bM
Copy file name to clipboardExpand all lines: docs/Trope-Particularity-Integration.adoc
+2-2Lines changed: 2 additions & 2 deletions
Display the source diff
Display the rich diff
Original file line number
Diff line number
Diff line change
@@ -55,7 +55,7 @@ Two further alignments make the fit unusually tight:
55
55
`echo_input`, `echo_output` implement witness-retention and irreversible erasure
56
56
— which the calculus names `preserve`, `detach`, and field `project` (§5).
57
57
* **The verification toolchains already overlap.** The trope-checker's core is an
58
-
Agda reference plus an Idris2 implementation (`trope-checker/src/idris2/Main.idr`);
58
+
Agda reference plus an Idris2 implementation (the `trope-checker` repo's Idris2 core, `Main.idr`);
59
59
Error-Lang already carries an Idris2 proof of the *scalar* bound
60
60
(`src/abi/Stability.idr`). The integration generalises that proof's target from
61
61
a clamped integer to a checked grade.
@@ -186,7 +186,7 @@ recoverable as a projection, but the verdict additionally names the edge to repa
186
186
| Trust boundary | Pin `trope-checker/schemas/trope-ir.schema.json` at `version 0.1`, `profile prevent`. The schema is the contract (mirrors the IR spec's "schema is the trust boundary").
187
187
| Dependency | Depend on the `trope-checker` *binary* (a pure `IR → verdict` function) and the *IR schema* by URL. Do **not** vendor the calculus, the checker, or `haec`.
188
188
| New backend | Add a `trope` lowering target beside the existing codegen backends: Error-Lang AST/VM ops → Trope IR DAG (schema-validated) → `trope-checker` → verdict object → surfaced as Error-Lang diagnostics.
189
-
| Precedent | The same trust-tagged "fold external prover output back into our report" pattern panic-attack uses in `src/aggregate/`.
189
+
| Precedent | The same trust-tagged "fold external prover output back into our report" pattern the panic-attack repo uses in its `aggregate/` module.
190
190
| Multi-producer | Sanctioned by `trope-ir.adoc`: "a static analyser for an existing language MAY emit Trope IR for code it did not author." Error-Lang's analyzer is exactly such a producer.
0 commit comments