code completions suggesting proofs/definitions to link to when writing a PROOF or SPEC clause #23

New issue

Open

opened 2026-10-09 15:06:57 +02:00 by EatOreo · 0 comments

EatOreo commented

2026-10-09 15:06:57 +02:00

Owner

first do #56

When typing in a SPEC/PROOF clause link like:
PROOF verif_thing.v:body_...
We could suggest the lemmas/theorems inside verif_thing.v as code completions, we can access already get all lemmas/theorems in a rocq file via the vsrocq api: src/commands/services/vsrocq/vsrocq-api.ts
So we would register a completionProvider checking if the cursor is inside a SPEC/PROOF clause_contents node, then fetch all relevant suggestions

first do #56 When typing in a SPEC/PROOF clause link like: PROOF verif_thing.v:body_...<cursor> We could suggest the lemmas/theorems inside verif_thing.v as code completions, we can access already get all lemmas/theorems in a rocq file via the vsrocq api: src/commands/services/vsrocq/vsrocq-api.ts So we would register a completionProvider checking if the cursor is inside a SPEC/PROOF clause_contents node, then fetch all relevant suggestions

EatOreo referenced this issue

2026-10-16 14:10:53 +02:00

general code completions #56

EatOreo added the

blocked

label

2026-10-16 14:11:00 +02:00