Expose interpret proof to the command palette #55

New issue

Open

opened 2026-10-16 14:09:17 +02:00 by marfavi · 0 comments

marfavi commented

2026-10-16 14:09:17 +02:00

Owner

crocq.interpretProof is registered by the extension (PR #54) but not declared in package.json's contributes.commands, so it is only reachable through the Crocq: Interpret proof code lens.

The lens passes the command two arguments it needs: the Uri of the Rocq proof document and the position to interpret to. To make the command useful from the palette it has to infer that context itself, e.g.:

find the C function the cursor is standing in,
look up its PROOF file.v:proof_name annotation,
resolve the proof document and the proof block (as the lens does) to get the position to interpret to.

That is a bit more than the lens PR, hence this separate issue. Once the command can derive the context, declare it in contributes.commands so it shows up in the palette (and can be bound to a keybinding).

`crocq.interpretProof` is registered by the extension (PR #54) but not declared in `package.json`'s `contributes.commands`, so it is only reachable through the `Crocq: Interpret proof` code lens. The lens passes the command two arguments it needs: the Uri of the Rocq proof document and the position to interpret to. To make the command useful from the palette it has to infer that context itself, e.g.: - find the C function the cursor is standing in, - look up its `PROOF file.v:proof_name` annotation, - resolve the proof document and the proof block (as the lens does) to get the position to interpret to. That is a bit more than the lens PR, hence this separate issue. Once the command can derive the context, declare it in `contributes.commands` so it shows up in the palette (and can be bound to a keybinding).

marfavi added this to the Release roadmap project

2026-10-22 14:51:14 +02:00

marfavi added the

quick-pick

label

2026-10-29 15:02:52 +01:00