The joys of decoupling: whenever anyone uses native_compute
in a Coq development, Nix CI needs ocaml
and findlib
as explicit dependencies. Otherwise, one gets the following error, which is at least self-explanatory:
Error: The OCaml compiler was not found. Make sure it is installed, together with findlib.
There's even an issue about this: https://github.com/NixOS/nixpkgs/issues/34657
And a trivial fix that I support, but I haven't cared enough to open a PR. Maybe I should?
if it helps Nix in CI, I'm all for it
in the meantime, I did the dumb fix: https://github.com/coq-community/coqtail-math/pull/1/commits/9038465eeb251a188c8c07e80fccd2bfa9649761
I opened: https://github.com/NixOS/nixpkgs/pull/101058
A similar PR will be necessary for the version in the Coq repository.
I can confirm there's no fundamental incompatibility between native_compute
with a local nix OCaml installation, as it is the setup I use
if some improvements of native_compute
could help with the Nix packaging, feel free to open a feature request / PR
Last updated: Oct 13 2024 at 01:02 UTC