pkgs/development/ocaml-modules/lambdapi/default.nix

   1 {
   2   lib,
   3   fetchurl,
   4   buildDunePackage,
   5   alcotest,
   6   dedukti,
   7   bindlib,
   8   camlp-streams,
   9   cmdliner,
  10   menhir,
  11   pratter,
  12   sedlex,
  13   stdlib-shims,
  14   timed,
  15   why3,
  16   yojson,
  17 }:
  18
  19 buildDunePackage rec {
  20   pname = "lambdapi";
  21   version = "2.3.1";
  22
  23   minimalOCamlVersion = "4.12";
  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
  33     camlp-streams
  34     cmdliner
  35     pratter
  36     sedlex
  37     stdlib-shims
  38     timed
  39     why3
  40     yojson
  41   ];
  42
  43   checkInputs = [
  44     alcotest
  45     dedukti
  46   ];
  47   doCheck = false; # anomaly: Sys_error("/homeless-shelter/.why3.conf: No such file or directory")
  48
  49   meta = with lib; {
  50     homepage = "https://github.com/Deducteam/lambdapi";
  51     description = "Proof assistant based on the λΠ-calculus modulo rewriting";
  52     license = licenses.cecill21;
  53     changelog = "https://github.com/Deducteam/lambdapi/raw/${version}/CHANGES.md";
  54     maintainers = with maintainers; [ bcdarwin ];
  55   };
  56 }