Tidy up the Coq package sets #32737

vbgl · 2017-12-16T11:42:49Z

Motivation for this change

See discussion of #30698.
cc/ @maximedenes @jwiegley @Zimmi48

There are three (3) coqPackages_XX set, one for each version of Coq (8.5, 8.6, 8.7); there are all built from the same function mkCoqPackages.

Before this PR, this sets all have the same attributes but many libraries are not compatible with all these versions of Coq. Therefore, many derivations in these sets are broken: they either fail at evaluation or at build time. It makes difficult to know what are the available libraries in nixpkgs and whether something is broken by mistake or by design.

The goal of this PR is that all attributes evaluate and build. Here is how it is achieved:

Move most Coq-related stuff in a dedicated file pkgs/top-level/coq-packages.nix, available through the coqLib attribute.
Add to most Coq library derivations a meta.compatibleCoqVersions attributes: it is a function from version strings to booleans and tells whether said version is compatible with said library. If this attribute is missing, it means that the library is compatible with all versions (i.e., defaults to _: true).
At the end of the fixed point computation, the (recursive) attribute set coqPackages_XX is filtered to keep only those attributes that are compatible with the corresponding Coq version.

NB: I intended to do the filtering during the fixed point computation, but run into infinite loops. It’s probably not a big deal but I wished I understood what’s going on…

Things done

Tested using sandboxing (nix.useSandbox on NixOS, or option build-use-sandbox in nix.conf on non-NixOS)
Built on platform(s)
- NixOS
- macOS
- other Linux distributions
Tested via one or more NixOS test(s) if existing and applicable for the change (look inside nixos/tests)
Tested compilation of all pkgs that depend on this change using nix-shell -p nox --run "nox-review wip"
Tested execution of all binary files (usually in ./result/bin/)
Fits CONTRIBUTING.md.

Zimmi48 · 2017-12-16T13:32:23Z

This looks good to me. And I've done some testing under NixOS (with sandboxing).

Given that the predicate is applied to the coq-version attribute, I would rather prefer a definition of the form compatibleCoqVersions = v: builtins.elem v [ "8.6" "8.7" ]; that has IMO the advantage of being explicit.

I suppose that what grahamcofborg-eval-check-meta shows is that this information should not be in the meta attribute set.

orivej · 2017-12-16T21:51:50Z

pkgs/top-level/coq-packages.nix

+      let pred =
+        if p ? meta && p.meta ? compatibleCoqVersions
+        then p.meta.compatibleCoqVersions
+        else _: true;


The predicate is equivalent to p ? meta.compatibleCoqVersions, and the whole conditional is equivalent to p.meta.compatibleCoqVersions or (_: true).

Note that compatibleCoqVersions isn't a valid meta attribute. Maybe passthru would be more appropriate?

orivej · 2017-12-16T22:02:55Z

pkgs/top-level/coq-packages.nix

+    };
+
+  filterCoqPackages = coq:
+    lib.filterAttrsRecursive


Is lib.filterAttrs insufficient?

orivej · 2017-12-16T22:18:26Z

pkgs/top-level/all-packages.nix

-  coqPackages_8_7 = mkCoqPackages coqPackages_8_7 coq_8_7;
-  coqPackages = coqPackages_8_6;
-  coq = coqPackages.coq;
+  inherit (coqLib)


May you inherit (callPackage ./coq-packages.nix {}) to avoid confusing naming. (Due to coqLib = ./coq-packages ≠ coqPackages.)

vbgl · 2017-12-17T07:55:42Z

Thanks for the comments. I addressed your concerns in 791776b.

Do you know if there is a way to inherit all attributes from a set? Currently the line inherit (callPackage ./coq-packages.nix {}) …; repeats all the attributes.

jwiegley · 2017-12-17T08:32:40Z

It all looks good to me, though I haven't had the time to try it out yet.

Zimmi48 · 2017-12-17T13:35:29Z

Do you know if there is a way to inherit all attributes from a set? Currently the line inherit (callPackage ./coq-packages.nix {}) …; repeats all the attributes.

Not an answer to this question, but we could also go the same route as ocamlPackages which recently moved from top-level to ocaml-ng, with some aliases kept for compatibility, although I must say that this change confused me until I found where new package sets were hiding.

vbgl · 2017-12-17T18:34:10Z

