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

Inline SPEC/INV bodies with inferred DECLARE #86

Open
marfavi wants to merge 4 commits from feat/infer-inline-declare into main
pull from: feat/infer-inline-declare
merge into: code2rocq:main
Conversation 0 Commits 4 Files changed 19 +29061 -29248
marfavi commented 2026-10-28 14:55:29 +01:00
Owner

Fixes #70

Write SPEC x.v:y <{ ... }> / INV x.v:y <{ ... }> directly; replaces SPEC_INLINE/INV_INLINE.

A spec's inline body may omit DECLARE; the function name is inferred and added in that case.

Before:

/*@
  SPEC verif_sumarray_inline.v:sumarray_spec
  SPEC_INLINE <{
    DECLARE _sumarray
    WITH a: val, sh : share, contents : list Z, size: Z
    ...
  }>
*/

After:

/*@
  SPEC verif_sumarray_inline.v:sumarray_spec <{
    WITH a: val, sh : share, contents : list Z, size: Z
    ...
  }>
*/

Same for INV / INV_INLINE. DECLARE _sumarray is inferred from the function name.

Fixes #70 Write `SPEC x.v:y <{ ... }>` / `INV x.v:y <{ ... }>` directly; replaces `SPEC_INLINE`/`INV_INLINE`. A spec's inline body may omit DECLARE; the function name is inferred and added in that case. --- Before: ``` /*@ SPEC verif_sumarray_inline.v:sumarray_spec SPEC_INLINE <{ DECLARE _sumarray WITH a: val, sh : share, contents : list Z, size: Z ... }> */ ``` After: ``` /*@ SPEC verif_sumarray_inline.v:sumarray_spec <{ WITH a: val, sh : share, contents : list Z, size: Z ... }> */ ``` Same for `INV` / `INV_INLINE`. `DECLARE _sumarray` is inferred from the function name.
Infer DECLARE for SPEC_INLINE from the C function (#70)
All checks were successful
Grammar / Corpus and binding tests (pull_request) Successful in 1m9s
Details
Extension / Format, types, lint, extension tests (pull_request) Successful in 2m45s
Details
577bfdf931
marfavi changed title from Infer DECLARE for SPEC_INLINE from the C function to WIP: Infer DECLARE for SPEC_INLINE from the C function 2026-10-29 10:19:11 +01:00
Remove the separate SPEC_INLINE and INV_INLINE clauses
All checks were successful
Grammar / Corpus and binding tests (pull_request) Successful in 45s
Details
Extension / Format, types, lint, extension tests (pull_request) Successful in 1m54s
Details
26fa6f4ec5
marfavi changed title from WIP: Infer DECLARE for SPEC_INLINE from the C function to Inline SPEC/INV bodies with inferred DECLARE 2026-10-29 15:49:52 +01:00
All checks were successful
Grammar / Corpus and binding tests (pull_request) Successful in 45s
Required
Details
Extension / Format, types, lint, extension tests (pull_request) Successful in 1m54s
Required
Details
This pull request has changes conflicting with the target branch.
  • extension/README.md
  • extension/README.md~refs_heads_feat_infer-inline-declare
View command line instructions

Manual merge helper

Use this merge commit message when completing the merge manually.

Checkout

From your project repository, check out a new branch and test the changes.
git fetch -u origin 'feat/infer-inline-declare:feat/infer-inline-declare'
git switch 'feat/infer-inline-declare'
Sign in to join this conversation.
Reviewers
No reviewers
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
1 participant
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!86
No description provided.