diff --git a/pkgs/applications/science/logic/beluga/default.nix b/pkgs/applications/science/logic/beluga/default.nix new file mode 100644 index 00000000000..da0e9bf1c1d --- /dev/null +++ b/pkgs/applications/science/logic/beluga/default.nix @@ -0,0 +1,34 @@ +{ stdenv, fetchFromGitHub, ocamlPackages, omake }: + +stdenv.mkDerivation { + name = "beluga-20180403"; + + src = fetchFromGitHub { + owner = "Beluga-lang"; + repo = "Beluga"; + rev = "046aa59f008be70a7c4700b723bed0214ea8b687"; + sha256 = "0m68y0r0wdw3mg2jks68bihaww7sg305zdfnic1rkndq2cxv0mld"; + }; + + nativeBuildInputs = with ocamlPackages; [ findlib ocamlbuild omake ]; + buildInputs = with ocamlPackages; [ ocaml ulex ocaml_extlib ]; + + installPhase = '' + mkdir -p $out + cp -r bin $out/ + + mkdir -p $out/share/beluga + cp -r tools/ examples/ $out/share/beluga + + mkdir -p $out/share/emacs/site-lisp/beluga/ + cp -r tools/beluga-mode.el $out/share/emacs/site-lisp/beluga + ''; + + meta = { + description = "A functional language for reasoning about formal systems"; + homepage = http://complogic.cs.mcgill.ca/beluga/; + license = stdenv.lib.licenses.gpl3Plus; + maintainers = [ stdenv.lib.maintainers.bcdarwin ]; + platforms = stdenv.lib.platforms.unix; + }; +} diff --git a/pkgs/top-level/all-packages.nix b/pkgs/top-level/all-packages.nix index 4f6add40f87..fb07c9b5ea3 100644 --- a/pkgs/top-level/all-packages.nix +++ b/pkgs/top-level/all-packages.nix @@ -19879,6 +19879,8 @@ with pkgs; aspino = callPackage ../applications/science/logic/aspino {}; + beluga = callPackage ../applications/science/logic/beluga { }; + boogie = dotnetPackages.Boogie; inherit (callPackage ./coq-packages.nix {})