Review fixes for #58: inline clause correctness and robustness #68

marfavi · 2026-10-22T13:59:25+02:00

marfavi commented

2026-10-22 13:59:25 +02:00

Scanner: the inline-body regex is replaced by an external scanner, so }}>, }> inside comments/strings, and empty or unterminated wrappers no longer lose the annotation (they become invalid_inline_clause_contents, and the linked INV/SPEC survives).
Validation: inline bodies are checked before anything is written; malformed annotations and SPEC_INLINE without SPEC are reported.
Inline sync: saves the proof document, distinguishes unavailable/not-found, finds the real top-level :=, keeps one terminator, and is CRLF-safe.
Forwarded diagnostics: no longer dropped for other proof documents, debounced, and emitted on the body instead of the wrapper.
Tests/docs: regression tests for the examples/sumarray corruption and a README update.

Verified with npm run check, 139 unit tests and 115/115 grammar corpus cases; the extension-host tests run in CI.

- **Scanner**: the inline-body regex is replaced by an external scanner, so `}}>`, `}>` inside comments/strings, and empty or unterminated wrappers no longer lose the annotation (they become `invalid_inline_clause_contents`, and the linked `INV`/`SPEC` survives). - **Validation**: inline bodies are checked before anything is written; malformed annotations and `SPEC_INLINE` without `SPEC` are reported. - **Inline sync**: saves the proof document, distinguishes `unavailable`/`not-found`, finds the real top-level `:=`, keeps one terminator, and is CRLF-safe. - **Forwarded diagnostics**: no longer dropped for other proof documents, debounced, and emitted on the body instead of the wrapper. - **Tests/docs**: regression tests for the `examples/sumarray` corruption and a README update. Verified with `npm run check`, 139 unit tests and 115/115 grammar corpus cases; the extension-host tests run in CI.

marfavi added 16 commits

2026-10-22 13:59:26 +02:00

fix(grammar): keep inline clause contents inside the annotation 8fa86a6894

The inline body was matched with /<(?:[^}]|}[^>])*}>/, which can contain
`*/`. A body missing its closing `}>` therefore ran past the annotation's
own terminator, swallowed the rest of the comment (e.g. a stray `}>` and the
`*/` after it) and still produced a well-formed `crocq_annotation`. The
extension then wrote that text into the linked Rocq definition, corrupting the
proof document.

Exclude `*/` and `}>` from the body (tree-sitter's regex engine has no
lookahead, so both are excluded by consuming the character that starts them).
A malformed inline clause now fails to parse instead of silently absorbing the
file; the follow-up commits report that failure to the user and validate the
contents before they are used.

Adds corpus coverage for SPEC_INLINE and for bodies with braces, products and
Coq comments, plus a parser regression test using the example that produced
the corrupted proof document.

fix(annotations): validate inline clause bodies before using them 6457674fab

The inline contents came straight from the tree-sitter token and were written
into the proof document unfiltered, so anything the grammar happened to accept
ended up in a Rocq definition. Move the wrapper/body rules into one pure,
unit-tested helper and use it when the annotation is checked: the body must be
wrapped in <{ ... }>, must not be empty, and must not contain the C annotation
terminator or a nested wrapper. Annotations now carry the unwrapped body, which
is what gets written, instead of re-deriving it at write time.

fix(diagnostics): report annotations that fail to parse e4977e69bb

An annotation that fails to parse never becomes a crocq_annotation node, and
only ERROR nodes *inside* an annotation were reported. A typo in an inline
clause (a missing `}>`, the link form typed after INV_INLINE, ...) therefore
silently disabled the whole annotation: no diagnostic, no inline override, and
no navigation or decoration for the linked clause either.

Report the outermost ERROR node that still contains an annotation start as
"malformed crocq annotation", and keep reporting parse errors inside
annotations as before. The walk is a pure function now, so it is unit tested
against the example from examples/sumarray that produced corrupted proof
documents.

fix(annotations): require a SPEC link for SPEC_INLINE 35b2913bfe

A function annotation without SPEC kept its SPEC_INLINE silently: the inline
clause was parsed and then ignored, because there was no link to attach it to.
Report "SPEC_INLINE clause requires a SPEC clause" instead.

