Math classes 1.0.7 #30934
Math classes 1.0.7 #30934
Conversation
Bignums used to be part of the standard library of Coq. We provide a version for Coq 8.6, and one for Coq 8.7.
This version introduces compatibility with Coq 8.7.
|
Cc @jwiegley @siddharthist @vbgl @maximedenes. |
| src = fetchFromGitHub { | ||
| owner = "coq"; | ||
| repo = "bignums"; | ||
| inherit rev sha256; |
There was a problem hiding this comment.
Does this build? I don't see rev and sha256 in the parent dictionary.
There was a problem hiding this comment.
Yes it builds, the rev and sha256 are defined in an attribute set above that is imported using with.
There was a problem hiding this comment.
Ah, I see. The indentation is a little strange, it doesn't make it clear that the mkDerivation is a sub-expression of the if-else clause. Not a huge deal, though.
|
@Zimmi48 Thanks! Looking forward to having the new |
| stdenv.mkDerivation { | ||
| name = "coq${coq.coq-version}-math-classes-1.0.6"; | ||
| if ! stdenv.lib.versionAtLeast coq.coq-version "8.6" then | ||
| throw "Math-Classes requires Coq 8.6 or later." |
There was a problem hiding this comment.
Is this true? How difficult is it to keep the old package for 8.5 alive?
There was a problem hiding this comment.
@vbgl There is no package for 8.5 in the sense that the previous package available in nixpkgs was already requiring Coq 8.6 (at least that's what the corresponding OPAM package says, I haven't checked that there was indeed a build failure).
There was a problem hiding this comment.
My bad. You’re right: coqPackages_8_5.math-classes currently fails to build.
Motivation for this change
Introduces compatibility with Coq 8.7.0.
Also adds the bignums package which is a dependency.
Things done
build-use-sandboxinnix.confon non-NixOS)nix-shell -p nox --run "nox-review wip"./result/bin/)