Stream: Nix toolbox devs & users

Topic: Adding ${coq}/lib/coq as a dependency in a derivation

Stefan Malewski (Jan 05 2022 at 20:04):

I'm trying to compile metacoq, which has an ocaml plugin, using nix. I was having some troubles; it appears thatmkCoqDerivation is not putting COQLIB in the environment. Compilation works fine if I explicitly export it before the compilation phase. Shouldn't COQLIB be automatically put in scope, at least when mlPlugin is set?

Théo Zimmermann (Jan 06 2022 at 09:56):

This goes beyond my expertise. Deferring to @Enrico Tassi and @Cyril Cohen.

Stefan Malewski (Jan 07 2022 at 16:07):

I think I failed my communication's roll, will try again (changed the title, also):
I'm trying to build a package that depends on coq sources in ${coq}/lib/coq. The problem is that adding coq to extraBuildInputs doesn't put that in the path. I guess that makes some sense since coq is a program.
A workaround is to explicitly set the COQLIB environment variable to the library's path.
My question is, shouldn't it makes sense to add ${coq}/lib/coq to the path sometimes? For example when making a plugin.
Or maybe is there an easy way of adding that dependency that I'm missing.

Cyril Cohen (Jan 07 2022 at 22:34):

You can simply add COQLIB = "${coq}/lib/coq" to your derivation, no need to add it upstream.

Cyril Cohen (Jan 07 2022 at 22:37):

can you share your nix file?

Cyril Cohen (Jan 07 2022 at 22:39):

(However, I'm not completely sure why you would need that...)

Stefan Malewski (Jan 11 2022 at 02:58):

Sure, here they are: https://github.com/smalewski/dotfiles/tree/master/derivations
The metacoqfolder has a derivation for MetaCoq 8.14 and it works fine.
The one that needed COQLIB is in template-coq-rewrite which is the artifact for the paper 'The taming of the rew: a type theory with computational assumptions'.

Cyril Cohen (Jan 11 2022 at 12:24):

So it worked, right?

Kenji Maillard (Jan 11 2022 at 17:50):

I think it worked fine, but wouldn't that problem (setting COQLIB) appear for almost any ml plugin for coq since it needs to have access to the internals of coq ?

Théo Zimmermann (Jan 12 2022 at 10:18):

Something that really puzzles me is that I had no idea that the COQLIB environment variable could have any relation with OCaml libraries. I went to look at the documentation, and it seems to me that this environment variable is virtually undocumented. From past work https://github.com/NixOS/nixpkgs/pull/136908 based on past discussions with @Enrico Tassi and @Vincent Laporte, it even seemed to me that this was mostly an internal variable (though maybe not in all cases).

Cyril Cohen (Jan 12 2022 at 16:06):

To my knowledge coqc -where is the "standard" way of getting access to the right directory, setting it through the nix derivation does not bring extra knowledge, nor does require the compilation of more stuff than needed. That's why I would not set it in the general mkCoqDerivation.

Kenji Maillard (Jan 14 2022 at 16:16):

These are good points, I don't understand yet why COQLIB should be set in order to get a working nix derivation for MetaCoq, but it might be some quirk of MetaCoq setup.

Last updated: Oct 13 2024 at 01:02 UTC