Also fold the while-statement clause scan into the same accumulate-as-you-go
shape the function annotation uses, which fixes the message for a duplicate
INV_INLINE (it said INV) and names INV_INLINE in the unexpected-clause error.
The previous pre-scan is gone; a malformed INV clause still reports only its
own error and suppresses the annotation.

refactor: drop dead inline-clause code and duplication 0da35be1b1

- The "link + inline clause" selection was copy-pasted three times in
  inlineClauses.ts (and had already drifted: one copy tested kind !== 'PROOF',
  the others kind !== 'SPEC' && kind !== 'INV'). It is one helper now.
- `InlineClause.contentsNode` duplicated `node.contentsNode`; the contents node
  is only needed for ranges, so read it from the clause node.
- `LoopAnnotation.invClause` is always an INV link by construction, so the
  `kind === 'INV'` guards in goto.ts and rocqNavigation.ts were always true.

fix(inline-clauses): stop dropping forwarded diagnostics of other documents 774000baac

Forwarding cleared the whole diagnostic collection and then repopulated only
the proof document that triggered the event, so with two C files inlining into
different proof documents a diagnostics update in one wiped the forwarded
diagnostics of the other until its next update.

Recompute every inline target on each pass instead, keyed by the target's own
proof document, and debounce the burst of onDidChangeDiagnostics events (each
pass costs a definition lookup per annotation). Forwarded diagnostics now land
on the body between `<{` and `}>` rather than on the wrapper tokens too.

fix(inline-clauses): wait for the language server instead of doing nothing 0083b2cc95

A save whose definition lookup answered 'unavailable' (the server had not
loaded the proof document yet, which is the usual state right after opening a
workspace) returned silently: the inline body was never written and nothing
said so. 'not-found' was just as silent.

Retry the lookup for a few seconds, then tell the user whether the server is
still not ready or the definition does not exist. The retry loop is a small
pure helper with unit tests; the messages name the clause, target and file.

fix(inline-clauses): save the proof document after updating it fefe268c67

The inline body was applied as an editor edit and then left in an unsaved,
invisible buffer: the README promises the definition is replaced, but the file
on disk (what coqc and CI read) kept the old body until the user happened to
save a tab they may not even have open.

Save the proof document after applying the edit, report when that fails, and
log the update. The README documents the behaviour in a follow-up commit.

fix(inline-clauses): make the definition body replacement exact 1843ff68ed

Three ways the replacement could produce invalid Rocq:

- `indexOf(':=')` found the first assignment anywhere in the definition, so a
  type such as `(let y := 0 in y = 0)` was treated as the body start and the
  definition was cut in half. Find the first `:=` at bracket depth 0 instead,
  skipping Coq comments and strings (new pure scanner, unit tested).
- the replacement always appended a period, so a body pasted with one ended up
  as `..`, and a definition range that excludes the final period also got two.
  Keep exactly one, whichever the outline range includes.
- the "already up to date" check compared raw text, so CRLF documents were
  rewritten on every save. Normalise line endings for the comparison and write
  the replacement with the document's own EOL.

`inlineClauseEdit` now takes an options object and the validated body (the
wrapper rules live in one place, inlineClauseBody.ts).

fix(inline-clauses): do not forward diagnostics that only touch a definition 5288188944

rangesOverlap compared boundaries inclusively, so a diagnostic ending exactly
where the definition starts (or starting exactly where it ends) was treated as
belonging to the definition. Use strict position comparisons and move the
predicate into a vscode-free module so it can be unit tested with range
doubles.

test(inline-clauses): cover the corrupted-output example and test hygiene d77690e37e

- Add an extension-host regression test for the example from examples/sumarray
  that produced corrupted proof documents: a malformed inline clause must
  report "malformed crocq annotation" and leave the proof document (memory and
  disk) untouched.
- The end-to-end test wrote its fixtures into src/test/integration/test-assets,
  so a timeout left untracked files in the repository and parallel runs shared
  one directory; use the existing createTempDir helper instead.
- Pin the exact generated body instead of `includes('\nFalse.')`, which cannot
  tell `False.` from `False..`, and check the file on disk (the update is saved
  now, not just applied to a buffer).

docs: document inline clause overrides and their limits d440b594f2

