Karl Palmskog (Mar 06 2022 at 11:49): Karl Palmskog (Mar 06 2022 at 11:49):I'm seeing errors like this for plugins with the simple Nix CI workflow on Coq master:
ocamlfind: Cannot mkdir /nix/store/glacvh0889ylw7zpjmr0x6pg33nacmm5-coq-dev/lib/coq/../coq-core//../coq-aac-tactics: Permission denied
Has something changed in the install target? This error indicates that it is not respecting the COQMF_COQLIB option that we pass to tell it where to install the plugin (and it tries instead to install it under the Coq path, which is read-only in Nix store).
Enrico Tassi (Mar 06 2022 at 14:50):it seems the usual findlib bug, I'm working with Cyril on this.
Enrico Tassi (Mar 06 2022 at 14:51):https://github.com/coq-community/coq-nix-toolbox/pull/99#
Last updated: Oct 13 2024 at 01:02 UTC