Skip to content

Commit

Permalink
coqPackages.interval: Add bignums, now a required dependency
Browse files Browse the repository at this point in the history
  • Loading branch information
@jwiegley
jwiegley committed Nov 12, 2017
1 parent f7bb8d2 commit 9ea242c
Showing 1 changed file with 2 additions and 2 deletions.
4 changes: 2 additions & 2 deletions pkgs/development/coq-modules/interval/default.nix
View file
@@ -1,4 +1,4 @@
{ stdenv, fetchurl, which, coq, coquelicot, flocq, mathcomp }:
{ stdenv, fetchurl, which, coq, coquelicot, flocq, mathcomp, bignums }:

let param =
if stdenv.lib.versionAtLeast coq.coq-version "8.5"
Expand All @@ -21,7 +21,7 @@ stdenv.mkDerivation {
};

nativeBuildInputs = [ which ];
buildInputs = [ coq ];
buildInputs = [ coq bignums ];
propagatedBuildInputs = [ coquelicot flocq mathcomp ];

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

3 comments on commit 9ea242c

@vbgl
Copy link
Contributor

@vbgl vbgl commented on 9ea242c Nov 13, 2017

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

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
Copy link
Contributor Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

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

@vbgl
Copy link
Contributor

@vbgl vbgl commented on 9ea242c Nov 13, 2017

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

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.