Author: maggesi
Date: Wed Sep 15 21:41:18 2010
New Revision: 23815
URL: https://svn.nixos.org/websvn/nix/?rev=23815&sc=1
Log:
Update HOL Light to version 20100820 (rev57 on google code).
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
Added:
nixpkgs/trunk/pkgs/applications/science/logic/hol_light/dmtcp_checkpoint.nix
nixpkgs/trunk/pkgs/applications/science/logic/hol_light/dmtcp_selfdestruct.ml
nixpkgs/trunk/pkgs/applications/science/logic/hol_light/parser_setup.patch
nixpkgs/trunk/pkgs/applications/science/logic/hol_light/sources.nix
Deleted:
nixpkgs/trunk/pkgs/applications/science/logic/hol_light/binaries.nix
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
Modified:
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/default.nix
==============================================================================
--- nixpkgs/trunk/pkgs/applications/science/logic/hol_light/default.nix Wed Sep
15 21:36:56 2010 (r23814)
+++ nixpkgs/trunk/pkgs/applications/science/logic/hol_light/default.nix Wed Sep
15 21:41:18 2010 (r23815)
@@ -1,44 +1,43 @@
-{stdenv, fetchsvn, ocaml, camlp5_transitional}:
+{stdenv, writeText, writeTextFile, ocaml, camlp5_transitional,
hol_light_sources}:
-stdenv.mkDerivation rec {
- name = "hol_light-${version}";
- version = "20100820svn57";
+let
+ version = hol_light_sources.version;
- inherit ocaml;
camlp5 = camlp5_transitional;
- src = fetchsvn {
- url = http://hol-light.googlecode.com/svn/trunk;
- rev = "57";
- sha256 =
"d1372744abca6c9978673850977d3e1577fd8cfd8298826eb713b3681c10cccd";
- };
-
- buildInputs = [ ocaml camlp5 ];
-
- buildCommand = ''
- 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())" \
- "\"$HOL_DIR\""
+ hol_light_src_dir = "${hol_light_sources}/lib/hol_light/src";
- 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
+ pa_j_cmo = stdenv.mkDerivation {
+ name = "pa_j.cmo";
+ inherit ocaml camlp5;
+ buildInputs = [ ocaml camlp5 ];
+ buildCommand = ''
+ ocamlc -c \
+ -pp "camlp5r pa_lexer.cmo pa_extend.cmo q_MLast.cmo" \
+ -I "${camlp5}/lib/ocaml/camlp5" \
+ -o $out \
+ "${hol_light_src_dir}/pa_j_`ocamlc -version | cut -c1-4`.ml"
+ '';
+ };
+
+ start_ml = writeText "start.ml" ''
+ Topdirs.dir_directory "${hol_light_src_dir}";;
+ Topdirs.dir_directory "${camlp5}/lib/ocaml/camlp5";;
+ Topdirs.dir_load Format.std_formatter "camlp5o.cma";;
+ Topdirs.dir_load Format.std_formatter "${pa_j_cmo}";;
+ #use "${hol_light_src_dir}/make.ml";;
'';
-
+in
+writeTextFile {
+ name = "hol_light-${version}";
+ destination = "/bin/start_hol_light";
+ executable = true;
+ text = ''
+ #!/bin/sh
+ exec ${ocaml}/bin/ocaml -init ${start_ml}
+ '';
+} // {
+ inherit (hol_light_sources) version src;
meta = {
description = "An interactive theorem prover based on Higher-Order Logic.";
longDescription = ''
@@ -52,6 +51,5 @@
'';
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/dmtcp_checkpoint.nix
==============================================================================
--- /dev/null 00:00:00 1970 (empty, because file is newly added)
+++
nixpkgs/trunk/pkgs/applications/science/logic/hol_light/dmtcp_checkpoint.nix
Wed Sep 15 21:41:18 2010 (r23815)
@@ -0,0 +1,99 @@
+{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;
+ };
+}
Added:
nixpkgs/trunk/pkgs/applications/science/logic/hol_light/dmtcp_selfdestruct.ml
==============================================================================
--- /dev/null 00:00:00 1970 (empty, because file is newly added)
+++
nixpkgs/trunk/pkgs/applications/science/logic/hol_light/dmtcp_selfdestruct.ml
Wed Sep 15 21:41:18 2010 (r23815)
@@ -0,0 +1,19 @@
+(* ------------------------------------------------------------------------- *)
+(* 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";;
Added:
nixpkgs/trunk/pkgs/applications/science/logic/hol_light/parser_setup.patch
==============================================================================
--- /dev/null 00:00:00 1970 (empty, because file is newly added)
+++ nixpkgs/trunk/pkgs/applications/science/logic/hol_light/parser_setup.patch
Wed Sep 15 21:41:18 2010 (r23815)
@@ -0,0 +1,35 @@
+diff -Nuar hol_light/hol.ml hol_light.nixos/hol.ml
+--- hol_light/hol.ml 2010-09-12 18:57:28.000000000 +0200
++++ hol_light.nixos/hol.ml 2010-09-12 19:09:09.000000000 +0200
+@@ -11,8 +11,8 @@
+
+ let hol_version = "2.20++";;
+
+-let hol_dir = ref
+- (try Sys.getenv "HOLLIGHT_DIR" with Not_found -> Sys.getcwd());;
++let hol_dir = ref "@HOL_LIGHT_SRC_DIR@";;
++Topdirs.dir_directory "@HOL_LIGHT_SRC_DIR@";;
+
+ (* -------------------------------------------------------------------------
*)
+ (* Should eventually change to "ref(Filename.temp_dir_name)".
*)
+@@ -23,20 +23,6 @@
+ let temp_path = ref "/tmp";;
+
+ (* -------------------------------------------------------------------------
*)
+-(* Load in parsing extensions.
*)
+-(* For Ocaml < 3.10, use the built-in camlp4
*)
+-(* and for Ocaml >= 3.10, use camlp5 instead.
*)
+-(* -------------------------------------------------------------------------
*)
+-
+-if let v = String.sub Sys.ocaml_version 0 4 in
+- v = "3.10" or v = "3.11"
+-then (Topdirs.dir_directory "+camlp5";
+- Topdirs.dir_load Format.std_formatter "camlp5o.cma")
+-else (Topdirs.dir_load Format.std_formatter "camlp4o.cma");;
+-
+-Topdirs.dir_load Format.std_formatter (Filename.concat (!hol_dir)
"pa_j.cmo");;
+-
+-(* -------------------------------------------------------------------------
*)
+ (* Load files from system and/or user-settable directories.
*)
+ (* Paths map initial "$/" to !hol_dir dynamically; use $$ to get the actual
*)
+ (* $ character at the start of a directory.
*)
Added: nixpkgs/trunk/pkgs/applications/science/logic/hol_light/sources.nix
==============================================================================
--- /dev/null 00:00:00 1970 (empty, because file is newly added)
+++ nixpkgs/trunk/pkgs/applications/science/logic/hol_light/sources.nix Wed Sep
15 21:41:18 2010 (r23815)
@@ -0,0 +1,28 @@
+{stdenv, fetchsvn}:
+
+stdenv.mkDerivation rec {
+ name = "hol_light_sources-${version}";
+ version = "20100820";
+
+ src = fetchsvn {
+ url = http://hol-light.googlecode.com/svn/trunk;
+ rev = "57";
+ sha256 =
"d1372744abca6c9978673850977d3e1577fd8cfd8298826eb713b3681c10cccd";
+ };
+
+ buildCommand = ''
+ export HOL_DIR="$out/lib/hol_light"
+ ensureDir "$HOL_DIR"
+ cp -a "${src}" "$HOL_DIR/src"
+ cd "$HOL_DIR/src"
+ chmod +wX -R .
+ patch -p1 < ${./parser_setup.patch}
+ substituteInPlace hol.ml --subst-var-by HOL_LIGHT_SRC_DIR "$HOL_DIR/src"
+ '';
+
+ meta = {
+ description = "Sources for the HOL Light theorem prover";
+ homepage = http://www.cl.cam.ac.uk/~jrh13/hol-light/;
+ license = "BSD";
+ };
+}
Modified: nixpkgs/trunk/pkgs/top-level/all-packages.nix
==============================================================================
--- nixpkgs/trunk/pkgs/top-level/all-packages.nix Wed Sep 15 21:36:56
2010 (r23814)
+++ nixpkgs/trunk/pkgs/top-level/all-packages.nix Wed Sep 15 21:41:18
2010 (r23815)
@@ -6691,7 +6691,10 @@
hol_light = callPackage ../applications/science/logic/hol_light { };
- hol_light_binaries = callPackage
../applications/science/logic/hol_light/binaries.nix { };
+ hol_light_sources = callPackage
../applications/science/logic/hol_light/sources.nix { };
+
+ hol_light_checkpoint_dmtcp =
+ recurseIntoAttrs (callPackage
../applications/science/logic/hol_light/dmtcp_checkpoint.nix { });
isabelle = import ../applications/science/logic/isabelle {
inherit (pkgs) stdenv fetchurl nettools perl polyml;
_______________________________________________
nix-commits mailing list
[email protected]
http://mail.cs.uu.nl/mailman/listinfo/nix-commits
