pyrox.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 let
20 case = coq: mc: out: {
21 cases = [
22 coq
23 mc
24 ];
25 inherit out;
26 };
27 in
28 with versions;
29 switch
30 [
31 coq.coq-version
32 metacoq.version
33 ]
34 [
35 (case (range "8.20" "9.0") (range "1.3.2" "1.3.4") "0.1.1")
36 (case (range "8.17" "8.19") (range "1.3.1" "1.3.3") "0.1.0")
37 ]
38 null;
39
40 release."0.1.0".sha256 = "+Of/DP2Vjsa7ASKswjlvqqhcmDhC9WrozridedNZQkY=";
41 release."0.1.1".sha256 = "CPZ5J9knJ1aYoQ7RQN8YFSpxqJXjgQaxIA4F8G6X4tM=";
42
43 releaseRev = v: "v${v}";
44
45 propagatedBuildInputs = [
46 coq.ocamlPackages.findlib
47 metacoq
48 ];
49
50 postPatch = ''
51 patchShebangs ./process_extraction.sh
52 patchShebangs ./tests/process-extraction-examples.sh
53 '';
54
55 mlPlugin = true;
56
57 meta = {
58 description = "Framework for extracting Coq programs to Rust";
59 maintainers = with maintainers; [ _4ever2 ];
60 license = licenses.mit;
61 };
62}