This is going to be a similar post to my previous Visual Studio Code post from March, but about a different extension.

Coq (the French word for rooster) is a theorem prover that can be used both to prove mathematical theorems, and (in theory) to produce software that is "certified correct" via its proof-checking kernel and code generation facilities. It is also a dependently-typed programming language in its own right. I have been interested in dependent type systems for a long time – I founded the Dependent Types subreddit – and I implemented the code and proofs for my MSc thesis in Coq over a decade ago. I haven't used Coq very much since then, but it has continued to be developed and had more and more features added – like Haskell, it's a language and community with a long pedigree. In fact, it's slightly older than Haskell, which itself dates from 1990.

The workhorse IDE integration for Coq for a long time was Proof General, which integrated Coq into emacs. (As an aside, Proof General's formerly rather imposing "military general" logo has been replaced by an IMO somewhat twee anime girl general.) Coq also has a native IDE called CoqIDE, which is quite nice. However, it's 2020, so I wondered if there was a Visual Studio Code extension for Coq by now – and sure enough, there was – VSCoq! I should state, as a disclaimer, that I haven't really used it non-trivially yet, but in my view, at worst this is going to be another viable option to choose from to develop Coq proof scripts or programs from within a GUI, and at best, this setup might offer some additional features or convenience over the other two alternatives I just mentioned.

In contrast to the Haskell VScode extension that I wrote about last time, VSCoq doesn't have a new, dedicated backend process that you have to install – rather, it's necessary (and sufficient) to simply install Coq itself, whose existing binaries provide the necessary XML-based backend.

Running VSCoq under Flatpak

I wanted to try it out on Linux, but I have installed Coq on the Guix Linux distribution, and VSCode is not available in the official Guix package repositories, so I chose to install it using flatpak instead. Firstly, because on Guix flathub isn't configured as a source of flatpaks by default, I began by adding it:

flatpak --user remote-add flathub https://flathub.org/repo/flathub.flatpakrepo

Because the flatpak I used last time for VSCode has not been kept up-to-date, I chose this time to install a different open source build of VSCode, called VSCodium:

flatpak install --user flathub com.vscodium.codium

Unfornately flatpak didn't install a desktop entry – or at least not one that that the XFCE desktop on Guix recognised – so once again, I had to run it from the command line. This turned out to be the necessary incantation:

flatpak run --user com.vscodium.codium

From my adventures last time with the VSCode Haskell extension, I was aware that the VSCoq extension wasn't going to work without some tweaking to the settings. Once again, because flatpacks run in their own isolated container, I needed to create some wrapper scripts to allow the flatpak to call out to the Coq binaries that I'd installed in the main Guix operating system, outside of the flatpak container.

Initially, I couldn't get my wrapper scripts to work. It took installing auditd, getting it working, and fiddling with it for a bit to see the commands that were actually being run to figure out what was going wrong here.

In case anyone is wondering, the command I ended up using to get the necessary information logged was:

sudo auditctl -a exit,always -F euid=1000 -F arch=b64 -S execve -k user-execs

and when I had found the necessary information, I disabled the logging again using:

sudo auditctl -D

Basically, the problem turned out to be that on Guix there is no coqidetop.opt, only a coqidetop. So I fixed my scripts, and the solution I ended up with was two very similar scripts, one saved in /usr/local/bin/coqidetop.opt containing:

#! /bin/bash
exec flatpak-spawn --forward-fd=1 --host --watch-bus --env=BASH_ENV=~/.bashrc bash -c "coqidetop $*"

and one saved in /usr/local/bin/coqtop containing:

#! /bin/bash
exec flatpak-spawn --forward-fd=1 --host --watch-bus --env=BASH_ENV=~/.bashrc bash -c "coqtop $*"

with both marked executable (sudo chmod a+x /usr/local/bin/coq*). It seems that the user's full home directory (as opposed to individual files and directories opened by the user) isn't visible by default from the Codium flatpak, so I couldn't have put those scripts under my home directory.

The --env=BASH_ENV=~/.bashrc part forces bash to reload .bashrc, so that the PATH variable will be set correctly, which is very important in Guix as it doesn't use the usual Linux Filesystem Hierarchy Standard, and in particular standard locations like /bin and /usr/bin are not where to find installed programs. You might not need that part of the script, but it's unlikely to hurt.

Then, in the preferences for the extension (which are not be found on the extension's page, as it's done in Chromium, but in the VSCode settings, as it's done in most other applications), I set the directory path to the path that the directory containing those two scripts is visible from:

Fortunately the necessary filesystem mapping (a bind mount or something like that) is already set up by default for the VSCodium flatpak, so I didn't have to set that up.

Comments