4e5db40581
Also replace the monolitic derivation hol_light_binaries with smaller derivations. Now the installation works as follows: # Install the base system and a script "start_hol_light" $ nix-env -i hol_light_sources hol_light # Install a checkpointed executable with the core library preloaded $ nix-env -i hol_light_core_dmtcp # Install HOL Light binaries preloaded with other specific libraries: $ nix-env -i hol_light_multivariate_dmtcp $ nix-env -i hol_light_complex_dmtcp $ nix-env -i hol_light_sosa_dmtcp $ nix-env -i hol_light_card_dmtcp svn path=/nixpkgs/trunk/; revision=23815
20 lines
916 B
OCaml
20 lines
916 B
OCaml
(* ------------------------------------------------------------------------- *)
|
|
(* Create a standalone HOL image. Assumes that we are running under Linux *)
|
|
(* and have the program "dmtcp" available to create checkpoints. *)
|
|
(* ------------------------------------------------------------------------- *)
|
|
|
|
let dmtcp_checkpoint, dmtcp_selfdestruct =
|
|
let call_dmtcp opts 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(); Unix.sleep 1;
|
|
Format.print_string "Checkpointing..."; Format.print_newline();
|
|
try ignore(Unix.system ("dmtcp_command -bc " ^ opts))
|
|
with Unix.Unix_error _ -> ();
|
|
Format.print_string complete_banner;
|
|
Format.print_newline(); Format.print_newline())
|
|
in
|
|
call_dmtcp "", call_dmtcp "-q";;
|