nixpkgs: add lean-20150328, a theorem prover.
Signed-off-by: Austin Seipp <aseipp@pobox.com>
This commit is contained in:
parent
75ab87edc8
commit
a6813ca62d
28
pkgs/applications/science/logic/lean/default.nix
Normal file
28
pkgs/applications/science/logic/lean/default.nix
Normal file
@ -0,0 +1,28 @@
|
|||||||
|
{ stdenv, fetchFromGitHub, cmake, gmp, mpfr, luajit, boost, python
|
||||||
|
, gperftools, ninja }:
|
||||||
|
|
||||||
|
stdenv.mkDerivation rec {
|
||||||
|
name = "lean-20150328";
|
||||||
|
|
||||||
|
src = fetchFromGitHub {
|
||||||
|
owner = "leanprover";
|
||||||
|
repo = "lean";
|
||||||
|
rev = "1b15036dba469020d37f7d6b77b88974d8a36cb1";
|
||||||
|
sha256 = "0w38g83gp7d3ybfiz9jpl2jz3ljad70bxmar0dnnv45wx42clg96";
|
||||||
|
};
|
||||||
|
|
||||||
|
buildInputs = [ gmp mpfr luajit boost cmake python gperftools ninja ];
|
||||||
|
enableParallelBuilding = true;
|
||||||
|
|
||||||
|
preConfigure = "cd src";
|
||||||
|
|
||||||
|
cmakeFlags = [ "-DCMAKE_BUILD_TYPE=Release" ];
|
||||||
|
|
||||||
|
meta = {
|
||||||
|
description = "Automatic and interactive theorem prover";
|
||||||
|
homepage = "http://leanprover.github.io";
|
||||||
|
license = stdenv.lib.licenses.asl20;
|
||||||
|
platforms = stdenv.lib.platforms.unix;
|
||||||
|
maintainers = [ stdenv.lib.maintainers.thoughtpolice ];
|
||||||
|
};
|
||||||
|
}
|
@ -13370,6 +13370,8 @@ let
|
|||||||
|
|
||||||
iprover = callPackage ../applications/science/logic/iprover {};
|
iprover = callPackage ../applications/science/logic/iprover {};
|
||||||
|
|
||||||
|
lean = callPackage ../applications/science/logic/lean {};
|
||||||
|
|
||||||
leo2 = callPackage ../applications/science/logic/leo2 {};
|
leo2 = callPackage ../applications/science/logic/leo2 {};
|
||||||
|
|
||||||
logisim = callPackage ../applications/science/logic/logisim {};
|
logisim = callPackage ../applications/science/logic/logisim {};
|
||||||
|
Loading…
x
Reference in New Issue
Block a user