pyrox.dev
lol
1{
2 lib,
3 mkCoqDerivation,
4 coq,
5 mathcomp,
6 stdlib,
7 version ? null,
8}:
9
10mkCoqDerivation {
11 pname = "gaia";
12
13 release."1.11".sha256 = "sha256:0gwb0blf37sv9gb0qpn34dab71zdcx7jsnqm3j9p58qw65cgsqn5";
14 release."1.12".sha256 = "sha256:0c6cim4x6f9944g8v0cp0lxs244lrhb04ms4y2s6y1wh321zj5mi";
15 release."1.13".sha256 = "sha256:0i8ix2rbw10v34bi0yrx0z89ng96ydqbxm8rv2rnfgy4d1b27x6q";
16 release."1.14".sha256 = "sha256-wgeQC0fIN3PSmRY1K6/KTy+rJmqqxdo3Bhsz1vjVAes=";
17 release."1.15".sha256 = "sha256:04zchnkvaq2mzpcilpspn5l947689gj3m0w20m0nd7w4drvlahnw";
18 release."1.17".sha256 = "sha256-2VzdopXgKS/wC5Rd1/Zlr12J5bSIGINFjG1nrMjDrGE=";
19 release."2.2".sha256 = "sha256-y8LlQg9d9rfPFjzS9Xu3BW/H3tPiOC+Eb/zwXJGW9d4=";
20 release."2.3".sha256 = "sha256-inWJok0F3SZpVfoyMfpRXHVHn4z2aY8JjCKKhdVTnoc=";
21 releaseRev = (v: "v${v}");
22
23 inherit version;
24 defaultVersion =
25 let
26 case = coq: mc: out: {
27 cases = [
28 coq
29 mc
30 ];
31 inherit out;
32 };
33 in
34 with lib.versions;
35 lib.switch
36 [ coq.coq-version mathcomp.version ]
37 [
38 (case (range "8.16" "9.1") (range "2.0" "2.4") "2.3")
39 (case (range "8.16" "9.0") (range "2.0" "2.3") "2.2")
40 (case (range "8.10" "8.18") (range "1.12.0" "1.18.0") "1.17")
41 (case (range "8.10" "8.12") "1.11.0" "1.11")
42 ]
43 null;
44
45 propagatedBuildInputs = [
46 mathcomp.boot
47 mathcomp.fingroup
48 mathcomp.algebra
49 stdlib
50 ];
51
52 meta = with lib; {
53 description = "Implementation of books from Bourbaki's Elements of Mathematics in Coq";
54 maintainers = with maintainers; [ Zimmi48 ];
55 license = licenses.mit;
56 };
57}