Is it possible to share binary-only libraries across OSes?

Hi everyone,

Is it possible to distribute Coq binaries (.vo) across OSes?

I noticed that Coq complains when I use different versions of Coq and if I use different versions of OCaml. So if I were using the same version of ocamlc and coqc work?

Alternatively, is anyone aware of free CI/CD services for coq and macOS?


I use Coq to teach a couple of courses and one of the main challenges I have are regarding distributing my course-libraries to my students. Distributing the library as source doesn’t work as many students struggle with compiling, since the Coq platform doesn’t make coqc available in the PATH.

It seems that this is not possible, since a version compiled for Windows does not work in Linux using the same combination of compilers:

$ # Coq Platform 22.04.1 for Windows
$ wine /opt/coq/bin/coqc.exe --version
The Coq Proof Assistant, version 8.15.1
compiled with OCaml 4.13.1
$ # Same version compiled for Linux
$ coqc --version
The Coq Proof Assistant, version 8.15.1
compiled with OCaml 4.13.1
$ # Linux version fails
$ coqc -Q Turing Turing Test.v
File "./Test.v", line 1, characters 0-20:
Compiled library Turing.Util (in file /turing/foo/Turing/Util.vo) makes inconsistent assumptions over library Coq.Init.Notations
$ # Windows version passes
$ wine /opt/coq/bin/coqc.exe -Q Turing Turing Test.v

The .vo files contain a checksum of all the OCaml plugins and Coq files they loaded. Since the compilation of a plugin depends on the operating system (e.g., different calling conventions) and since most tactics are provided by a plugin, you will unfortunately never be able to successfully pass the consistency check.

One of the goal of the Coq Platform is to make it easy for teachers to produce custom installers with the libraries they need. You can open a draft PR on the Coq Platform repo, setting the libraries you need instead of the default set, and it will build installers for Windows, macOS and a Snap for Linux. You can also request help on the Coq Platform stream on Zulip. This has already been done multiple times in various contexts (including summer schools for instance).

1 Like

JsCoq could be also be of help to you, the current release is quite usable, tho for more advanced stuff you wanna use our LSP branch.

I wasn’t aware of the PR capability of the Coq Platform project, it seems really interesting and useful.

I will definitely join the Zulip channel. Thanks for the great suggestions!