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.2")
30 ];
31 out = "0.1.0";
32 }
33 ]
34 null;
35
36 release."0.1.0".sha256 = "+Of/DP2Vjsa7ASKswjlvqqhcmDhC9WrozridedNZQkY=";
37
38 releaseRev = v: "v${v}";
39
40 propagatedBuildInputs = [
41 coq.ocamlPackages.findlib
42 metacoq
43 ];
44
45 postPatch = ''
46 patchShebangs ./process_extraction.sh
47 patchShebangs ./tests/process-extraction-examples.sh
48 '';
49
50 mlPlugin = true;
51
52 meta = {
53 description = "A framework for extracting Coq programs to Rust";
54 maintainers = with maintainers; [ _4ever2 ];
55 license = licenses.mit;
56 };
57}