@Zimmi48 Just above (#32737 (comment)) Orivej suggested not to introduce such an attribute (because of confusing naming).

orivej · 2017-12-17T19:47:18Z

This PR looks ready to merge, but "coqPackages: wip" suggests that the last commit is work in progress, i.e. unfinished. Do you consider it ready?

Do you know if there is a way to inherit all attributes from a set?

There is { one = set; } // another-set, but it is not used in all-packages and there is no equivalent with inherit. IMHO explicit inherit of coq attributes is fine.

vbgl · 2017-12-18T01:43:13Z

I just cleaned the commits and added some documentation. Also I add the library that is used as an example in the docs.

Zimmi48

Kudos for updating the doc!

Zimmi48 · 2017-12-18T10:03:48Z

doc/languages-frameworks/coq.xml

-    generated using <literal>coq_makefile</literal> so we only have to
+    depends on Coq. It builds on the Mathematical Components library, thus it
+    also takes <literal>mathcomp</literal> as <literal>buildInputs</literal>.
+    Its <literal>makefile</literal> has been generated using


Use a capital M here, especially since it is a literal.

Zimmi48 · 2017-12-18T10:06:59Z

doc/languages-frameworks/coq.xml


  buildInputs = [ coq ];
+  propagatedBuildInputs = [ mathcomp ];


Some Coq packages also propagate Coq. Should the rule be not to propagate it? In this case, we should probably update the packages which do not respect this rule.

And how important is it to propagate math-comp? Should Coq package dependencies be always propagated? There are also examples where it is not the case.

I think it should only be propagated if users of that library also (almost always) need to require import from mathcomp. Otherwise, they could specify mathcomp in their own dependencies list, right?

vbgl added the 8.has: clean-up label Dec 16, 2017

vbgl force-pushed the coq-packages-filter branch from 983c2fa to b014c15 Compare December 16, 2017 15:37

orivej reviewed Dec 16, 2017

View reviewed changes

GrahamcOfBorg added 10.rebuild-darwin: 0 10.rebuild-linux: 0 labels Dec 17, 2017

vbgl force-pushed the coq-packages-filter branch from 791776b to 79bebac Compare December 18, 2017 01:30

orivej approved these changes Dec 18, 2017

View reviewed changes

Zimmi48 reviewed Dec 18, 2017

View reviewed changes

vbgl added 4 commits December 18, 2017 15:30

coqPackages: move to a separate file and filter the package set

d9f41a5

coq: minor cleaning

4c454a3

coqPackages: update documentation

5642f4a

coqPackages.multinomials: init at 1.0

fcb89df

vbgl force-pushed the coq-packages-filter branch from 79bebac to fcb89df Compare December 18, 2017 15:31

vbgl merged commit b455192 into NixOS:master Dec 19, 2017

vbgl deleted the coq-packages-filter branch May 22, 2019 09:49

Provide feedback

Saved searches

Use saved searches to filter your results more quickly

Tidy up the Coq package sets #32737

Tidy up the Coq package sets #32737

vbgl commented Dec 16, 2017

Zimmi48 commented Dec 16, 2017

orivej Dec 16, 2017

grahamc Dec 17, 2017

orivej Dec 16, 2017

orivej Dec 16, 2017

vbgl commented Dec 17, 2017

jwiegley commented Dec 17, 2017

Zimmi48 commented Dec 17, 2017

vbgl commented Dec 17, 2017

orivej commented Dec 17, 2017 •

edited

vbgl commented Dec 18, 2017

Zimmi48 left a comment

Zimmi48 Dec 18, 2017

Zimmi48 Dec 18, 2017

jwiegley Dec 18, 2017

Tidy up the Coq package sets #32737

Tidy up the Coq package sets #32737

Conversation

vbgl commented Dec 16, 2017

Motivation for this change

Things done

Zimmi48 commented Dec 16, 2017

orivej Dec 16, 2017

Choose a reason for hiding this comment

grahamc Dec 17, 2017

Choose a reason for hiding this comment

orivej Dec 16, 2017

Choose a reason for hiding this comment

orivej Dec 16, 2017

Choose a reason for hiding this comment

vbgl commented Dec 17, 2017

jwiegley commented Dec 17, 2017

Zimmi48 commented Dec 17, 2017

vbgl commented Dec 17, 2017

orivej commented Dec 17, 2017 • edited

vbgl commented Dec 18, 2017

Zimmi48 left a comment

Choose a reason for hiding this comment

Zimmi48 Dec 18, 2017

Choose a reason for hiding this comment

Zimmi48 Dec 18, 2017

Choose a reason for hiding this comment

jwiegley Dec 18, 2017

Choose a reason for hiding this comment

orivej commented Dec 17, 2017 •

edited