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

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