For Catala to be usable by industrial users, it would be hugely beneficial if its distribution and installation would not entail installing the whole opam toolchain + the C/C++ dependencies : GMP, Z3.
When creating these binaries, I had to use z3.4.8.11 instead of the latest z3.4.8.14 because z3.4.8.13 introduced a breaking change that forbids static linking:
Right now I managed only to compile for x86 ELF because that's what I got on my machine but we would need Windows and ARM/M1 binaries as well, preferably automatically generated through some CI that gets called at each release.
Context
For Catala to be usable by industrial users, it would be hugely beneficial if its distribution and installation would not entail installing the whole
opam
toolchain + the C/C++ dependencies : GMP, Z3.First, as mentionned by https://github.com/CatalaLang/catala/issues/207, it would be good to be able to not include Z3 in the Catala compiler on demand with a custom build profile.
Portable executables
Second, an easy way to distribute the Catala compiler would be as a static, portable executable. @AltGr wrote this excellent tutorial about static binaries compiled from OCaml code: https://www.ocamlpro.com/fr/blog/2021_09_02_generating_static_and_portable_executables_with_ocaml. Following it, I was able to produce portable Linux/ELF x86-64 binaries for Catala and Clerk included in the v0.6.0 release.
First issue: z3 static linking
When creating these binaries, I had to use
z3.4.8.11
instead of the latestz3.4.8.14
becausez3.4.8.13
introduced a breaking change that forbids static linking:https://github.com/ocaml/opam-repository/blob/1fbd9337269c59f74b4046cd9a60efeaa9e52d02/packages/z3/z3.4.8.13/opam#L32-L37
Can we overcome this ? The OCaml API readme in Z3's folder still seems to say that you can statically link https://github.com/Z3Prover/z3/tree/master/src/api/ml
Second issue: cross-compilation
Right now I managed only to compile for x86 ELF because that's what I got on my machine but we would need Windows and ARM/M1 binaries as well, preferably automatically generated through some CI that gets called at each release.