tjh.dev
1{
2 lib,
3 fetchurl,
4 buildDunePackage,
5 alcotest,
6 dedukti,
7 bindlib,
8 camlp-streams,
9 cmdliner,
10 dream,
11 lwt_ppx,
12 menhir,
13 pratter,
14 sedlex,
15 stdlib-shims,
16 timed,
17 why3,
18 yojson,
19}:
20
21buildDunePackage rec {
22 pname = "lambdapi";
23 version = "2.6.0";
24
25 minimalOCamlVersion = "4.12";
26
27 src = fetchurl {
28 url = "https://github.com/Deducteam/lambdapi/releases/download/${version}/lambdapi-${version}.tbz";
29 hash = "sha256-0B5fE9suq6bk/jMGZxSeAFnUiGxlH/nWtnLbLfyXZe0=";
30 };
31
32 nativeBuildInputs = [
33 dream
34 menhir
35 ];
36 buildInputs = [ lwt_ppx ];
37 propagatedBuildInputs = [
38 bindlib
39 camlp-streams
40 cmdliner
41 dream
42 pratter
43 sedlex
44 stdlib-shims
45 timed
46 why3
47 yojson
48 ];
49
50 checkInputs = [
51 alcotest
52 dedukti
53 ];
54 doCheck = false; # anomaly: Sys_error("/homeless-shelter/.why3.conf: No such file or directory")
55
56 meta = with lib; {
57 homepage = "https://github.com/Deducteam/lambdapi";
58 description = "Proof assistant based on the λΠ-calculus modulo rewriting";
59 license = licenses.cecill21;
60 changelog = "https://github.com/Deducteam/lambdapi/raw/${version}/CHANGES.md";
61 maintainers = with maintainers; [ bcdarwin ];
62 };
63}