Thanks. Evaluation errors are indeed much better that build failures.

However, there should be a clean mechanism to properly declare what packages are available for which versions of Coq. Here is a rough suggestion.

Each Coq package comes with a meta.compatibleCoqVersions attribute (name subject to bike-shedding) which is a function (defaults to _: true) which takes as argument a version of Coq and returns whether this package is compatible with said version of Coq.

Then the result of mkCoqPackages is filtered (as in lib.filterAttrsRecursive) to keep only compatible packages.

Any thoughts?

Indeed, I think this is a much better approach. I'll give it a try. Meanwhile, I think this patch should be merged. Is that ok with you, @jwiegley ? I'll open a similar PR on coqPackages.QuickChick.

Can you rename the subject of the issue and the commit message to: "coqPackages.dpdgraph: remove support for coq 8.7"? Otherwise, if upstream doesn't support 8.7, I don't see any reason to not commit this.

I only added dpdgraph so that it would evaluate, thinking we could subsequently fix the build error. There are packages in all the other Coq versions that evaluate but don't build as well.

@jwiegley Indeed, many coq packages are broken (as in evaluate but don't build), and I think a clean up would be good, so I'd like to try the approach suggested by @vbgl.

Meanwhile, this PR can either be merged to avoid a build failure, or be closed to wait for a more general clean up of coqPackages. I'm personally fine either way.

I think we should merge to make parts of 8.7 available, and then consider how we will do it right. coqPackages has felt ad hoc since the beginning, and I only made it worse by continuing that approach. It's time for a redo.

It's been some time since I've wanted to document coqPackages in more details but if it's about to be redesigned, I'd better wait that this happens before.

There's something specific to Coq packages which isn't there for most languages AFAIK which is that we have lots of plugins which are very dependent on the version of Coq, and most of them do not try to provide a Makefile which would switch implementations based on which version of Coq is used but instead they provide several releases / branches. Library authors, on the contrary are encouraged to support several releases at once and generally do so.

If I understand @vbgl's suggestion correctly, the goal is to use this function when building the coqPackages_8_x set to only put the packages which have a corresponding version. That would be ideal indeed. A less perfect but good-enough solution would be to throw a clear evaluation error as early as possible as I did there: https://github.com/Zimmi48/nixpkgs/blob/coq-8-7/pkgs/development/coq-modules/bignums/default.nix (that's a derivation that I didn't submitted because I understand that @maximedenes has prepared something similar).

I would rather filter the set of available packages during the fixpoint computation (i.e. in the definition of mkCoqPackages).

Concerning your example, Théo, you can use a single lookup in an attribute-set instead of a long chain of if-then-else with equality checks. You can use the ? operator to check whether a set has a particular attribute to throw an appropriate error message. That being said, resorting to evaluation errors does not appear to me as a good solution; in particular it is difficult to (automatically) distinguish between errors that are there by design from simple mistakes.

We could also think about generating the packages from the Coq Package Index, rather than having an ad-hoc collection, btw: https://coq.inria.fr/packages

@vbgl Thanks for the comments.

@maximedenes

We could also think about generating the packages from the Coq Package Index, rather than having an ad-hoc collection, btw: https://coq.inria.fr/packages

Indeed, and this is something that is done for some other languages (e.g. Haskell from Stack I think, or Emacs from MELPA) and we can even adapt the way the meta data is stored if it helps.

Shouldn't we open a new issue to track this?