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