Coq: minor refactoring #21879
Coq: minor refactoring #21879
Conversation
| @@ -19,8 +20,8 @@ let | |||
| "8.6" = "1pw1xvy1657l1k69wrb911iqqflzhhp8wwsjvihbgc72r3skqg3f"; | |||
| }."${version}"; | |||
| coq-version = builtins.substring 0 3 version; | |||
| buildIde = lablgtk != null; | |||
| ideFlags = if buildIde then "-lablgtkdir ${lablgtk}/lib/ocaml/*/site-lib/lablgtk2 -coqide opt" else ""; | |||
| camlp5 = ocamlPackages.camlp5_transitional; | |||
There was a problem hiding this comment.
It would have been simpler if ocaml, findlib, lablgtk are defined this way. Then the inherit can be made 1 line, and buildInputs doesn't require the ocamlPackages namespace prefix.
There was a problem hiding this comment.
ic, this is specific to camlp5_transitional. The others should have been casted with (ocamlPackages).
| @@ -16929,13 +16929,8 @@ in | |||
| }; | |||
| coq_8_5 = callPackage ../applications/science/logic/coq { | |||
| version = "8.5pl3"; | |||
| inherit (ocamlPackages) ocaml findlib lablgtk; | |||
There was a problem hiding this comment.
I see, so indeed this makes the all-packages.nix cleaner. If this can be extended to other packages as well?
|
@vbgl |
While this is not in checkbox format, I think this implies nox-review has been run. |
So that Coq libraries that need it can easyly use it
|
@jpierre03 this PR does not change any derivation, it changes how said derivations are defined. There is thus no build to check. |
Motivation for this change
Remove some duplication and ease future maintenance.
Things done
nox-reviewsays: “Nothing changed”.If someone has a better way to compute
coq-version, please share it!