From 1298fd8aba8637ea0e539b45db4270482d812516 Mon Sep 17 00:00:00 2001 From: Marco Maggesi Date: Sat, 21 May 2011 11:18:35 +0000 Subject: Update hol_light and cleanup: * Update hol_light to rev 90 * Remove dmtcp checkpoint (it doesn't work properly). * General cleanup and simplification svn path=/nixpkgs/trunk/; revision=27290 --- .../science/logic/hol_light/default.nix | 61 ++++++------- .../science/logic/hol_light/dmtcp_checkpoint.nix | 99 ---------------------- .../science/logic/hol_light/dmtcp_selfdestruct.ml | 19 ----- .../science/logic/hol_light/parser_setup.patch | 34 -------- .../science/logic/hol_light/sources.nix | 28 ------ pkgs/top-level/all-packages.nix | 8 +- 6 files changed, 29 insertions(+), 220 deletions(-) delete mode 100644 pkgs/applications/science/logic/hol_light/dmtcp_checkpoint.nix delete mode 100644 pkgs/applications/science/logic/hol_light/dmtcp_selfdestruct.ml delete mode 100644 pkgs/applications/science/logic/hol_light/parser_setup.patch delete mode 100644 pkgs/applications/science/logic/hol_light/sources.nix diff --git a/pkgs/applications/science/logic/hol_light/default.nix b/pkgs/applications/science/logic/hol_light/default.nix index f923095f857..ea68738af57 100644 --- a/pkgs/applications/science/logic/hol_light/default.nix +++ b/pkgs/applications/science/logic/hol_light/default.nix @@ -1,43 +1,36 @@ -{stdenv, writeText, writeTextFile, ocaml, findlib, camlp5_transitional, hol_light_sources}: +{stdenv, fetchsvn, writeScript, ocaml, findlib, camlp5}: -let - version = hol_light_sources.version; +stdenv.mkDerivation rec { + name = "hol_light-20110423"; + src = fetchsvn { + url = http://hol-light.googlecode.com/svn/trunk; + rev = "90"; + sha256 = "e10f32392eb94de559495f2a2977da9e325ff1f39edbcd28db701a1801566c89"; + }; - camlp5 = camlp5_transitional; + buildInputs = [ ocaml findlib camlp5 ]; - hol_light_src_dir = "${hol_light_sources}/lib/hol_light/src"; + start_script = '' + #!/bin/sh + cd "$out/lib/hol_light" + exec ${ocaml}/bin/ocaml -I "$(ocamlfind query camlp5)" -init make.ml + ''; - pa_j_cmo = stdenv.mkDerivation { - name = "pa_j.cmo"; - inherit ocaml camlp5; - buildInputs = [ ocaml camlp5 findlib ]; - buildCommand = '' - ocamlc -c \ - -pp "camlp5r pa_lexer.cmo pa_extend.cmo q_MLast.cmo" \ - -I "$(ocamlfind query camlp5)" \ - -o $out \ - "${hol_light_src_dir}/pa_j_`ocamlc -version | cut -c1-4`.ml" - ''; - }; + buildPhase = '' + make pa_j.ml + ocamlc -c \ + -pp "camlp5r pa_lexer.cmo pa_extend.cmo q_MLast.cmo" \ + -I "$(ocamlfind query camlp5)" \ + pa_j.ml + ''; - start_ml = writeText "start.ml" '' - Topdirs.dir_directory "${hol_light_src_dir}";; - Topdirs.dir_directory ("${camlp5}/lib/ocaml/"^Sys.ocaml_version^"/site-lib/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";; + installPhase = '' + ensureDir "$out/lib/hol_light" "$out/bin" + cp -a . $out/lib/hol_light + echo "${start_script}" > "$out/bin/hol_light" + chmod a+x "$out/bin/hol_light" ''; -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 = '' diff --git a/pkgs/applications/science/logic/hol_light/dmtcp_checkpoint.nix b/pkgs/applications/science/logic/hol_light/dmtcp_checkpoint.nix deleted file mode 100644 index 9071d63c298..00000000000 --- a/pkgs/applications/science/logic/hol_light/dmtcp_checkpoint.nix +++ /dev/null @@ -1,99 +0,0 @@ -{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; - }; -} diff --git a/pkgs/applications/science/logic/hol_light/dmtcp_selfdestruct.ml b/pkgs/applications/science/logic/hol_light/dmtcp_selfdestruct.ml deleted file mode 100644 index f85a7a6c5fd..00000000000 --- a/pkgs/applications/science/logic/hol_light/dmtcp_selfdestruct.ml +++ /dev/null @@ -1,19 +0,0 @@ -(* ------------------------------------------------------------------------- *) -(* 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";; diff --git a/pkgs/applications/science/logic/hol_light/parser_setup.patch b/pkgs/applications/science/logic/hol_light/parser_setup.patch deleted file mode 100644 index 0ad17ca1a0b..00000000000 --- a/pkgs/applications/science/logic/hol_light/parser_setup.patch +++ /dev/null @@ -1,34 +0,0 @@ -diff -Nuar hol_light/hol.ml hol_light.nixos/hol.ml ---- hol_light/hol.ml 2010-11-03 23:09:01.000000000 +0100 -+++ hol_light.nixos/hol.ml 2010-11-03 23:10:31.000000000 +0100 -@@ -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,19 +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" --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. *) diff --git a/pkgs/applications/science/logic/hol_light/sources.nix b/pkgs/applications/science/logic/hol_light/sources.nix deleted file mode 100644 index c6bf6592876..00000000000 --- a/pkgs/applications/science/logic/hol_light/sources.nix +++ /dev/null @@ -1,28 +0,0 @@ -{stdenv, fetchsvn}: - -stdenv.mkDerivation rec { - name = "hol_light_sources-${version}"; - version = "20110417"; - - src = fetchsvn { - url = http://hol-light.googlecode.com/svn/trunk; - rev = "89"; - sha256 = "a14a7ce61002443daac85583362f9f6f5509b22d441effaeb378e0f2c29185e5"; - }; - - 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"; - }; -} diff --git a/pkgs/top-level/all-packages.nix b/pkgs/top-level/all-packages.nix index fdc05669ce1..72dc23bf5d3 100644 --- a/pkgs/top-level/all-packages.nix +++ b/pkgs/top-level/all-packages.nix @@ -7649,14 +7649,10 @@ let hol = callPackage ../applications/science/logic/hol { }; hol_light = callPackage ../applications/science/logic/hol_light { - inherit (ocamlPackages) findlib camlp5_transitional; + inherit (ocamlPackages) findlib; + camlp5 = ocamlPackages.camlp5_strict; }; - 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; inherit (pkgs.emacs23Packages) proofgeneral; -- cgit 1.4.1