The feature description promised that the linked definition is replaced, but
not that the proof document is saved, that the target must have a `:=` body,
that at most one inline clause is allowed, that its link is required, that the
C side wins over edits to the definition body, that the wrapper is a single
token (no annotation terminator, space before `}>` when the body ends with
`}`), or that proof diagnostics are mirrored into the C file.

fix: tie the inline diagnostics listener to the feature's lifetime a26137c727

InlineClauses exposed its diagnostics subscription so extension.ts could push
it separately, which made disposing the feature easy to get wrong; dispose it
with the rest of the feature instead.

Also give the save listener a rejection handler: an async event listener's
promise is ignored, so a failure in the document sync was an unhandled
rejection and, worse, skipped the inline clause sync entirely.

fix(inline-clauses): drop annotations of closed documents a935c21206

The annotation store was never cleaned up when a C document closed, so inline
clauses kept forwarding diagnostics for documents that were no longer open.
Remove the entry together with the document's parse state.

test(inline-clauses): keep fixtures inside the workspace 4135ec2b2e

Following up on the previous commit: the Rocq language server loads proof
documents that live inside the workspace folder, so a directory in the OS temp
dir is not a safe home for these fixtures. Create a unique directory inside the
extension's workspace under `out/` instead: still isolated and cleaned up, but
inside the tree the server serves. Also assert the VsRocq API is available in
the malformed-clause test, so a missing dependency fails immediately instead of
timing out waiting for a diagnostic.

fix(grammar): delimit inline clause bodies with an external scanner

Grammar / Corpus and binding tests (pull_request) Successful in 52s

Details

Extension / Format, types, lint, extension tests (pull_request) Failing after 3m4s

Details

fd9c5c7409

A regex cannot delimit `<{ ... }>`: the body may contain `}`, and the token
must not run past the annotation's own terminator. The regex workaround from
the earlier commit was correct for ordinary bodies but had to reject
`}}>`, could be fooled by `}>` in a Coq comment, and still lost the whole
annotation when the wrapper was malformed.

Replace it with an external scanner (src/scanner.c) that has the lookahead
the regex engine lacks:

- a valid wrapper ends at the first `}>` outside a Coq comment or string, so
  a body may contain `}` (including the `}}>` ending),
- the scanner never consumes the annotation's terminator; when the wrapper is
  not closed before it, it hands back `invalid_inline_clause_contents`, so
  the annotation still parses and the extension reports a precise diagnostic
  on the clause while keeping its linked INV/SPEC,
- the contents are optional, so an empty `INV_INLINE` is reported instead of
  losing the annotation,
- only text that starts with `<{` is claimed: during error recovery every
  external symbol is valid, and a token that matched anything would swallow
  the rest of the file.

The extension-side validator now allows `}>` inside the body (it can appear in
a Coq comment or string) and keeps rejecting the annotation terminator as
defence in depth. Corpus tests cover `}}>`, `}>` in a comment, an empty
clause, an unterminated wrapper and a wrapper on the next line; the unit and
end-to-end tests are updated to the new contract. The packaged extension no
longer ships src/scanner.c (it is compile-only).

marfavi added 1 commit

2026-10-22 14:05:01 +02:00

test(inline-clauses): use a clean fixture for the malformed wrapper

Grammar / Corpus and binding tests (pull_request) Successful in 1m8s

Details

Extension / Format, types, lint, extension tests (pull_request) Successful in 3m16s

Details

be768dd9cd

The end-to-end regression test kept the stray `}>` and `*/` lines from the
original corruption repro. Now that the scanner keeps the annotation alive,
those tokens sit between the annotation and its `while`, so the C parse no
longer attaches the annotation and the test waited for a wrapper diagnostic
that could never appear (CI: "Condition was not met within 15000 ms").

Drop the stray tokens: the annotation attaches to the loop again, the scanner
reports invalid contents, and the test asserts the wrapper diagnostic and an
untouched proof document.

EatOreo requested changes

2026-10-22 15:23:24 +02:00

extension/src/annotationParseErrors.ts Outdated

					
				@ -0,0 +1,64 @@

				import type { SyntaxNode as Node } from 'tree-sitter';

can this be in a subfolder of src/?

assuming you mean the whole file, yes