513d653d68
Add pkgs/applications/science/logic/hol_light and pkgs/applications/science/emacs-modes/hol_light Some functionalities of HOL Light requires the compiled sources of OCaml. For now we provide a new package ocaml_with_sources. After this shuold be merged with the current version of OCaml already present in nixpkgs. svn path=/nixpkgs/trunk/; revision=20008
30 lines
1.4 KiB
OCaml
30 lines
1.4 KiB
OCaml
(* ========================================================================= *)
|
|
(* Create a standalone HOL image. Assumes that we are running under Linux *)
|
|
(* and have the program "dmtcp" available to create checkpoints. *)
|
|
(* *)
|
|
(* (c) Copyright, John Harrison 1998-2007 *)
|
|
(* (c) Copyright, Marco Maggesi 2010 *)
|
|
(* ========================================================================= *)
|
|
|
|
#use "make.ml";;
|
|
|
|
(* ------------------------------------------------------------------------- *)
|
|
(* Non-destructive checkpoint using DMTCP. *)
|
|
(* ------------------------------------------------------------------------- *)
|
|
|
|
let checkpoint bannerstring =
|
|
let longer_banner = startup_banner ^ " with DMTCP" in
|
|
let complete_banner =
|
|
if bannerstring = "" then longer_banner
|
|
else longer_banner^"\n "^bannerstring in
|
|
(Gc.compact();
|
|
loadt "Examples/update_database.ml";
|
|
print_newline ();
|
|
Unix.sleep 1;
|
|
try ignore(Unix.system ("dmtcp_command -bc")) with _ -> ();
|
|
Format.print_string complete_banner;
|
|
Format.print_newline(); Format.print_newline());;
|
|
|
|
loadt "Multivariate/make_complex.ml";;
|
|
dmtcp_checkpoint "Preloaded with multivariate-based complex analysis";;
|