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