6
$\begingroup$

I’m currently trying out Visual Studio + VSCoq, having previously used Emacs + Proof General for Coq, and there’s one part of my usual workflow that I haven’t managed to replicate yet. Is there a way to issue an arbitrary Gallina query, via the prompt?

That is: Both VSCoq and Proof General provide specific commands to issue frequently used Gallina queries from the command prompt/minibuffer (e.g. VSCoq’s Coq: Prompt Check for Gallina’s Check). But often I want to issue a less-common Gallina query (e.g. Show, Eval), and either no editor command/keybinding is provided, or I haven’t memorised it yet. Proof General provides an excellent catch-all command for this situation: “Issue command” (C-c C-v), which lets the user type an arbitrary Gallina query in the minibuffer. Is there some equivalent in VSCoq?

Of course, there is a fallback option of typing the query in the proof script, stepping forward, then stepping back and deleting the line afterwards. But it would be nice to avoid these extra steps.

(To be technically precise: by “query”, I mean the kinds of Gallina command that Proof General classes as state-preserving — Check, About, Search, Print, and so on.)

Improve this question
$\endgroup$
1
  • 1
    $\begingroup$ It doesn't look like VSCoq has such an option at the moment; a workaround would be to open a terminal at the bottom (an ad hoc minibuffer) and use coqtop -l file so that you can interact with the file without modifying it. A downside to this is you have to rerun coqtop when you make a change, as far as I know. $\endgroup$
    – Andrew Marmaduke
    Jul 19, 2022 at 14:19

0

Reset to default

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service and acknowledge that you have read and understand our privacy policy and code of conduct.

Browse other questions tagged or ask your own question.