Shortcut for CoqIde `Compile` => `Compile Buffer`

[gabrielle-ohlson]

What is the shortcut/command name for compiling a buffer in vscoq (as one would do with Compile Buffer in CoqIde's toolbar)? I can find the interpret commands, but I am unsure how to compile the file.v to produce a file.vo etc.

Thanks!

[artagnon]

As far as I know, there are no build commands available in VSCoq. I personally just hit make or dune build in the integrated terminal in VSCode.

[rtetley]

I am closing this for now as it feels like the proposed solution works well enough.