code2rocq/crocq
code2rocq/crocq
Watch
3
2
Fork
You've already forked crocq
 0
Code Issues 18 Pull requests 3 Projects 1 Releases 1 Packages 2 Activity Actions

Add inline versions of INV and SPEC clauses #58

Merged
marfavi merged 13 commits from proof-of-concept/inline-clauses into main 2026-10-28 10:21:28 +01:00
Conversation 4 Commits 13 Files changed 29 +29393 -26702
EatOreo commented 2026-10-16 15:27:12 +02:00
Owner
No description provided.
proof of concept
All checks were successful
Grammar / Corpus and binding tests (pull_request) Successful in 41s
Details
Extension / Format, types, lint, extension tests (pull_request) Successful in 2m4s
Details
7a1f22d64b
EatOreo changed title from WIP: proof of concept to WIP: proof of concept: inline clauses 2026-10-16 15:27:38 +02:00
also spec_inline
Some checks failed
Grammar / Corpus and binding tests (pull_request) Successful in 52s
Details
Extension / Format, types, lint, extension tests (pull_request) Has been cancelled
Details
1f6182d09f
rename to inline clause
All checks were successful
Grammar / Corpus and binding tests (pull_request) Successful in 40s
Details
Extension / Format, types, lint, extension tests (pull_request) Successful in 1m53s
Details
b9f82c227c
rename invInlineClause
All checks were successful
Grammar / Corpus and binding tests (pull_request) Successful in 42s
Details
Extension / Format, types, lint, extension tests (pull_request) Successful in 1m48s
Details
84d281dcf5
refactor inline clauses
Some checks failed
Grammar / Corpus and binding tests (pull_request) Successful in 47s
Details
Extension / Format, types, lint, extension tests (pull_request) Failing after 53s
Details
36cee8dac1
better diagnostics subscription
All checks were successful
Grammar / Corpus and binding tests (pull_request) Successful in 49s
Details
Extension / Format, types, lint, extension tests (pull_request) Successful in 1m53s
Details
8418acf821
add comments and tests
All checks were successful
Grammar / Corpus and binding tests (pull_request) Successful in 38s
Details
Extension / Format, types, lint, extension tests (pull_request) Successful in 1m38s
Details
6c293d7498
integration test
All checks were successful
Grammar / Corpus and binding tests (pull_request) Successful in 43s
Details
Extension / Format, types, lint, extension tests (pull_request) Successful in 1m43s
Details
e4d6d2c3b7
EatOreo commented 2026-10-21 14:10:54 +02:00
Author
Owner

fixes #50

fixes #50
EatOreo commented 2026-10-21 14:11:21 +02:00
Author
Owner

feature

