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