Diagnostics
The reader of a sysr diagnostic is often a program: a model repairing its design, or the benchmark scoring it. So every problem is one structure with a stable code, a span, a message and, where they apply, the obligation that failed, a trace and fixes. sysr check --json prints that structure; the text a person reads is rendered from it, never written separately.
CODES in sysr/diag.rkttests/corpus, at least one for every code but I001tests/diag-test.rktJSON first, text derived
sysr/diag.rkt defines one diagnostic struct (code, severity, span, message, related spans, expected and actual types, obligation, trace, fixes, module) and one report per run (the file, the top module, the diagnostics, the holes, the assumes and some counts). report->jsexpr turns a report into JSON, leaving out every optional key that is empty. render-text starts from that same JSON and prints each diagnostic as file:line:col: severity[CODE]: message, then its details, then one summary line. So the two forms cannot disagree: the text is a view of the JSON, and tests/diag-test.rkt checks that a trace survives the trip.
The JSON is the same shape as sysp's diagnostics, with trace in place of sysp's counterexample; P001 and P002 come from the reader the two languages share and mean the same in both registries (import-reader-diagnostics). A report is ok when it has no error and no hole: a warning (W001, an assume) does not fail a check, but a hole (H001, severity info) does.
The shape of a diagnostic
Below are two views of one report: the text sysr check printed for the docs' buggy counter when the docs were built, and the JSON it was rendered from. Select a key to see where it shows in the text, or that it does not.
sysr check --json (the structure)
sysr check (the text, rendered from it)
sysr itself writes keys in any order.The keys a diagnostic can carry, from diagnostic->jsexpr:
| Key | When | What it holds |
|---|---|---|
code | always | a registered code, such as V004; report-add! raises an error for any other |
severity | always | error, warning (W001) or info (H001) |
span | always | file, line, col, end_line, end_col and the character offsets start and end |
message | always | one sentence, with the offending expression written back as sysr |
module | when known | the module the problem is in |
related | when there are any | other spans with a message each, such as the first definition of a name defined twice; printed as note: lines |
expected, actual | type errors | both types, such as (bits 8) and (bits 9) |
obligation | V codes but V005 | what had to be proven, as a sysr expression |
trace | when the solver found one | kind (from-reset or induction), depth, fails_at, and cycles: each cycle's inputs, regs and, if the module has instances, the instances' outputs |
fixes | when there is a likely repair | each a description and, where one is known, a replacement |
Beside the diagnostics, a report has holes (each hole's name, expected type and the signals in scope, so a model can fill it), assumes (the span of every assume, listed in every summary) and stats: modules, obligations, how many were proven, the deepest k at which one was proven, and the time. If a module is elaborated with several parameter sets, a fault in its text is reported once: report-add! drops a second diagnostic with the same code at the same place.
Two real reports
The docs' example counter-bug.sysr counts to 10 where it should wrap after 9, so its promise (<= q 9) is false. Whether sysr can show that from reset depends on how deep it looks. With the default --depth 8 it cannot: the counter needs more cycles than that to reach 10, so the report is V007, "not inductive", with an induction trace. With --depth 12 it is V002 with a trace from reset: a real bug. Step through either report line by line.
count in each cycle, the dashed line the promise q ≤ 9, the red point the cycle where it fails. An amber first point marks a state the solver chose freely, which may not be reachable.Why V007 first: k-induction tries k = 1 to 8. The base case looks for a failure in the first k cycles after reset and finds none: in 8 cycles from reset the counter gets no further than 7. The step asks whether any k+1 consecutive, pairwise distinct states in which the promise holds in the first k must keep it in the last; even at k = 8 the solver answers no, with the run in the induction trace, which climbs to 10. sysr cannot tell whether that start is reachable, so it says the property "holds from reset for 8 cycles but is not inductive" and suggests an invariant. Here no invariant helps, because the bug is real; looking deeper turns it into V002. The reference says so too: a real bug that needs more cycles than the depth is also reported as V007.
In both runs the summary says 1/2 obligations proven at k-induction depth 5: the other obligation is that (+ count 1) does not overflow its 4 bits, which holds. The depth in the summary is the deepest k at which some obligation was proven, not the depth searched.
What a model is shown
In the benchmark's write-check-repair loop (bench loop), a sysr candidate is built with sysr build --json, and the scorer turns the JSON into a short list: each diagnostic's line, column, severity, code and message, and each hole with its expected type (render-check in bench/score.rkt). After a failed attempt the model gets that list, under the outcome, and is asked for the whole corrected file. The trace and the fixes are not passed on, but for V codes the message already names the obligation. For the report above, the model would read:
The registry
CODES in sysr/diag.rkt lists every code with a one-line meaning. The registry is append-only, and it is exactly the table in specs/001-core-and-bench/contracts/diagnostics.md: tests/diag-test.rkt reads both and compares them. The first letter says what kind of problem it is. "Raised in" is found here by searching the toolchain's source (from data.js) for the quoted code; the corpus column is each code's design in tests/corpus, which tests/check-test.rkt and tests/verify-test.rkt check reports exactly the codes its ; expect: line names.
| Code | Meaning | Raised in | Corpus design |
|---|