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