tjh.dev
Clone of https://github.com/NixOS/nixpkgs.git (to stress-test knotserver)
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.0") "4.11.2")
27 (case (range "8.13" "8.20") "4.11.1")
28 (case (range "8.12" "8.19") "4.10.0")
29 (case (range "8.12" "8.18") "4.9.0")
30 (case (range "8.12" "8.17") "4.8.0")
31 (case (range "8.12" "8.16") "4.6.0")
32 (case (range "8.8" "8.16") "4.5.2")
33 (case (range "8.8" "8.12") "4.0.0")
34 (case (range "8.7" "8.11") "3.4.2")
35 (case (range "8.5" "8.6") "3.3.0")
36 ] null;
37 release."4.11.2".sha256 = "sha256-ouhjHtlxcqt06+Pt+UZAzwp83bVYPh3N+8jnsVvapSU=";
38 release."4.11.1".sha256 = "sha256-QWZvU468rOhK796xCCEawW6rhCRTPnE0iLll9ynKflo=";
39 release."4.11.0".sha256 = "sha256-vPwa4zSjyvxHLGDoNaBnHV2pb77dnQFbC50BL80fcvE=";
40 release."4.10.0".sha256 = "sha256-MZJVoKGLXjDabdv9BuUSK1L9z1cubzC9cqVuWevKIXQ=";
41 release."4.9.0".sha256 = "sha256-+5NppyQahcc1idGu/U3B+EIWuZz2L3/oY7dIJR6pitE=";
42 release."4.8.1".sha256 = "sha256-gknZ3bA90YY2AvwfFsP5iMhohwkQ8G96mH+4st2RPDc=";
43 release."4.8.0".sha256 = "sha256-YPQ1tuUgGixAVdQUJ9a3lZUNVgm2pKK3RKvl3m+/8rY=";
44 release."4.7.0".sha256 = "sha256-Cel25w4BeaNqu9KAW3N2KYO2IGY0EOAK5FQ6VHBPmFQ=";
45 release."4.6.1".sha256 = "sha256-ZZSxt8ksz0g6dl/LEido5qJXgsaxHrVLqkGUHu90+e0=";
46 release."4.6.0".sha256 = "sha256-n9ECKnV0L6XYcIcbYyOJKwlbisz/RRbNW5YESHo07X0=";
47 release."4.5.2".sha256 = "sha256-r0yE9pkC4EYlqsimxkdlCXevRcwKa3HGFZiUH+ueUY8=";
48 release."4.5.1".sha256 = "sha256-5OxbSPdw/1FFENubulKSk6fEIEYSPCxfvMMgtgN6j6s=";
49 release."4.3.0".sha256 = "sha256-k8DLC4HYYpHeEEgXUafS8jkaECqlM+/CoYaInmUTYko=";
50 release."4.2.0".sha256 = "sha256-SD5thgpirs3wmZBICjXGpoefg9AAXyExb5t8tz3iZhE=";
51 release."4.1.1".sha256 = "sha256-h2NJ6sZt1C/88v7W2xyuftEDoyRt3H6kqm5g2hc1aoU=";
52 release."4.0.0".sha256 = "1hhih6zmid610l6c8z3x4yzdzw9jniyjiknd1vpkyb2rxvqm3gzp";
53 release."3.4.2".sha256 = "07ngix32qarl3pjnm9d0vqc9fdrgm08gy7zp306hwxjyq7h1v7z0";
54 release."3.3.0".sha256 = "0lz2hgggzn4cvklvm8rpaxvwaryf37i8mzqajqgdxdbd8f12acsz";
55 releaseRev = v: "interval-${v}";
56
57 nativeBuildInputs = [ autoconf ];
58 propagatedBuildInputs =
59 lib.optional (lib.versions.isGe "8.6" coq.coq-version) bignums
60 ++ [
61 coquelicot
62 flocq
63 mathcomp-boot
64 mathcomp-fingroup
65 ]
66 ++ lib.optionals (lib.versions.isGe "4.2.0" defaultVersion) [ gnuplot_qt ];
67 useMelquiondRemake.logpath = "Interval";
68 mlPlugin = true;
69 enableParallelBuilding = true;
70
71 meta = with lib; {
72 description = "Tactics for simplifying the proofs of inequalities on expressions of real numbers for the Coq proof assistant";
73 license = licenses.cecill-c;
74 maintainers = with maintainers; [ vbgl ];
75 };
76}