[feature](https://drive.google.com/file/d/1WxnW4BLuLsERndH2i9Mz6br3U_-ETMGa/view?usp=drive_link)
EatOreo changed title from WIP: proof of concept: inline clauses to inline clauses 2026-10-21 14:12:06 +02:00
marfavi self-assigned this 2026-10-22 10:02:09 +02:00
marfavi changed title from inline clauses to Add inline versions of INV and SPEC clauses 2026-10-22 10:03:08 +02:00
Merge branch 'main' into proof-of-concept/inline-clauses
All checks were successful
Grammar / Corpus and binding tests (pull_request) Successful in 55s
Details
Extension / Format, types, lint, extension tests (pull_request) Successful in 1m53s
Details
34615300fd
Merge remote-tracking branch 'origin/main' into proof-of-concept/inline-clauses
Some checks failed
Grammar / Corpus and binding tests (pull_request) Successful in 1m2s
Details
Extension / Format, types, lint, extension tests (pull_request) Failing after 3m2s
Details
c65a30d8b5
 
# Conflicts:
#	extension/src/extension.ts
#	extension/src/language_features/documentSync.ts
test(stale-model): expect the SPEC_INLINE-aware clause message
Some checks are pending
Extension / Format, types, lint, extension tests (pull_request) Waiting to run
Details
Grammar / Corpus and binding tests (pull_request) Waiting to run
Details
5da4239a22
Review fixes for #58: inline clause correctness and robustness (#68)
All checks were successful
Grammar / Corpus and binding tests (pull_request) Successful in 49s
Details
Extension / Format, types, lint, extension tests (pull_request) Successful in 2m16s
Details
ec4263fd06 
- **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.

Co-authored-by: EatOreo <[email protected]>
Reviewed-on: #68
Co-authored-by: Omid Marfavi <[email protected]>
Co-committed-by: Omid Marfavi <[email protected]>
build: reinstall the grammar when node_modules is stale
Some checks failed
Grammar / Corpus and binding tests (pull_request) Successful in 48s
Details
Extension / Format, types, lint, extension tests (pull_request) Has been cancelled
Details
ee6af2bc99
marfavi force-pushed proof-of-concept/inline-clauses from ee6af2bc99
Some checks failed
Grammar / Corpus and binding tests (pull_request) Successful in 48s
Details
Extension / Format, types, lint, extension tests (pull_request) Has been cancelled
Details
to ec4263fd06
All checks were successful
Grammar / Corpus and binding tests (pull_request) Successful in 49s
Details
Extension / Format, types, lint, extension tests (pull_request) Successful in 2m16s
Details
2026-10-23 15:35:04 +02:00 Compare
EatOreo scheduled this pull request to auto merge when all checks succeed 2026-10-23 15:43:28 +02:00
Merge remote-tracking branch 'origin/main' into proof-of-concept/inline-clauses
All checks were successful
Grammar / Corpus and binding tests (pull_request) Successful in 43s
Details
Extension / Format, types, lint, extension tests (pull_request) Successful in 1m39s
Details
5816963d4c
 
Conflict resolution in `extension/src/extension.ts`:

- `annotationStore` is now declared once, at the top of `activate()` next to
  `crocqParser`, as main moved it (the create-proof-files command needs the
  parser before the workspace services are wired).
- Kept the inline-clauses `onDocumentSaved` wrapper and added `inlineClauses`
  to the single `context.subscriptions.push(...)` that main consolidated. No
  disposable is pushed twice: the diagnostics collections, the navigation
  provider and the code-lens provider moved into that push, so the earlier
  separate push from this branch was dropped.

Also restored the generation bookkeeping of the "Create Rocq model" command,
which main's #28 merge resolution left behind: the command was registered with
a second, bare `createRocqModelHandler()` that omitted `modelGeneration` and
`onModelCreated`, leaving an orphaned comment fragment. A manually generated
model therefore recorded no hash and the stale-model warning fired right away.
The command uses the shared `createRocqModel` handler again.

Verified: prettier, format parity, tsc, eslint, 200 unit tests and 66
integration tests all pass.
marfavi reviewed 2026-10-23 16:07:00 +02:00
examples/sumarray/sumarray.c
@ -3,3 +3,3 @@
/*@
SPEC verif_sumarray.v:sumarray_spec
PROOF verif_sumarray.v:body_sumarray
SPEC verif_sumarray.v:sumarray_spec
marfavi commented 2026-10-22 10:16:08 +02:00
Owner

Swapping these for code lens aesthetic, maybe the code lens should just always be at the top of a Crocq annotation (out of scope of this PR, create separate issue)

Swapping these for code lens aesthetic, maybe the code lens should just always be at the top of a Crocq annotation (out of scope of this PR, create separate issue)
marfavi commented 2026-10-28 10:17:29 +01:00
Owner

#75

#75
marfavi marked this conversation as resolved
examples/sumarray/sumarray.c
@ -12,2 +12,4 @@
/*@
INV verif_sumarray.v:loop_invariant
INV_INLINE <{
EX i: Z,
marfavi commented 2026-10-22 10:23:51 +02:00
Owner

Handle whitespace so we indent this inline def without impacting generated output

Handle whitespace so we indent this inline def without impacting generated output
marfavi commented 2026-10-28 10:17:16 +01:00
Owner

let's look at this in another branch (see issue #76)

let's look at this in another branch (see issue #76)
marfavi marked this conversation as resolved
extension/src/annotations.ts Outdated
@ -21,0 +22,4 @@
kind: 'INV_INLINE' | 'SPEC_INLINE';
node: ClauseNode;
contentsNode: Node;
filePath?: never;
marfavi commented 2026-10-22 10:27:30 +02:00
Owner

never types, are they necessary?

`never` types, are they necessary?
marfavi marked this conversation as resolved
marfavi scheduled this pull request to auto merge when all checks succeed 2026-10-28 10:20:34 +01:00
marfavi approved these changes 2026-10-28 10:21:21 +01:00
marfavi deleted branch proof-of-concept/inline-clauses 2026-10-28 10:21:30 +01:00
Sign in to join this conversation.
Reviewers
No reviewers
marfavi
Labels
Clear labels   
blocked
should wait for another issue to be addressed

  
bug

   
priority!

   
quick-pick
No labels
blocked
bug
priority!
quick-pick
Milestone
Clear milestone
No items
No milestone
Projects
Clear projects
No items
No project
Assignees
Clear assignees
No assignees
marfavi
EatOreo
2 participants
Notifications
Due date
The due date is invalid or out of range. Please use the format "yyyy-mm-dd".

No due date set.

Dependencies

No dependencies set

Reference
code2rocq/crocq!58
No description provided.