Skip to content

Commit 9ea242c

Browse files
jwiegleyjwiegley
committedNov 12, 2017
coqPackages.interval: Add bignums, now a required dependency
·
branch-off-24.1118.03-beta
1 parent f7bb8d2 commit 9ea242c

File tree

1 file changed

+2
-2
lines changed

1 file changed

+2
-2
lines changed
 

‎pkgs/development/coq-modules/interval/default.nix

+2-2
Original file line numberDiff line numberDiff line change
@@ -1,4 +1,4 @@
1-
{ stdenv, fetchurl, which, coq, coquelicot, flocq, mathcomp }:
1+
{ stdenv, fetchurl, which, coq, coquelicot, flocq, mathcomp, bignums }:
22

33
let param =
44
if stdenv.lib.versionAtLeast coq.coq-version "8.5"
@@ -21,7 +21,7 @@ stdenv.mkDerivation {
2121
};
2222

2323
nativeBuildInputs = [ which ];
24-
buildInputs = [ coq ];
24+
buildInputs = [ coq bignums ];
2525
propagatedBuildInputs = [ coquelicot flocq mathcomp ];
2626

2727
configurePhase = "./configure --libdir=$out/lib/coq/${coq.coq-version}/user-contrib/Interval";

3 commit comments

Comments
 (3)

vbgl commented on Nov 13, 2017

@vbgl
vbgl
on Nov 13, 2017
Contributor

This does not properly fix coqPackages_8_7.interval:

$ coqtop
Welcome to Coq 8.7.0 (November 2017)

Coq < From Interval Require Import Interval_tactic.
Toplevel input, characters 0-45:
> From Interval Require Import Interval_tactic.
> ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
Error:
Cannot load Bignums.SpecViaZ.NSig: no physical path bound to Bignums.SpecViaZ

The bignum library should be propagated.

It works with Coq 8.6.1; by accident I guess.

This breaks coqPackages_8_5.interval:

error: bignums is not available for Coq 8.5

This breaks coqPackages_8_4.interval:

error: anonymous function at …/pkgs/development/coq-modules/interval/default.nix:1:1 called without required argument ‘bignums’, at …/lib/customisation.nix:74:12

jwiegley commented on Nov 13, 2017

@jwiegley
jwiegley
on Nov 13, 2017
ContributorAuthor

Thanks for catching this @vbgl, I'll work on a fix today.

vbgl commented on Nov 13, 2017

@vbgl
vbgl
on Nov 13, 2017
Contributor

I think these issues have been addressed by 985cfa7 and d7e8415.

Going through a pull-request is a good way to avoid pushing breaking commits to master.

Please sign in to comment.