diff options
author | Peter Simons <simons@cryp.to> | 2010-08-25 19:50:24 +0000 |
---|---|---|
committer | Peter Simons <simons@cryp.to> | 2010-08-25 19:50:24 +0000 |
commit | 970b3402e9062668c8679e8297303103f1513899 (patch) | |
tree | 239b28f80c35d5f34bcf419743fa0cd8e47925bc /pkgs/applications/science/logic | |
parent | 9570117dc494922675233dc00d1160e2428f0a9b (diff) | |
download | nixlib-970b3402e9062668c8679e8297303103f1513899.tar nixlib-970b3402e9062668c8679e8297303103f1513899.tar.gz nixlib-970b3402e9062668c8679e8297303103f1513899.tar.bz2 nixlib-970b3402e9062668c8679e8297303103f1513899.tar.lz nixlib-970b3402e9062668c8679e8297303103f1513899.tar.xz nixlib-970b3402e9062668c8679e8297303103f1513899.tar.zst nixlib-970b3402e9062668c8679e8297303103f1513899.zip |
pkgs/applications/science/logic/hol: initial version
svn path=/nixpkgs/trunk/; revision=23430
Diffstat (limited to 'pkgs/applications/science/logic')
-rw-r--r-- | pkgs/applications/science/logic/hol/default.nix | 55 |
1 files changed, 55 insertions, 0 deletions
diff --git a/pkgs/applications/science/logic/hol/default.nix b/pkgs/applications/science/logic/hol/default.nix new file mode 100644 index 000000000000..63040b7fdd52 --- /dev/null +++ b/pkgs/applications/science/logic/hol/default.nix @@ -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"; + }; +} |