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:
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:
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:
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.
The Haskell Language Server Client is a project, slowly chugging along since 2016, which aims to add Haskell IDE-like support to Visual Studio Code (VSCode), Microsoft's open source text-editor-cum-IDE.
Anyway, back to the Haskell Language Server Client. It relies upon the Haskell IDE Engine (HIE) – which is in the process of merging with the GHCIDE project to form the Haskell Language Server. HIE/HLS looks like it might become the new standard backend for next-generation Haskell IDE implementations. HIE is effectively a user service/daemon which examines Haskell projects and exposes a dynamic view of them via a cross-language, industry open standard called Language Server Protocol (LSP) for IDE and text editor plugins to use, and is already used by a bunch of IDE and text editor plugins in addition to the VSCode one. This should be good news for Haskell IDE efforts – of which there have been many over the years – as at least the backend work for those that choose to use HIE should be centralised in one project (HIE), avoiding needless duplication of effort.
Running HIE under Flatpak
I wanted to try it out on Linux, but VSCode is not available in the official Fedora Linux package repositories, so I chose to install it using flatpak instead, as suggested on the Fedora wiki:
Unfortunately, my Linux VM ran out of disk space on its home partition when trying to install it. And even after re-running the install command above again, the disk full problem had seemingly caused flatpak to corrupt the install of VSCode or one of its dependencies, so I then had to force-reinstall it:
Running it (on Qubes, a highly-secure hypervisor/meta-OS for my desktop Fedora VMs which doesn't provide a desktop for each VM but rather a unified desktop for all of them) was a bit tricky, but this turned out to be the necessary incantation:
flatpak run --user --branch=stable com.visualstudio.code.oss
However, after installing the extension, initially, the extension didn't work, as it wasn't able to start HIE, even though I had followed the instructions and successfully installed HIE first.
The reason why soon became apparent. Flatpaks are run in a containerised environment – a bit like Docker for Linux desktop applications – and although the default permissions for the VSCode flatpak are quite permissive, it's still not quite like running VSCode directly on the host system, i.e. in a non-containerised way.
In particular, launching a terminal from VSCode doesn't work as you might expect, because by default none of the software installed on the host system is on the PATH, only VSCode itself and whatever basic command-line tools the flatpak maintainer has made available within the container. However, launching a terminal from within VSCode was a good way to see more clearly what was going on within the container.
The solution turned out to be relatively straightforward. I used a combination of the two techniques from this StackExchange answer. The extension already had a way to set a custom wrapper script for starting HIE in its preferences, so I created such a wrapper script which invoked the flatpak-spawn command to escape from the flatpak container to run the copy of hie that stack had installed at ~/.local/bin/hie:
and saved it (as root) as /usr/local/bin/hie-wrapper and marked it as executable (sudo chmod a+x /usr/local/bin/hie-wrapper). I could have equally well saved it under my home directory, I just chose to do it this way.
The --env=BASH_ENV=~/.bashrc part forces bash to reload .bashrc, so that the PATH variable will be set correctly and therefore the correct (newer) version of stack will be found on the PATH. I actually have two versions of stack installed – one in /usr/bin which was installed from a system package, which is too old to build some projects, and one in ~/.local/bin, which was installed manually. 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 wrapper script path to the path that this file is visible from:
Fortunately the necessary filesystem mapping (a bind mount or something like that) is already set up by default for the VSCode flatpak, so I didn't have to set that up.
Bought myself a nice 5.1 speaker system a few months ago – so I don’t use our tinny crappy old computer speakers any more, yay! But the irony is, I usually just plug my Nexus 7 into it (using the bog standard noisey stereo input, instead of the higher quality digital input cable) to play music from Spotify!
That’s because, while Spotify is available for Linux, it’s only officially supported at the moment on Android, and it’s been a bit of a pain to install on Fedora Linux / QubesOS – there are two community-created install methods, one of which is currently known to be broken, and neither of which worked for me the last time I tried them.
I only use Skype on my Nexus too, for a similar reason. Skype on Linux is behind – it doesn’t support group calls. Microsoft, who acquired Skype Technologies in 2011, have said they are working on it. Microsoft? Working on commercial software for desktop Linux? That’s a new one on me!
But the irony is, both Fedora and Android are Linux!
Well, they’re Linux underneath – the operating system infrastructure on top of the Linux kernel, and how developers typically write applications, is quite different in each. There are now two main branches of Linux in the wild: desktop/server Linux, which is further subdivided into numerous distributions, and Android. “Server Linux” is conceptually just Desktop Linux with bits removed (and/or left unused) – it’s not really a separate thing, except for marketing purposes. There’s also a couple more branches of Linux which have just started to appear in the mobile market: Firefox OS and Sailfish OS; and two more nascent ones which haven’t been commercially released on real devices yet: Ubuntu Touch and Tizen.
In terms of open source, my sense is that desktop Linux and Firefox OS are the most open, and Tizen (if it ever gets properly released), followed by Sailfish OS, will be the least open, with Android somewhere in the middle in practice, although I may be wrong on that. I’m talking about the platforms here, not third-party apps – the open source application ecosystem seems to me to be far stronger on desktop and server Linux than on Android.
One of these is not like the others, though! Ubuntu Touch is an attempt to bring Ubuntu to mobile platforms – a bit like Microsoft’s ideas of platform convergence that it tried to force onto its users (not entirely successfully!) with Windows 8 – so it’s not a clean break like the other mobile operating systems.1
Also, Firefox OS is pushing the concept of HTML5 apps – although these can also be downloaded like regular mobile apps, so it’s not completely clear to me where Firefox OS really stands in the convergence spectrum.2
Finally – and perhaps most importantly – as I posted about yesterday on Google+, Google has said that Chromebooks will get the ability to run Android apps3 by the end of this year – and Chromium OS, on which Chrome OS is closely based, is open source. So hopefully that ability will appear in Chromium OS, and then be ported to other Linux distributions – solving my Skype and Spotify dilemma.
The music industry probably won’t be bothered, as they’ve already agreed that Spotify users on tablets can have the same rights to stream music as Spotify on desktops – unlike Spotify users on mobile phones.4
But goodness knows what Microsoft will make of that! Wailing and gnashing of teeth, probably!
Sailfish also runs Android apps, but since they’re both mobile platforms at the moment, that’s not as interesting or impressive to me as the idea of Ubuntu Touch.↩︎
Sailfish also pushes HTML5, although not to the extent that Firefox OS does.↩︎
Presumably, this means without using an Android emulator – which is slow, as far as I know.↩︎
But how do phablets fit into Spotify’s streaming licensing scheme? We simply must be told!↩︎