blob: 3c9dcfd32e5f362d8b50f77a19d3ffcc28e01665 (
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
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
|
{
lib,
mkCoqDerivation,
which,
coq,
stdlib,
metarocq-erasure,
version ? null,
single ? false,
}:
let
pname = "TypedExtraction";
repo = "rocq-typed-extraction";
owner = "peregrine-project";
domain = "github.com";
inherit version;
defaultVersion =
let
case = coq: mr: out: {
cases = [
coq
mr
];
inherit out;
};
in
lib.switch
[
coq.coq-version
metarocq-erasure.version
]
[
(case "9.1" "1.5.1-9.1" "0.2.1")
(case "9.1" (lib.versions.range "1.4" "1.4.1") "0.2.0")
]
null;
release = {
"0.2.1".sha256 = "sha256-GWdu/l7CipeBubgS5OGHsZfpP2Fkr1cfiZMRH5d1n0g=";
"0.2.0".sha256 = "sha256-rgg39X45IXjcnejBhh8N7wMiH+gHQrfO8pBbFEWOGVI=";
};
releaseRev = v: "v${v}";
packages = {
"common" = [ ];
"elm" = [
"common"
];
"rust" = [
"common"
];
"plugin" = [
"elm"
"rust"
];
"all" = [
"plugin"
];
};
typedextraction_ =
package:
let
typedextraction-deps = lib.optionals (package != "single") (
map typedextraction_ packages.${package}
);
pkgpath = if package == "single" then "./" else "./${package}";
pname = if package == "all" then "TypedExtraction" else "TypedExtraction-${package}";
pkgallMake = ''
mkdir all
echo "all:" > all/Makefile
echo "install:" >> all/Makefile
'';
derivation = (
mkCoqDerivation (
{
inherit
version
pname
defaultVersion
release
releaseRev
repo
owner
;
mlPlugin = true;
propagatedBuildInputs = [
stdlib
coq.ocamlPackages.findlib
metarocq-erasure
]
++ typedextraction-deps;
patchPhase = ''
patchShebangs ./configure.sh
patchShebangs ./plugin/process_extraction.sh
'';
configurePhase =
lib.optionalString (package == "all") pkgallMake
+ ''
touch ${pkgpath}/_config
''
+ lib.optionalString (package == "single") ''
./configure.sh local
'';
preBuild = ''
cd ${pkgpath}
'';
meta = {
homepage = "https://peregrine-project.github.io/";
description = "A framework for extracting Rocq programs to Rust and Elm";
maintainers = with lib.maintainers; [ _4ever2 ];
license = lib.licenses.mit;
};
}
// lib.optionalAttrs (package != "single") {
passthru = lib.mapAttrs (package: deps: typedextraction_ package) packages;
}
)
);
in
derivation;
in
typedextraction_ (if single then "single" else "all")
|
