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
|
{
lib,
fetchurl,
buildDunePackage,
alcotest,
dedukti,
camlp-streams,
cmdliner,
dream,
lwt_ppx,
menhir,
pratter,
sedlex,
stdlib-shims,
timed,
why3,
yojson,
}:
buildDunePackage rec {
pname = "lambdapi";
version = "3.0.0";
minimalOCamlVersion = "4.14";
src = fetchurl {
url = "https://github.com/Deducteam/lambdapi/releases/download/${version}/lambdapi-${version}.tbz";
hash = "sha256-EGau0mGP2OakAMUUfb9V6pd86NP+LlGKxnhcZ3WhuL4=";
};
nativeBuildInputs = [
dream
menhir
];
buildInputs = [ lwt_ppx ];
propagatedBuildInputs = [
camlp-streams
cmdliner
dream
pratter
sedlex
stdlib-shims
timed
why3
yojson
];
checkInputs = [
alcotest
dedukti
];
doCheck = false; # anomaly: Sys_error("/homeless-shelter/.why3.conf: No such file or directory")
meta = {
homepage = "https://github.com/Deducteam/lambdapi";
description = "Proof assistant based on the λΠ-calculus modulo rewriting";
license = lib.licenses.cecill21;
changelog = "https://github.com/Deducteam/lambdapi/raw/${version}/CHANGES.md";
maintainers = with lib.maintainers; [ bcdarwin ];
};
}
|
