tjh.dev
nixpkgs mirror (for testing)
github.com/NixOS/nixpkgs
nix
1{
2 lib,
3 coq,
4 mkCoqDerivation,
5 mathcomp-character,
6 version ? null,
7}:
8
9mkCoqDerivation {
10 pname = "odd-order";
11 owner = "math-comp";
12
13 release."2.3.0".sha256 = "sha256-53FG8I9O+tsIlmaa9qy6VYyJNwWfGmhavKhbZ0VqAGc=";
14 release."2.2.0".sha256 = "sha256-z0C7+wtY8NpoT8wYqHiy8mB2HPYAeJndzDmf7Bb0mg8=";
15 release."2.1.0".sha256 = "sha256-TPlaQbO0yXEpUgy3rlCx/w1MSLECJk5tdU26fAGe48Q=";
16 release."1.14.0".sha256 = "0iln70npkvixqyz469l6nry545a15jlaix532i1l7pzfkqqn6v68";
17 release."1.13.0".sha256 = "sha256-EzNKR/JzM8T17sMhPhgZNs14e50X4dY3OwFi133IsT0=";
18 release."1.12.0".sha256 = "sha256-omsfdc294CxKAHNMMeqJCcVimvyRCHgxcQ4NJOWSfNM=";
19 releaseRev = v: "mathcomp-odd-order.${v}";
20
21 inherit version;
22 defaultVersion =
23 let
24 case = coq: mc: out: {
25 cases = [
26 coq
27 mc
28 ];
29 inherit out;
30 };
31 in
32 with lib.versions;
33 lib.switch
34 [ coq.coq-version mathcomp-character.version ]
35 [
36 (case (range "9.0" "9.1") (range "2.5" "2.5") "2.3.0")
37 (case (range "8.16" "9.1") (range "2.2.0" "2.4.0") "2.2.0")
38 (case (range "8.16" "9.0") (range "2.1.0" "2.3.0") "2.1.0")
39 (case (range "8.11" "8.16") (range "1.13.0" "1.15.0") "1.14.0")
40 (case (range "8.10" "8.15") (range "1.12.0" "1.14.0") "1.13.0")
41 (case (range "8.10" "8.14") (range "1.10.0" "1.12.0") "1.12.0")
42 ]
43 null;
44
45 propagatedBuildInputs = [
46 mathcomp-character
47 ];
48
49 meta = {
50 description = "Formal proof of the Odd Order Theorem";
51 maintainers = with lib.maintainers; [ siraben ];
52 license = lib.licenses.cecill-b;
53 platforms = lib.platforms.unix;
54 };
55}