Stream: Coq devs & plugin devs

Topic: Nix and native_compute


view this post on Zulip Karl Palmskog (Oct 17 2020 at 05:06):

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.

view this post on Zulip Théo Zimmermann (Oct 19 2020 at 08:28):

There's even an issue about this: https://github.com/NixOS/nixpkgs/issues/34657

view this post on Zulip Théo Zimmermann (Oct 19 2020 at 08:29):

And a trivial fix that I support, but I haven't cared enough to open a PR. Maybe I should?

view this post on Zulip Karl Palmskog (Oct 19 2020 at 08:57):

if it helps Nix in CI, I'm all for it

view this post on Zulip Karl Palmskog (Oct 19 2020 at 08:58):

in the meantime, I did the dumb fix: https://github.com/coq-community/coqtail-math/pull/1/commits/9038465eeb251a188c8c07e80fccd2bfa9649761

view this post on Zulip Théo Zimmermann (Oct 19 2020 at 09:59):

I opened: https://github.com/NixOS/nixpkgs/pull/101058
A similar PR will be necessary for the version in the Coq repository.

view this post on Zulip Maxime Dénès (Oct 19 2020 at 10:16):

I can confirm there's no fundamental incompatibility between native_compute with a local nix OCaml installation, as it is the setup I use

view this post on Zulip Maxime Dénès (Oct 19 2020 at 10:16):

if some improvements of native_compute could help with the Nix packaging, feel free to open a feature request / PR


Last updated: Oct 21 2021 at 20:02 UTC