tjh.dev
nixpkgs mirror (for testing)
github.com/NixOS/nixpkgs
nix
1{
2 coq,
3 mkCoqDerivation,
4 mathcomp-boot,
5 lib,
6 version ? null,
7}:
8
9let
10 derivation = mkCoqDerivation {
11
12 namePrefix = [
13 "coq"
14 "mathcomp"
15 ];
16 pname = "finmap";
17 owner = "math-comp";
18 inherit version;
19 defaultVersion =
20 let
21 case = coq: mc: out: {
22 cases = [
23 coq
24 mc
25 ];
26 inherit out;
27 };
28 in
29 with lib.versions;
30 lib.switch
31 [ coq.coq-version mathcomp-boot.version ]
32 [
33 (case (range "8.20" "9.1") (range "2.3" "2.5") "2.2.2")
34 (case (range "8.20" "9.1") (range "2.3" "2.4") "2.2.0")
35 (case (range "8.16" "9.0") (range "2.0" "2.3") "2.1.0")
36 (case (range "8.16" "8.18") (range "2.0" "2.1") "2.0.0")
37 (case (range "8.13" "8.20") (range "1.12" "1.19") "1.5.2")
38 (case (isGe "8.10") (range "1.11" "1.17") "1.5.1")
39 (case (range "8.7" "8.11") "1.11.0" "1.5.0")
40 (case (isEq "8.11") (range "1.8" "1.10") "1.4.0+coq-8.11")
41 (case (range "8.7" "8.11.0") (range "1.8" "1.10") "1.4.0")
42 (case (range "8.7" "8.11.0") (range "1.8" "1.10") "1.3.4")
43 (case (range "8.7" "8.9") "1.7.0" "1.1.0")
44 (case (range "8.6" "8.7") (range "1.6.1" "1.7") "1.0.0")
45 ]
46 null;
47 release = {
48 "2.2.2".sha256 = "sha256-G5fSdx4MhOXtQ2H8lpyK5FuIbWAZNc7vRL3hcYmGA2o=";
49 "2.2.0".sha256 = "sha256-oDQEZOutrJxmN8FvzovUIhqw0mwc8Ej7thrieJrW8BY=";
50 "2.1.0".sha256 = "sha256-gh0cnhdVDyo+D5zdtxLc10kGKQLQ3ITzHnMC45mCtpY=";
51 "2.0.0".sha256 = "sha256-0Wr1ZUYVuZH74vawO4EZlZ+K3kq+s1xEz/BfzyKj+wk=";
52 "1.5.2".sha256 = "sha256-0KmmSjc2AlUo6BKr9RZ4FjL9wlGISlTGU0X1Eu7l4sw=";
53 "1.5.1".sha256 = "0ryfml4pf1dfya16d8ma80favasmrygvspvb923n06kfw9v986j7";
54 "1.5.0".sha256 = "0vx9n1fi23592b3hv5p5ycy7mxc8qh1y5q05aksfwbzkk5zjkwnq";
55 "1.4.1".sha256 = "0kx4nx24dml1igk0w0qijmw221r5bgxhwhl5qicnxp7ab3c35s8p";
56 "1.4.0+coq-8.11".sha256 = "1fd00ihyx0kzq5fblh9vr8s5mr1kg7p6pk11c4gr8svl1n69ppmb";
57 "1.4.0".sha256 = "0mp82mcmrs424ff1vj3cvd8353r9vcap027h3p0iprr1vkkwjbzd";
58 "1.3.4".sha256 = "0f5a62ljhixy5d7gsnwd66gf054l26k3m79fb8nz40i2mgp6l9ii";
59 "1.2.1".sha256 = "0jryb5dq8js3imbmwrxignlk5zh8gwfb1wr4b1s7jbwz410vp7zf";
60 "1.1.0".sha256 = "05df59v3na8jhpsfp7hq3niam6asgcaipg2wngnzxzqnl86srp2a";
61 "1.0.0".sha256 = "0sah7k9qm8sw17cgd02f0x84hki8vj8kdz7h15i7rmz08rj0whpa";
62 };
63
64 propagatedBuildInputs = [ mathcomp-boot ];
65
66 meta = {
67 description = "Finset and finmap library";
68 license = lib.licenses.cecill-b;
69 };
70 };
71in
72# this is just a wrapper for rocqPackages.mathcomp-finmap for Rocq >= 9.0
73if coq.rocqPackages ? mathcomp-finmap then
74 coq.rocqPackages.mathcomp-finmap.override {
75 inherit version mathcomp-boot;
76 inherit (coq.rocqPackages) rocq-core;
77 }
78else
79 derivation