1 {stdenv, fetchurl, ocaml_with_sources}:
6 webpage = http://www.cl.cam.ac.uk/~jrh13/hol-light/;
10 (* ------------------------------------------------------------------------- *)
11 (* Non-destructive checkpoint using DMTCP. *)
12 (* ------------------------------------------------------------------------- *)
14 let dmtcp_checkpoint bannerstring =
15 let longer_banner = startup_banner ^ " with DMTCP" in
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());;
28 name = "${pname}-${version}";
32 url = "${webpage}${pname}_${version}.tgz";
33 sha256 = "1jkn9vpl3n9dgb96zwmly32h1p3f9mcf34pg6vm0fyvqp9kbx3ac";
36 buildInputs = [ ocaml_with_sources ];
45 substituteInPlace hol.ml --replace \
46 "(try Sys.getenv \"HOLLIGHT_DIR\" with Not_found -> Sys.getcwd())" \
47 "\"$out/src/hol_light\""
49 substituteInPlace Examples/update_database.ml --replace \
50 "Filename.concat ocaml_source_dir" \
51 "Filename.concat \"${ocaml_with_sources}/src/ocaml\""
53 echo '${dmtcp_checkpoint}' >> make.ml
59 description = "An interactive theorem prover based on Higher-Order Logic.";
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