tjh.dev
nixpkgs mirror (for testing)
github.com/NixOS/nixpkgs
nix
1{
2 lib,
3 mkCoqDerivation,
4 coq,
5 version ? null,
6 equations,
7 mathcomp-boot,
8 mathcomp-analysis,
9 mathcomp-experimental-reals,
10 extructures,
11 deriving,
12 mathcomp-word,
13}:
14
15(mkCoqDerivation {
16 pname = "ssprove";
17 owner = "SSProve";
18
19 inherit version;
20 defaultVersion =
21 let
22 case = coq: mc: out: {
23 cases = [
24 coq
25 mc
26 ];
27 inherit out;
28 };
29 in
30 with lib.versions;
31 lib.switch
32 [ coq.coq-version mathcomp-boot.version ]
33 [
34 (case (range "8.20" "9.1") (range "2.3.0" "2.5.0") "0.3.0")
35 (case (range "8.18" "9.1") (range "2.3.0" "2.4.0") "0.2.4")
36 (case (range "8.18" "8.20") (range "2.3.0" "2.3.0") "0.2.3")
37 (case (range "8.18" "8.20") (range "2.1.0" "2.2.0") "0.2.2")
38 # This is the original dependency:
39 # (case "8.17" "1.18.0" "0.1.0")
40 # But it is not loadable. The math-comp nixpkgs configuration
41 # will always only output version 1.18.0 for Coq 8.17.
42 # Hence, the Coq 8.17 and math-comp 1.17.0 must be explicitly set
43 # to load it.
44 # (This version is not on the math-comp CI and hence not checked.)
45 (case "8.17" "1.17.0" "0.1.0")
46 ]
47 null;
48
49 releaseRev = v: "v${v}";
50
51 release."0.3.0".sha256 = "sha256-ioPqavLOc8ZEzroalLR4dpqDbnOyzzOmWSF9+J1yPdQ=";
52 release."0.2.4".sha256 = "sha256-uglr47aDgSkKi2JyVyN+2BrokZISZUAE8OUylGjy7ds=";
53 release."0.2.3".sha256 = "sha256-Y3dmNIF36IuIgrVILteofOv8e5awKfq93S4YN7enswI=";
54 release."0.2.2".sha256 = "sha256-tBF8equJd6hKZojpe+v9h6Tg9xEnMTVFgOYK7ZnMfxk=";
55 release."0.2.1".sha256 = "sha256-X00q5QFxdcGWeNqOV/PLTOqQyyfqFEinbGUTO7q8bC4=";
56 release."0.2.0".sha256 = "sha256-GDkWH0LUsW165vAUoYC5of9ndr0MbfBtmrPhsJVXi3o=";
57 release."0.1.0".sha256 = "sha256-Yj+k+mBsudi3d6bRVlZLyM4UqQnzAX5tHvxtKoIuNTE=";
58
59 propagatedBuildInputs = [
60 equations
61 mathcomp-boot
62 mathcomp-analysis
63 mathcomp-experimental-reals
64 extructures
65 deriving
66 mathcomp-word
67 ];
68
69 meta = {
70 description = "SSProve: A Foundational Framework for Modular Cryptographic Proofs in Coq";
71 license = lib.licenses.mit;
72 maintainers = [
73 {
74 name = "Sebastian Ertel";
75 email = "sebastian.ertel@gmail.com";
76 github = "sertel";
77 githubId = 3703100;
78 }
79 ];
80 };
81
82})