WIP: proof-of-concept: show proof status #45

Draft

EatOreo wants to merge 34 commits from feature/proof-status into main

pull from: feature/proof-status

merge into: code2rocq:main

code2rocq:main

code2rocq:release/0.1.0

code2rocq:fix/resync-on-v-rename

code2rocq:feat/infer-inline-declare

code2rocq:feat/grammar-highlighting

code2rocq:feat/clightgen-command-in-status

code2rocq:fix/code-lens-annotation-top

code2rocq:fix/inline-clauses-review-findings

Conversation 0 Commits 34 Files changed 25 +29530 -27976

EatOreo commented 2026-10-15 15:53:37 +02:00

Owner

• Copy link
• Copy Markdown

fixes #42

fixes #42

EatOreo added 21 commits 2026-10-15 15:53:38 +02:00

upsii cf0451b744

Find definitions in the VsRocq document outline bfc18353a4

Don't report missing annotations while VsRocq is starting 7350766209

wip d23c1134d4

Merge branch 'main' into find-by-symbol 0f4d38a416

Drop the per-lookup retries; the document resync already waits 568907dfa4

Show linked targets as pending while the language server is starting 50b2ff32d4

Catch VsRocq's synchronous startup errors in the proof lookup 18d672f3d7

Mute the pending linked-target diagnostic (hint, not information) 547bbe7aab

Merge remote-tracking branch 'origin/find-by-symbol' into navigation-smooth-af 2c73948210

handle links to wrong filetypes 6c9bff91a5

don't show loading ui anyway 0e03df7433

rm bs 8bc3914a71

dedupe some code d5b53998c5

less code duplication 10cd67cacf

Merge remote-tracking branch 'origin/find-by-symbol' into navigation-smooth-af 5482ef103e

Merge remote-tracking branch 'origin/main' into navigation-smooth-af 6221fe3e14

rm unrelated 075a2ada43

remove logic out from extension.ts ab2f666081

fix test c0b5aa8d23

beautiful proof statuses 8ca7a01071

EatOreo added 1 commit 2026-10-15 16:00:06 +02:00

Merge remote-tracking branch 'origin/main' into feature/proof-status 47bdc8a9cf

EatOreo referenced this pull request 2026-10-16 10:50:03 +02:00

Show status of proof next to PROOF clause #42

EatOreo added 1 commit 2026-10-16 10:52:08 +02:00

reveal range 87cea2d3f8

marfavi changed title from WIP: feature/proof-status to WIP: proof-of-concept: show proof status 2026-10-16 11:17:39 +02:00

EatOreo added 10 commits 2026-10-21 14:28:00 +02:00

proof of concept 7a1f22d64b

also spec_inline 1f6182d09f

rename to inline clause b9f82c227c

rename invInlineClause 84d281dcf5

refactor inline clauses 36cee8dac1

better diagnostics subscription 8418acf821

add comments and tests 6c293d7498

integration test e4d6d2c3b7

Merge branch 'proof-of-concept/inline-clauses' into feature/proof-status eb169c6990

rm duplication 1c1b455dbb

EatOreo added 1 commit 2026-10-29 13:41:43 +01:00

wip b44f320499

Some checks failed

Hide checks

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

Required

Details

Extension / Format, types, lint, extension tests (pull_request) Failing after 2m38s

Required

Details

This pull request has changes conflicting with the target branch.

• examples/sumarray/sumarray.c
• examples/sumarray/verif_sumarray_linked.v
• extension/README.md
• extension/README.md~refs_heads_feature_proof-status
• extension/src/annotations.ts
• extension/src/extension.ts
• extension/src/language_features/documentSync.ts
• extension/src/language_features/inlineClauses.ts
• extension/src/language_features/wordDecoration.ts
• extension/src/test/integration/inlineClauses.test.ts
• extension/src/test/unit/annotations.test.ts
• tree-sitter-crocq/grammar.js
• tree-sitter-crocq/src/grammar.json
• tree-sitter-crocq/src/node-types.json
• tree-sitter-crocq/src/parser.c
• tree-sitter-crocq/test/corpus/crocq_annotations.txt

View command line instructions

Manual merge helper

Use this merge commit message when completing the merge manually.

Merge commit title WIP: proof-of-concept: show proof status (#45)

Merge commit body Reviewed-on: https://git.marfavi.com/code2rocq/crocq/pulls/45

WIP: proof-of-concept: show proof status (#45) Reviewed-on: https://git.marfavi.com/code2rocq/crocq/pulls/45 Copy merge commit message

Checkout

From your project repository, check out a new branch and test the changes.

git fetch -u origin 'feature/proof-status:feature/proof-status'

git switch 'feature/proof-status'

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

Subscribe

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!45

No description provided.