diff options
author | William A. Kennington III <william@wkennington.com> | 2015-03-25 22:14:10 -0700 |
---|---|---|
committer | William A. Kennington III <william@wkennington.com> | 2015-03-25 22:14:10 -0700 |
commit | 2e815a74447e4f4cc0849df3a98a04c2a2df827a (patch) | |
tree | ec79818f48fdded63fdda3320d2f0f7b0c79088e /pkgs/applications | |
parent | 18867a6b83a62df988f05039534a6b518bfef6b7 (diff) | |
parent | 172167c937595938871559fafcd083f002c32a22 (diff) | |
download | nixlib-2e815a74447e4f4cc0849df3a98a04c2a2df827a.tar nixlib-2e815a74447e4f4cc0849df3a98a04c2a2df827a.tar.gz nixlib-2e815a74447e4f4cc0849df3a98a04c2a2df827a.tar.bz2 nixlib-2e815a74447e4f4cc0849df3a98a04c2a2df827a.tar.lz nixlib-2e815a74447e4f4cc0849df3a98a04c2a2df827a.tar.xz nixlib-2e815a74447e4f4cc0849df3a98a04c2a2df827a.tar.zst nixlib-2e815a74447e4f4cc0849df3a98a04c2a2df827a.zip |
Merge pull request #6961 from bcdarwin/abella
new package: abella 2.0.2
Diffstat (limited to 'pkgs/applications')
-rw-r--r-- | pkgs/applications/science/logic/abella/default.nix | 38 |
1 files changed, 38 insertions, 0 deletions
diff --git a/pkgs/applications/science/logic/abella/default.nix b/pkgs/applications/science/logic/abella/default.nix new file mode 100644 index 000000000000..1c3e8e412f80 --- /dev/null +++ b/pkgs/applications/science/logic/abella/default.nix @@ -0,0 +1,38 @@ +{ stdenv, fetchurl, rsync, ocaml }: + +stdenv.mkDerivation rec { + name = "abella-${version}"; + version = "2.0.2"; + + src = fetchurl { + url = "http://abella-prover.org/distributions/${name}.tar.gz"; + sha256 = "b56d865ebdb198111f1dcd5b6fbcc0d7fc6dd1294f7601903ba4e3c3322c099c"; + }; + + buildInputs = [ rsync ocaml ]; + + installPhase = '' + mkdir -p $out/bin + rsync -av abella $out/bin/ + + mkdir -p $out/share/emacs/site-lisp/abella/ + rsync -av emacs/ $out/share/emacs/site-lisp/abella/ + + mkdir -p $out/share/abella/examples + rsync -av examples/ $out/share/abella/examples/ + ''; + + meta = { + description = "Interactive theorem prover"; + longDescription = '' + Abella is an interactive theorem prover based on lambda-tree syntax. + This means that Abella is well-suited for reasoning about the meta-theory + of programming languages and other logical systems which manipulate + objects with binding. + ''; + homepage = http://abella-prover.org/; + license = stdenv.lib.licenses.gpl3; + maintainers = with stdenv.lib.maintainers; [ bcdarwin ]; + platforms = stdenv.lib.platforms.unix; + }; +} |