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

   1 {stdenv, fetchurl, ocaml_with_sources}:
   2
   3 let
   4   pname = "hol_light";
   5   version = "100110";
   6   webpage = http://www.cl.cam.ac.uk/~jrh13/hol-light/;
   7
   8   dmtcp_checkpoint = ''
   9
  10 (* ------------------------------------------------------------------------- *)
  11 (* Non-destructive checkpoint using DMTCP.                                   *)
  12 (* ------------------------------------------------------------------------- *)
  13
  14 let dmtcp_checkpoint bannerstring =
  15   let longer_banner = startup_banner ^ " with DMTCP" in
  16   let complete_banner =
  17     if bannerstring = "" then longer_banner
  18     else longer_banner^"\n        "^bannerstring in
  19   (Gc.compact(); Unix.sleep 1;
  20    try ignore(Unix.system ("dmtcp_command -bc")) with _ -> ();
  21    Format.print_string complete_banner;
  22    Format.print_newline(); Format.print_newline());;
  23   '';
  24
  25 in
  26
  27 stdenv.mkDerivation {
  28   name = "${pname}-${version}";
  29   inherit version;
  30
  31   src = fetchurl {
  32     url = "${webpage}${pname}_${version}.tgz";
  33     sha256 = "1jkn9vpl3n9dgb96zwmly32h1p3f9mcf34pg6vm0fyvqp9kbx3ac";
  34   };
  35
  36   buildInputs = [ ocaml_with_sources ];
  37
  38   buildCommand = ''
  39     ensureDir "$out/src"
  40     cd "$out/src"
  41
  42     tar -xzf "$src"
  43     cd hol_light
  44
  45     substituteInPlace hol.ml --replace \
  46       "(try Sys.getenv \"HOLLIGHT_DIR\" with Not_found -> Sys.getcwd())" \
  47       "\"$out/src/hol_light\""
  48
  49     substituteInPlace Examples/update_database.ml --replace \
  50       "Filename.concat ocaml_source_dir" \
  51       "Filename.concat \"${ocaml_with_sources}/src/ocaml\""
  52
  53     echo '${dmtcp_checkpoint}' >> make.ml
  54
  55     make
  56   '';
  57
  58   meta = {
  59     description = "An interactive theorem prover based on Higher-Order Logic.";
  60     longDescription = ''
  61 HOL Light is a computer program to help users prove interesting mathematical
  62 theorems completely formally in Higher-Order Logic.  It sets a very exacting
  63 standard of correctness, but provides a number of automated tools and
  64 pre-proved mathematical theorems (e.g., about arithmetic, basic set theory and
  65 real analysis) to save the user work.  It is also fully programmable, so users
  66 can extend it with new theorems and inference rules without compromising its
  67 soundness.
  68     '';
  69     homepage = webpage;
  70     license = "BSD";
  71   };
  72 }