blob: b9d2d731bcd781a0f3cd8e6a56da57078ea0c12c (
plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
|
{
lib,
mkCoqDerivation,
which,
coq,
metacoq,
version ? null,
}:
mkCoqDerivation {
pname = "RustExtraction";
repo = "coq-rust-extraction";
owner = "AU-COBRA";
domain = "github.com";
inherit version;
defaultVersion =
let
case = coq: mc: out: {
cases = [
coq
mc
];
inherit out;
};
inherit (lib.versions) range;
in
lib.switch
[
coq.coq-version
metacoq.version
]
[
(case (range "8.20" "9.0") (range "1.3.2" "1.3.4") "0.1.1")
(case (range "8.17" "8.19") (range "1.3.1" "1.3.3") "0.1.0")
]
null;
release."0.1.0".sha256 = "+Of/DP2Vjsa7ASKswjlvqqhcmDhC9WrozridedNZQkY=";
release."0.1.1".sha256 = "CPZ5J9knJ1aYoQ7RQN8YFSpxqJXjgQaxIA4F8G6X4tM=";
releaseRev = v: "v${v}";
propagatedBuildInputs = [
coq.ocamlPackages.findlib
metacoq
];
postPatch = ''
patchShebangs ./process_extraction.sh
patchShebangs ./tests/process-extraction-examples.sh
'';
mlPlugin = true;
meta = {
description = "Framework for extracting Coq programs to Rust";
maintainers = with lib.maintainers; [ _4ever2 ];
license = lib.licenses.mit;
};
}
|
