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

Using Coq
1

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?

Context

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.

2

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:
Error:
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
3

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.

4

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
5

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.

6

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!