Ofborg's current output is the problem I'm having with Coq, and I'm not sure what is even happening, so any help is welcome there

cc @vbgl You might have an idea about the Coq-related issue in this PR.

@Synthetica9 If I understand correctly, this allows the scheme name = "ocaml${ocaml.version}-${pname}-${version}" or name = "coq${coq.version}-${pname}-${version}", etc. Correct?

@Synthetica9 If I understand correctly, this allows the scheme name = "ocaml${ocaml.version}-${pname}-${version}" or name = "coq${coq.version}-${pname}-${version}", etc. Correct?

Correct. The current check is whether both pname and version (if the attributes exist) appear in name in their entirety. So any prefix, postfix, whatever is allowed. This was the most forgiving check I could think of that still meant anything, and it found a few genuine problems (see: most of the commits in this PR).

May I suggest that the issue is in your code rather than in the Coq package descriptions? It seems that the checks are run too early.

Please do remove the failing assertions (assert param != null). They break evaluation.

Can we ensure that mkDerivation is lazy? We rely on this property in coqPackages.

Can we ensure that mkDerivation is lazy? We rely on this property in coqPackages.

Only in the places altered in 0ab59bc37b21a13dc35b9d902d78f26af4bb56f2? Because I am currently testing a fix that should fix the issues caused by that. It seems to work fine (testing by compiling coqPackages_8_8)

  param = params."${coq.coq-version}" or null;
in

if param == null then null else
stdenv.mkDerivation rec {

What would be the value of builtins.hasAttr "coqprime" coqPackages_8_5 with your fix? I expect “false”.

@vbgl Everything should be okay now!

Thanks for your understanding. LGTM.

(Rebased to squash some commits, clarify a few messages, and solve merge conflicts)

Currently building on my Hydra (private, so no link, sorry!)

Seems to work fine (ran out of disk space at about 50%, but no errors yet):

@Mic92 Willing to give this another try?

Okay, next order of business is doing refactors in the tree to make packages use this pattern. I think that should go in master, once this PR gets there, am I correct?

Usually. If it actually changes the resulting name it will cause rebuilds though. If the package is high enough in the dpendency tree, that should go to staging. So if ofBorg reports excessive (>100) rebuilds, rebase on staging.

I was thinking of packages that define name = "${pname}-${version}", which shouldn't cause rebuilds at all, right?

Not sure, since the default builder will add pname as an environment variable for the build I think.

nixos-version was failing this check for me--but I might have missed some of the new goodness, and due to strange network problems it's not easy to confidently check against master right now. It's probably been fixed but if not thought I'd mention just in case :).

This pull request has been mentioned on NixOS Discourse. There might be relevant details there:

https://discourse.nixos.org/t/avoid-rec-expresions-in-nixpkgs/8293/4