@vbgl @Zimmi48 What do you think would be the right approach?

I would suggest to remove the ad-hoc coqPackages_8_4 (the next versions are more generic and better factorized). Coq 8.4 has been unsupported for nearly two years.

In a second step, I can try to convert the OPAM packages found in the Coq Package Index to Nix in a more systematic way.

Of course, I'm fine with any other approach, but it would be good to make sure it is going to scale and lead to some stability.

Let me just say that I find such a quick merge of a PR rude to say the least. Then I will add that I am completely puzzled to see that the Coq sub-community of Nix is so tightly attached to totally outdated and unsupported versions whereas the rest of the community tries to have only one version of a given package unless there is a good reason to. That math-comp maintainers decided to drop support for 8.4 should be telling you something on how it's time to move on. Personally I vote for the full removal of coqPackages_8_4.

I merged the original PR because things looked good and reverted to avoid build failures.

Let's just remove Coq 8.3 and 8.4... Then we can bring back the updated packages.

Note that there does seem to be something called verasco that depends on Coq 8.4

It was ok to revert my PR while we figure out what should be done, as it was indeed introducing more build failures than there is already.

Let's just remove Coq 8.3 and 8.4... Then we can bring back the updated packages.

+1

Note that there does seem to be something called verasco that depends on Coq 8.4

Yes, but I believe verasco is not maintained anymore. @vbgl can say more as he is one of the authors. I expect other unmaintained packages will have to go away at the same time.

If somebody wants to do that, go right ahead. I don't do any Coq usually, so I won't...

Yep, I'll take care of that this week and submit a PR.