nixpkgs: add alt-ergo 0.95.2

Signed-off-by: Austin Seipp <aseipp@pobox.com>
This commit is contained in:
Austin Seipp 2014-05-01 02:29:42 -05:00
parent 4ee4f76176
commit 6d52463bd3
3 changed files with 31 additions and 0 deletions

View File

@ -260,4 +260,10 @@
fullName = "Sleepycat Public License";
url = "https://en.wikipedia.org/wiki/Sleepycat_License";
};
cecill-c = {
shortName = "CeCILL-C";
fullName = "CEA CNRS INRIA Logiciel Libre";
url = "http://www.cecill.info/licences.en.html";
};
}

View File

@ -0,0 +1,23 @@
{ fetchurl, stdenv, ocaml, ocamlPackages, gmp }:
stdenv.mkDerivation rec {
name = "alt-ergo-${version}";
version = "0.95.2";
src = fetchurl {
url = "http://alt-ergo.ocamlpro.com/download_manager.php?target=${name}.tar.gz";
name = "${name}.tar.gz";
sha256 = "1b7f0rh3jgm67g0x2m3wv7gnnqmz9cjlrfm136z56ihlkhsd8v2s";
};
buildInputs = with ocamlPackages;
[ ocaml findlib ocamlgraph zarith lablgtk gmp ];
meta = {
description = "Alt-Ergo is a high-performance theorem prover and SMT solver";
homepage = "http://alt-ergo.ocamlpro.com/";
license = stdenv.lib.licenses.cecill-c; # LGPL-2 compatible
platforms = stdenv.lib.platforms.linux;
maintainers = [ stdenv.lib.maintainers.thoughtpolice ];
};
}

View File

@ -10294,6 +10294,8 @@ let
### SCIENCE/LOGIC
alt-ergo = callPackage ../applications/science/logic/alt-ergo {};
coq = callPackage ../applications/science/logic/coq {
inherit (ocamlPackages) findlib lablgtk;
camlp5 = ocamlPackages.camlp5_transitional;