tjh.dev
nixpkgs mirror (for testing)
github.com/NixOS/nixpkgs
nix
1{
2 lib,
3 mkCoqDerivation,
4 autoconf,
5 coq,
6 coquelicot,
7 flocq,
8 mathcomp-boot,
9 mathcomp-fingroup,
10 bignums ? null,
11 gnuplot_qt,
12 version ? null,
13}:
14
15mkCoqDerivation rec {
16 pname = "interval";
17 owner = "coqinterval";
18 domain = "gitlab.inria.fr";
19 inherit version;
20 defaultVersion =
21 let
22 case = case: out: { inherit case out; };
23 in
24 with lib.versions;
25 lib.switch coq.coq-version [
26 (case (range "8.13" "9.1") "4.11.3")
27 (case (range "8.13" "9.0") "4.11.2")
28 (case (range "8.13" "8.20") "4.11.1")
29 (case (range "8.12" "8.19") "4.10.0")
30 (case (range "8.12" "8.18") "4.9.0")
31 (case (range "8.12" "8.17") "4.8.0")
32 (case (range "8.12" "8.16") "4.6.0")
33 (case (range "8.8" "8.16") "4.5.2")
34 (case (range "8.8" "8.12") "4.0.0")
35 (case (range "8.7" "8.11") "3.4.2")
36 (case (range "8.5" "8.6") "3.3.0")
37 ] null;
38 release."4.11.3".sha256 = "sha256-Cwovc3ln7ZEEDgMEh+pSUYqD/rtwFk4ED2hTRdy9YRg";
39 release."4.11.2".sha256 = "sha256-ouhjHtlxcqt06+Pt+UZAzwp83bVYPh3N+8jnsVvapSU=";
40 release."4.11.1".sha256 = "sha256-QWZvU468rOhK796xCCEawW6rhCRTPnE0iLll9ynKflo=";
41 release."4.11.0".sha256 = "sha256-vPwa4zSjyvxHLGDoNaBnHV2pb77dnQFbC50BL80fcvE=";
42 release."4.10.0".sha256 = "sha256-MZJVoKGLXjDabdv9BuUSK1L9z1cubzC9cqVuWevKIXQ=";
43 release."4.9.0".sha256 = "sha256-+5NppyQahcc1idGu/U3B+EIWuZz2L3/oY7dIJR6pitE=";
44 release."4.8.1".sha256 = "sha256-gknZ3bA90YY2AvwfFsP5iMhohwkQ8G96mH+4st2RPDc=";
45 release."4.8.0".sha256 = "sha256-YPQ1tuUgGixAVdQUJ9a3lZUNVgm2pKK3RKvl3m+/8rY=";
46 release."4.7.0".sha256 = "sha256-Cel25w4BeaNqu9KAW3N2KYO2IGY0EOAK5FQ6VHBPmFQ=";
47 release."4.6.1".sha256 = "sha256-ZZSxt8ksz0g6dl/LEido5qJXgsaxHrVLqkGUHu90+e0=";
48 release."4.6.0".sha256 = "sha256-n9ECKnV0L6XYcIcbYyOJKwlbisz/RRbNW5YESHo07X0=";
49 release."4.5.2".sha256 = "sha256-r0yE9pkC4EYlqsimxkdlCXevRcwKa3HGFZiUH+ueUY8=";
50 release."4.5.1".sha256 = "sha256-5OxbSPdw/1FFENubulKSk6fEIEYSPCxfvMMgtgN6j6s=";
51 release."4.3.0".sha256 = "sha256-k8DLC4HYYpHeEEgXUafS8jkaECqlM+/CoYaInmUTYko=";
52 release."4.2.0".sha256 = "sha256-SD5thgpirs3wmZBICjXGpoefg9AAXyExb5t8tz3iZhE=";
53 release."4.1.1".sha256 = "sha256-h2NJ6sZt1C/88v7W2xyuftEDoyRt3H6kqm5g2hc1aoU=";
54 release."4.0.0".sha256 = "1hhih6zmid610l6c8z3x4yzdzw9jniyjiknd1vpkyb2rxvqm3gzp";
55 release."3.4.2".sha256 = "07ngix32qarl3pjnm9d0vqc9fdrgm08gy7zp306hwxjyq7h1v7z0";
56 release."3.3.0".sha256 = "0lz2hgggzn4cvklvm8rpaxvwaryf37i8mzqajqgdxdbd8f12acsz";
57 releaseRev = v: "interval-${v}";
58
59 nativeBuildInputs = [ autoconf ];
60 propagatedBuildInputs =
61 lib.optional (lib.versions.isGe "8.6" coq.coq-version) bignums
62 ++ [
63 coquelicot
64 flocq
65 mathcomp-boot
66 mathcomp-fingroup
67 ]
68 ++ lib.optionals (lib.versions.isGe "4.2.0" defaultVersion) [ gnuplot_qt ];
69 useMelquiondRemake.logpath = "Interval";
70 mlPlugin = true;
71
72 meta = {
73 description = "Tactics for simplifying the proofs of inequalities on expressions of real numbers for the Coq proof assistant";
74 license = lib.licenses.cecill-c;
75 maintainers = with lib.maintainers; [ vbgl ];
76 };
77}