pkgs/applications/science/logic/hol: initial version
svn path=/nixpkgs/trunk/; revision=23430
This commit is contained in:
parent
9570117dc4
commit
970b3402e9
55
pkgs/applications/science/logic/hol/default.nix
Normal file
55
pkgs/applications/science/logic/hol/default.nix
Normal file
|
@ -0,0 +1,55 @@
|
||||||
|
{stdenv, fetchurl, polyml}:
|
||||||
|
|
||||||
|
stdenv.mkDerivation {
|
||||||
|
name = "hol";
|
||||||
|
|
||||||
|
src = fetchurl {
|
||||||
|
#url = "http://downloads.sourceforge.net/project/hol/hol/kananaskis-5/kananaskis-5.tar.gz";
|
||||||
|
url = mirror://sourceforge/hol/hol/kananaskis-5/kananaskis-5.tar.gz;
|
||||||
|
sha256 = "1qjfx5ii80v17yr04hz70n8aa46892fjc4qcxs9gs7nh3hw7rvmx";
|
||||||
|
};
|
||||||
|
|
||||||
|
buildInputs = [polyml];
|
||||||
|
|
||||||
|
buildCommand = ''
|
||||||
|
ensureDir "$out/src"
|
||||||
|
cd "$out/src"
|
||||||
|
|
||||||
|
tar -xzf "$src"
|
||||||
|
cd hol
|
||||||
|
|
||||||
|
substituteInPlace tools-poly/Holmake/Holmake.sml --replace \
|
||||||
|
"\"/bin/mv\"" \
|
||||||
|
"\"mv\""
|
||||||
|
|
||||||
|
#sed -ie "/compute/,999 d" tools/build-sequence # for testing
|
||||||
|
|
||||||
|
poly < tools/smart-configure.sml
|
||||||
|
|
||||||
|
bin/build -expk -symlink
|
||||||
|
|
||||||
|
ensureDir "$out/bin"
|
||||||
|
ln -st $out/bin $out/src/hol/bin/*
|
||||||
|
# ln -s $out/src/hol/bin $out/bin
|
||||||
|
'';
|
||||||
|
|
||||||
|
meta = {
|
||||||
|
description = "HOL4, an interactive theorem prover based on Higher-Order Logic.";
|
||||||
|
longDescription = ''
|
||||||
|
|
||||||
|
HOL4 is the latest version of the HOL interactive proof
|
||||||
|
assistant for higher order logic: a programming environment in
|
||||||
|
which theorems can be proved and proof tools
|
||||||
|
implemented. Built-in decision procedures and theorem provers
|
||||||
|
can automatically establish many simple theorems (users may have
|
||||||
|
to prove the hard theorems themselves!) An oracle mechanism
|
||||||
|
gives access to external programs such as SMT and BDD
|
||||||
|
engines. HOL4 is particularly suitable as a platform for
|
||||||
|
implementing combinations of deduction, execution and property
|
||||||
|
checking.
|
||||||
|
|
||||||
|
'';
|
||||||
|
homepage = "http://hol.sourceforge.net/";
|
||||||
|
license = "BSD";
|
||||||
|
};
|
||||||
|
}
|
|
@ -6759,6 +6759,8 @@ let
|
||||||
camlp5 = camlp5_transitional;
|
camlp5 = camlp5_transitional;
|
||||||
};
|
};
|
||||||
|
|
||||||
|
hol = callPackage ../applications/science/logic/hol { };
|
||||||
|
|
||||||
hol_light = callPackage ../applications/science/logic/hol_light { };
|
hol_light = callPackage ../applications/science/logic/hol_light { };
|
||||||
|
|
||||||
hol_light_binaries = callPackage ../applications/science/logic/hol_light/binaries.nix { };
|
hol_light_binaries = callPackage ../applications/science/logic/hol_light/binaries.nix { };
|
||||||
|
|
Loading…
Reference in New Issue
Block a user