pyrox.dev
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.18" "9.0") (range "2.3.0" "2.4.0") "0.2.4")
35 (case (range "8.18" "8.20") (range "2.3.0" "2.3.0") "0.2.3")
36 (case (range "8.18" "8.20") (range "2.1.0" "2.2.0") "0.2.2")
37 # This is the original dependency:
38 # (case "8.17" "1.18.0" "0.1.0")
39 # But it is not loadable. The math-comp nixpkgs configuration
40 # will always only output version 1.18.0 for Coq 8.17.
41 # Hence, the Coq 8.17 and math-comp 1.17.0 must be explicitly set
42 # to load it.
43 # (This version is not on the math-comp CI and hence not checked.)
44 (case "8.17" "1.17.0" "0.1.0")
45 ]
46 null;
47
48 releaseRev = v: "v${v}";
49
50 release."0.2.4".sha256 = "sha256-uglr47aDgSkKi2JyVyN+2BrokZISZUAE8OUylGjy7ds=";
51 release."0.2.3".sha256 = "sha256-Y3dmNIF36IuIgrVILteofOv8e5awKfq93S4YN7enswI=";
52 release."0.2.2".sha256 = "sha256-tBF8equJd6hKZojpe+v9h6Tg9xEnMTVFgOYK7ZnMfxk=";
53 release."0.2.1".sha256 = "sha256-X00q5QFxdcGWeNqOV/PLTOqQyyfqFEinbGUTO7q8bC4=";
54 release."0.2.0".sha256 = "sha256-GDkWH0LUsW165vAUoYC5of9ndr0MbfBtmrPhsJVXi3o=";
55 release."0.1.0".sha256 = "sha256-Yj+k+mBsudi3d6bRVlZLyM4UqQnzAX5tHvxtKoIuNTE=";
56
57 propagatedBuildInputs = [
58 equations
59 mathcomp-boot
60 mathcomp-analysis
61 mathcomp-experimental-reals
62 extructures
63 deriving
64 mathcomp-word
65 ];
66
67 meta = with lib; {
68 description = "SSProve: A Foundational Framework for Modular Cryptographic Proofs in Coq";
69 license = licenses.mit;
70 maintainers = [
71 {
72 name = "Sebastian Ertel";
73 email = "sebastian.ertel@gmail.com";
74 github = "sertel";
75 githubId = 3703100;
76 }
77 ];
78 };
79
80})