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
100 lines
2.9 KiB
Nix
100 lines
2.9 KiB
Nix
{stdenv, writeTextFile, hol_light, dmtcp}:
|
|
let
|
|
mkRestartScript = checkpointFile:
|
|
let filename = "hol_light_${checkpointFile.variant}_dmtcp"; in
|
|
writeTextFile {
|
|
name = "${filename}-${hol_light.version}";
|
|
destination = "/bin/${filename}";
|
|
executable = true;
|
|
text = ''
|
|
#!/bin/sh
|
|
exec ${dmtcp}/bin/dmtcp_restart --quiet ${checkpointFile}
|
|
'';
|
|
};
|
|
|
|
mkCkptFile =
|
|
{ variant
|
|
, banner
|
|
, loads
|
|
, startCkpt ? null
|
|
, buildCommand ? ''
|
|
cp ${startCkpt} hol_light_restart.ckpt
|
|
(echo "$loadScript" | dmtcp_restart --quiet hol_light_restart.ckpt) || exit 0
|
|
cp hol_light_restart.ckpt $out
|
|
''
|
|
}:
|
|
stdenv.mkDerivation rec {
|
|
name = "hol_light_${variant}_dmtcp.checkpoint-${hol_light.version}";
|
|
inherit variant banner buildCommand;
|
|
buildInputs = [ dmtcp hol_light ];
|
|
loadScript = ''
|
|
${loads}
|
|
dmtcp_checkpoint "${banner}";;
|
|
'';
|
|
};
|
|
in
|
|
rec {
|
|
hol_light_core_dmtcp = mkRestartScript hol_light_core_dmtcp_ckpt;
|
|
hol_light_sosa_dmtcp = mkRestartScript hol_light_sosa_dmtcp_ckpt;
|
|
hol_light_card_dmtcp = mkRestartScript hol_light_card_dmtcp_ckpt;
|
|
hol_light_multivariate_dmtcp = mkRestartScript hol_light_multivariate_dmtcp_ckpt;
|
|
hol_light_complex_dmtcp = mkRestartScript hol_light_complex_dmtcp_ckpt;
|
|
|
|
hol_light_core_dmtcp_ckpt = mkCkptFile rec {
|
|
variant = "core";
|
|
banner = "";
|
|
loads = ''
|
|
#use "${./dmtcp_selfdestruct.ml}";;
|
|
'';
|
|
buildCommand = ''
|
|
(echo "$loadScript" | dmtcp_checkpoint --quiet ${hol_light}/bin/start_hol_light) || exit 0
|
|
mv ckpt* $out
|
|
'';
|
|
};
|
|
|
|
hol_light_multivariate_dmtcp_ckpt = mkCkptFile {
|
|
variant = "multivariate";
|
|
banner = "Preloaded with multivariate analysis";
|
|
loads = ''
|
|
loadt "Multivariate/make.ml";;
|
|
'';
|
|
startCkpt = hol_light_core_dmtcp_ckpt;
|
|
};
|
|
|
|
hol_light_sosa_dmtcp_ckpt = mkCkptFile {
|
|
variant = "sosa";
|
|
banner = "Preloaded with analysis and SOS";
|
|
loads = ''
|
|
loadt "Library/analysis.ml";;
|
|
loadt "Library/transc.ml";;
|
|
loadt "Examples/sos.ml";;
|
|
loadt "update_database.ml";;
|
|
'';
|
|
startCkpt = hol_light_core_dmtcp_ckpt;
|
|
};
|
|
|
|
hol_light_card_dmtcp_ckpt = mkCkptFile {
|
|
variant = "card";
|
|
banner = "Preloaded with cardinal arithmetic";
|
|
loads = ''
|
|
loadt "Library/card.ml";;
|
|
loadt "update_database.ml";;
|
|
'';
|
|
startCkpt = hol_light_core_dmtcp_ckpt;
|
|
};
|
|
|
|
hol_light_complex_dmtcp_ckpt = mkCkptFile {
|
|
variant = "complex";
|
|
banner = "Preloaded with multivariate-based complex analysis";
|
|
loads = ''
|
|
loadt "Multivariate/complexes.ml";;
|
|
loadt "Multivariate/canal.ml";;
|
|
loadt "Multivariate/transcendentals.ml";;
|
|
loadt "Multivariate/realanalysis.ml";;
|
|
loadt "Multivariate/cauchy.ml";;
|
|
loadt "Multivariate/complex_database.ml";;
|
|
'';
|
|
startCkpt = hol_light_multivariate_dmtcp_ckpt;
|
|
};
|
|
}
|