tjh.dev
nixpkgs mirror (for testing)
github.com/NixOS/nixpkgs
nix
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.5") "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 = {
53 description = "Implementation of books from Bourbaki's Elements of Mathematics in Coq";
54 maintainers = with lib.maintainers; [ Zimmi48 ];
55 license = lib.licenses.mit;
56 };
57}