blob: 9dd0c0ebee5c63bcbb2a46aff6bd7557923770d4 (
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
|
{
lib,
mkRocqDerivation,
rocq-core,
version ? null,
}:
mkRocqDerivation {
pname = "micromega-plugin";
owner = "rocq-community";
inherit version;
defaultVersion =
let
case = case: out: { inherit case out; };
in
with lib.versions;
lib.switch rocq-core.rocq-version [
(case (range "9.0" "9.3") "1.1.1")
(case (range "9.0" "9.2") "1.1.0")
] null;
release = {
"1.1.1".hash = "sha256-TIUbrMRoPkLx3QcBGTAEdnzqt4HcKOHaQwJWUtBXUQA=";
"1.1.0".hash = "sha256-CWMbGErC5bu20Yu9eskgslLkzmSof6klNlOYEkQjUjc=";
};
releaseRev = v: "v${v}";
mlPlugin = true;
useDune = true;
nativeBuildInputs = [
rocq-core.ocamlPackages.ppx_optcomp
];
propagatedBuildInputs = [
rocq-core.ocamlPackages.findlib
];
configurePhase = ''
patchShebangs etc/with-rocq-wrap.sh
'';
buildPhase = ''
etc/with-rocq-wrap.sh dune build -p rocq-micromega-plugin @install ''${enableParallelBuilding:+-j $NIX_BUILD_CORES}
'';
installPhase = ''
etc/with-rocq-wrap.sh dune install --root . rocq-micromega-plugin --prefix=$out --libdir $OCAMLFIND_DESTDIR
mkdir $out/lib/coq/
mv $OCAMLFIND_DESTDIR/coq $out/lib/coq/${rocq-core.rocq-version}
'';
meta = {
description = "Plugin for (semi)decision procedures for arithmetic.";
license = lib.licenses.lgpl21;
};
}
|
