nixpkgs/pkgs/applications/science/logic/hol/default.nix
Bjørn Forsman 083d0890f5 More description fixes
* Remove package name
* Start with upper case letter
* Remove trailing period

Also reword some descriptions and move some long descriptions to
longDescription.

I'm not touching generated packages.
2013-10-06 12:01:38 +02:00

59 lines
1.7 KiB
Nix

{stdenv, fetchurl, polyml, experimentalKernel ? false}:
let
pname = "hol4";
version = "k.7";
kernelFlag = if experimentalKernel then "-expk" else "-stdknl";
in
stdenv.mkDerivation {
name = "${pname}-${version}";
src = fetchurl {
url = mirror://sourceforge/hol/hol/kananaskis-7/kananaskis-7.tar.gz;
sha256 = "0gs1nmjvsjhnndama9v7gids2g86iip53v7d7dm3sfq6jxmqkwkl";
};
buildInputs = [polyml];
buildCommand = ''
mkdir -p "$out/src"
cd "$out/src"
tar -xzf "$src"
cd hol4.${version}
substituteInPlace tools/Holmake/Holmake_types.sml \
--replace "\"/bin/mv\"" "\"mv\"" \
--replace "\"/bin/cp\"" "\"cp\""
#sed -ie "/compute/,999 d" tools/build-sequence # for testing
poly < tools/smart-configure.sml
bin/build ${kernelFlag} -symlink
mkdir -p "$out/bin"
ln -st $out/bin $out/src/hol4.${version}/bin/*
# ln -s $out/src/hol4.${version}/bin $out/bin
'';
meta = {
description = "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";
};
}