pkgs/applications/science/logic/hol_light/default.nix

   1 {stdenv, fetchsvn, ocaml, camlp5_transitional}:
   2
   3 stdenv.mkDerivation rec {
   4   name = "hol_light-${version}";
   5   version = "20100820svn57";
   6
   7   inherit ocaml;
   8   camlp5 = camlp5_transitional;
   9
  10   src = fetchsvn {
  11     url = http://hol-light.googlecode.com/svn/trunk;
  12     rev = "57";
  13     sha256 = "d1372744abca6c9978673850977d3e1577fd8cfd8298826eb713b3681c10cccd";
  14   };
  15
  16   buildInputs = [ ocaml camlp5 ];
  17
  18   buildCommand = ''
  19     export HOL_DIR="$out/src/hol_light"
  20     ensureDir `dirname $HOL_DIR` "$out/bin"
  21     cp -a "${src}" "$HOL_DIR"
  22     cd "$HOL_DIR"
  23     chmod -R u+rwX .
  24
  25     substituteInPlace hol.ml --replace \
  26       "(try Sys.getenv \"HOLLIGHT_DIR\" with Not_found -> Sys.getcwd())" \
  27       "\"$HOL_DIR\""
  28
  29     substituteInPlace Makefile --replace \
  30       "+camlp5" \
  31       "${camlp5}/lib/ocaml/camlp5"
  32
  33     substitute ${./start_hol_light} "$out/bin/start_hol_light" \
  34       --subst-var-by OCAML "${ocaml}" \
  35       --subst-var-by CAMLP5 "${camlp5_transitional}" \
  36       --subst-var HOL_DIR
  37     chmod +x "$out/bin/start_hol_light"
  38
  39     make
  40   '';
  41
  42   meta = {
  43     description = "An interactive theorem prover based on Higher-Order Logic.";
  44     longDescription = ''
  45 HOL Light is a computer program to help users prove interesting mathematical
  46 theorems completely formally in Higher-Order Logic.  It sets a very exacting
  47 standard of correctness, but provides a number of automated tools and
  48 pre-proved mathematical theorems (e.g., about arithmetic, basic set theory and
  49 real analysis) to save the user work.  It is also fully programmable, so users
  50 can extend it with new theorems and inference rules without compromising its
  51 soundness.
  52     '';
  53     homepage = http://www.cl.cam.ac.uk/~jrh13/hol-light/;
  54     license = "BSD";
  55     ocamlVersions = [ "3.10.0" "3.11.1" ];
  56   };
  57 }