Author: maggesi
Date: Wed Sep 8 13:07:45 2010
New Revision: 23685
URL: https://svn.nixos.org/websvn/nix/?rev=23685&sc=1
Log:
Improve hol_light:
* Upgrade hol_light to the latest svn version on google code (r57).
* Improve and semplify the mechanism for the generation of checkpointed
binaries.
* Make hol to work with camlp5 and thus with recent version of ocaml
(>=3.10, <=3.11).
* Remove ocaml_with_sources which is not needed anymore.
Added:
nixpkgs/trunk/pkgs/applications/science/logic/hol_light/restart_hol_light
nixpkgs/trunk/pkgs/applications/science/logic/hol_light/start_hol.ml
nixpkgs/trunk/pkgs/applications/science/logic/hol_light/start_hol_light
Deleted:
nixpkgs/trunk/pkgs/applications/science/logic/hol_light/configure-3.09.3
nixpkgs/trunk/pkgs/applications/science/logic/hol_light/ocaml-with-sources.nix
nixpkgs/trunk/pkgs/applications/science/logic/hol_light/selfcheckpoint_complex.ml
nixpkgs/trunk/pkgs/applications/science/logic/hol_light/selfcheckpoint_core.ml
nixpkgs/trunk/pkgs/applications/science/logic/hol_light/selfcheckpoint_multivariate.ml
Modified:
nixpkgs/trunk/pkgs/applications/science/logic/hol_light/binaries.nix
nixpkgs/trunk/pkgs/applications/science/logic/hol_light/default.nix
nixpkgs/trunk/pkgs/top-level/all-packages.nix
Modified: nixpkgs/trunk/pkgs/applications/science/logic/hol_light/binaries.nix
==============================================================================
--- nixpkgs/trunk/pkgs/applications/science/logic/hol_light/binaries.nix
Wed Sep 8 11:40:32 2010 (r23684)
+++ nixpkgs/trunk/pkgs/applications/science/logic/hol_light/binaries.nix
Wed Sep 8 13:07:45 2010 (r23685)
@@ -1,55 +1,60 @@
-{stdenv, ocaml_with_sources, hol_light, dmtcp, nettools, openssh}:
-# nettools and openssh needed for dmtcp restarting script.
+{stdenv, hol_light, dmtcp}:
let
- selfcheckpoint_core_ml = ./selfcheckpoint_core.ml;
- selfcheckpoint_multivariate_ml = ./selfcheckpoint_multivariate.ml;
- selfcheckpoint_complex_ml = ./selfcheckpoint_complex.ml;
+ cmd_core = ''
+ #use "${./start_hol.ml}";;
+ dmtcp_selfdestruct "";;
+ '';
+ cmd_multivariate = ''
+ loadt "Multivariate/make.ml";;
+ dmtcp_checkpoint "Preloaded with multivariate analysis";;
+ '';
+ cmd_complex = ''
+ 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";;
+ loadt "update_database.ml";;
+ dmtcp_checkpoint "Preloaded with multivariate-based complex analysis";;
+ '';
in
stdenv.mkDerivation {
name = "hol_light_binaries-${hol_light.version}";
- buildInputs = [ dmtcp ocaml_with_sources nettools openssh];
+ buildInputs = [ dmtcp hol_light hol_light.ocaml ];
buildCommand = ''
- HOL_DIR=${hol_light}/src/hol_light
- BIN_DIR=$out/bin
- ensureDir $BIN_DIR
+ HOL_DIR="${hol_light}/src/hol_light"
+ BIN_DIR="$out/bin"
+ ensureDir "$BIN_DIR"
# HOL Light Core
- dmtcp_coordinator --background
- echo 'Unix.system "dmtcp_command -k";;\n' |
- dmtcp_checkpoint -q -c "$BIN_DIR" \
- ocaml -I "$HOL_DIR" -init ${selfcheckpoint_core_ml}
- substituteInPlace dmtcp_restart_script.sh \
- --replace dmtcp_restart "dmtcp_restart --quiet"
- mv dmtcp_restart_script.sh $BIN_DIR/hol_light
- dmtcp_command -q
+ (echo '${cmd_core}' | dmtcp_checkpoint --quiet
${hol_light}/bin/start_hol_light) || exit 0
+ mv ckpt* "$BIN_DIR/hol_light.ckpt"
+ substitute "${./restart_hol_light}" "$BIN_DIR/hol_light" \
+ --subst-var-by DMTCP_RESTART `type -p dmtcp_restart` \
+ --subst-var-by CKPT_FILE "$BIN_DIR/hol_light.ckpt"
+ chmod +x "$BIN_DIR/hol_light"
# HOL Light Multivariate
- dmtcp_coordinator --background
- echo 'Unix.system "dmtcp_command -k";;\n' |
- dmtcp_checkpoint -q -c "$BIN_DIR" \
- ocaml -I "$HOL_DIR" -init ${selfcheckpoint_multivariate_ml}
- substituteInPlace dmtcp_restart_script.sh \
- --replace dmtcp_restart "dmtcp_restart --quiet"
- mv dmtcp_restart_script.sh $BIN_DIR/hol_light_multivariate
- dmtcp_command -q
+ cp "$BIN_DIR/hol_light.ckpt" .
+ (echo '${cmd_multivariate}' | dmtcp_restart --quiet hol_light.ckpt) ||
exit 0
+ mv hol_light.ckpt "$BIN_DIR/hol_light_multivariate.ckpt"
+ substitute "${./restart_hol_light}" "$BIN_DIR/hol_light_multivariate" \
+ --subst-var-by DMTCP_RESTART `type -p dmtcp_restart` \
+ --subst-var-by CKPT_FILE "$BIN_DIR/hol_light_multivariate.ckpt"
+ chmod +x "$BIN_DIR/hol_light_multivariate"
# HOL Light Complex
- dmtcp_coordinator --background
- echo 'Unix.system "dmtcp_command -k";;\n' |
- dmtcp_checkpoint -q -c "$BIN_DIR" \
- ocaml -I "$HOL_DIR" -init ${selfcheckpoint_complex_ml}
- substituteInPlace dmtcp_restart_script.sh \
- --replace dmtcp_restart "dmtcp_restart --quiet"
- mv dmtcp_restart_script.sh $BIN_DIR/hol_light_complex
- dmtcp_command -q
+ cp "$BIN_DIR/hol_light_multivariate.ckpt" .
+ (echo '${cmd_complex}' | dmtcp_restart --quiet
hol_light_multivariate.ckpt) || exit 0
+ mv hol_light_multivariate.ckpt "$BIN_DIR/hol_light_complex.ckpt"
+ substitute "${./restart_hol_light}" "$BIN_DIR/hol_light_complex" \
+ --subst-var-by DMTCP_RESTART `type -p dmtcp_restart` \
+ --subst-var-by CKPT_FILE "$BIN_DIR/hol_light_complex.ckpt"
+ chmod +x "$BIN_DIR/hol_light_complex"
'';
-
- meta = {
- description = "Preload binaries for HOL Light.";
- license = "BSD";
- };
}
Modified: nixpkgs/trunk/pkgs/applications/science/logic/hol_light/default.nix
==============================================================================
--- nixpkgs/trunk/pkgs/applications/science/logic/hol_light/default.nix Wed Sep
8 11:40:32 2010 (r23684)
+++ nixpkgs/trunk/pkgs/applications/science/logic/hol_light/default.nix Wed Sep
8 13:07:45 2010 (r23685)
@@ -1,56 +1,40 @@
-{stdenv, fetchurl, ocaml_with_sources}:
+{stdenv, fetchsvn, ocaml, camlp5_transitional}:
-let
- pname = "hol_light";
- version = "100110";
- webpage = http://www.cl.cam.ac.uk/~jrh13/hol-light/;
-
- dmtcp_checkpoint = ''
-
-(* ------------------------------------------------------------------------- *)
-(* Non-destructive checkpoint using DMTCP. *)
-(* ------------------------------------------------------------------------- *)
-
-let dmtcp_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(); Unix.sleep 1;
- try ignore(Unix.system ("dmtcp_command -bc")) with _ -> ();
- Format.print_string complete_banner;
- Format.print_newline(); Format.print_newline());;
- '';
-
-in
-
-stdenv.mkDerivation {
- name = "${pname}-${version}";
- inherit version;
-
- src = fetchurl {
- url = "${webpage}${pname}_${version}.tgz";
- sha256 = "1jkn9vpl3n9dgb96zwmly32h1p3f9mcf34pg6vm0fyvqp9kbx3ac";
+stdenv.mkDerivation rec {
+ name = "hol_light-${version}";
+ version = "20100820svn57";
+
+ inherit ocaml;
+ camlp5 = camlp5_transitional;
+
+ src = fetchsvn {
+ url = http://hol-light.googlecode.com/svn/trunk;
+ rev = "57";
+ sha256 =
"d1372744abca6c9978673850977d3e1577fd8cfd8298826eb713b3681c10cccd";
};
- buildInputs = [ ocaml_with_sources ];
+ buildInputs = [ ocaml camlp5 ];
buildCommand = ''
- ensureDir "$out/src"
- cd "$out/src"
-
- tar -xzf "$src"
- cd hol_light
+ export HOL_DIR="$out/src/hol_light"
+ ensureDir `dirname $HOL_DIR` "$out/bin"
+ cp -a "${src}" "$HOL_DIR"
+ cd "$HOL_DIR"
+ chmod -R u+rwX .
substituteInPlace hol.ml --replace \
"(try Sys.getenv \"HOLLIGHT_DIR\" with Not_found -> Sys.getcwd())" \
- "\"$out/src/hol_light\""
-
- substituteInPlace Examples/update_database.ml --replace \
- "Filename.concat ocaml_source_dir" \
- "Filename.concat \"${ocaml_with_sources}/src/ocaml\""
+ "\"$HOL_DIR\""
- echo '${dmtcp_checkpoint}' >> make.ml
+ substituteInPlace Makefile --replace \
+ "+camlp5" \
+ "${camlp5}/lib/ocaml/camlp5"
+
+ substitute ${./start_hol_light} "$out/bin/start_hol_light" \
+ --subst-var-by OCAML "${ocaml}" \
+ --subst-var-by CAMLP5 "${camlp5_transitional}" \
+ --subst-var HOL_DIR
+ chmod +x "$out/bin/start_hol_light"
make
'';
@@ -66,7 +50,8 @@
can extend it with new theorems and inference rules without compromising its
soundness.
'';
- homepage = webpage;
+ homepage = http://www.cl.cam.ac.uk/~jrh13/hol-light/;
license = "BSD";
+ ocamlVersions = [ "3.10.0" "3.11.1" ];
};
}
Added: nixpkgs/trunk/pkgs/applications/science/logic/hol_light/restart_hol_light
==============================================================================
--- /dev/null 00:00:00 1970 (empty, because file is newly added)
+++ nixpkgs/trunk/pkgs/applications/science/logic/hol_light/restart_hol_light
Wed Sep 8 13:07:45 2010 (r23685)
@@ -0,0 +1,3 @@
+#!/bin/sh
+
+exec @DMTCP_RESTART@ --quiet @CKPT_FILE@
Added: nixpkgs/trunk/pkgs/applications/science/logic/hol_light/start_hol.ml
==============================================================================
--- /dev/null 00:00:00 1970 (empty, because file is newly added)
+++ nixpkgs/trunk/pkgs/applications/science/logic/hol_light/start_hol.ml
Wed Sep 8 13:07:45 2010 (r23685)
@@ -0,0 +1,37 @@
+(* ========================================================================= *)
+(* 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 this instead of #use "make.ml";; for quick tests. *)
+(*
+let a = 1;
+#load "unix.cma";;
+let startup_banner = "Bogus banner\n";;
+Format.print_string "Hello!"; Format.print_newline();;
+*)
+
+#use "make.ml";;
+
+(* ------------------------------------------------------------------------- *)
+(* Checkpoint using DMTCP. *)
+(* dmtcp_selfdestruct is similar to dmtcp_checkpoint but terminates *)
+(* HOL Light and shuts down the dmtcp coordinator. *)
+(* ------------------------------------------------------------------------- *)
+
+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 4;
+ Format.print_string "Checkpointing..."; Format.print_newline();
+ try ignore(Unix.system ("dmtcp_command -bc " ^ opts)) with _ -> ();
+ Format.print_string complete_banner;
+ Format.print_newline(); Format.print_newline())
+ in
+ call_dmtcp "", call_dmtcp "-q";;
Added: nixpkgs/trunk/pkgs/applications/science/logic/hol_light/start_hol_light
==============================================================================
--- /dev/null 00:00:00 1970 (empty, because file is newly added)
+++ nixpkgs/trunk/pkgs/applications/science/logic/hol_light/start_hol_light
Wed Sep 8 13:07:45 2010 (r23685)
@@ -0,0 +1,3 @@
+#!/bin/sh
+
+exec @OCAML@/bin/ocaml -I @CAMLP5@/lib/ocaml/camlp5 -I @HOL_DIR@ "$@"
Modified: nixpkgs/trunk/pkgs/top-level/all-packages.nix
==============================================================================
--- nixpkgs/trunk/pkgs/top-level/all-packages.nix Wed Sep 8 11:40:32
2010 (r23684)
+++ nixpkgs/trunk/pkgs/top-level/all-packages.nix Wed Sep 8 13:07:45
2010 (r23685)
@@ -6783,11 +6783,6 @@
hol_light_binaries = callPackage
../applications/science/logic/hol_light/binaries.nix { };
- # This is a special version of OCaml handcrafted especially for
- # hol_light it should be merged with the current expresion for ocaml
- # one day.
- ocaml_with_sources = callPackage
../applications/science/logic/hol_light/ocaml-with-sources.nix { };
-
isabelle = import ../applications/science/logic/isabelle {
inherit (pkgs) stdenv fetchurl nettools perl polyml;
inherit (pkgs.emacs23Packages) proofgeneral;
_______________________________________________
nix-commits mailing list
[email protected]
http://mail.cs.uu.nl/mailman/listinfo/nix-commits
