diff options
author | Marco Maggesi <maggesi@math.unifi.it> | 2010-09-15 21:41:18 +0000 |
---|---|---|
committer | Marco Maggesi <maggesi@math.unifi.it> | 2010-09-15 21:41:18 +0000 |
commit | 4e5db40581ed97ec8b7c6d61187f47e5948a3226 (patch) | |
tree | d130f5e15ae3a2f2491851776570448c0b640c29 /pkgs/applications/science/logic | |
parent | 44f2d4439ff9a26b5f2ccf35fe198a2df5f0cbbc (diff) | |
download | nixlib-4e5db40581ed97ec8b7c6d61187f47e5948a3226.tar nixlib-4e5db40581ed97ec8b7c6d61187f47e5948a3226.tar.gz nixlib-4e5db40581ed97ec8b7c6d61187f47e5948a3226.tar.bz2 nixlib-4e5db40581ed97ec8b7c6d61187f47e5948a3226.tar.lz nixlib-4e5db40581ed97ec8b7c6d61187f47e5948a3226.tar.xz nixlib-4e5db40581ed97ec8b7c6d61187f47e5948a3226.tar.zst nixlib-4e5db40581ed97ec8b7c6d61187f47e5948a3226.zip |
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 svn path=/nixpkgs/trunk/; revision=23815
Diffstat (limited to 'pkgs/applications/science/logic')
9 files changed, 216 insertions, 140 deletions
diff --git a/pkgs/applications/science/logic/hol_light/binaries.nix b/pkgs/applications/science/logic/hol_light/binaries.nix deleted file mode 100644 index de89a7a5d4e8..000000000000 --- a/pkgs/applications/science/logic/hol_light/binaries.nix +++ /dev/null @@ -1,60 +0,0 @@ -{stdenv, hol_light, dmtcp}: - -let - 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 hol_light hol_light.ocaml ]; - - buildCommand = '' - HOL_DIR="${hol_light}/src/hol_light" - BIN_DIR="$out/bin" - ensureDir "$BIN_DIR" - - # HOL Light Core - (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 - 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 - 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" - ''; -} diff --git a/pkgs/applications/science/logic/hol_light/default.nix b/pkgs/applications/science/logic/hol_light/default.nix index 48ed8526d25d..932412daf75c 100644 --- a/pkgs/applications/science/logic/hol_light/default.nix +++ b/pkgs/applications/science/logic/hol_light/default.nix @@ -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\"" - - 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 + hol_light_src_dir = "${hol_light_sources}/lib/hol_light/src"; + + 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 @@ soundness. ''; homepage = http://www.cl.cam.ac.uk/~jrh13/hol-light/; license = "BSD"; - ocamlVersions = [ "3.10.0" "3.11.1" ]; }; } diff --git a/pkgs/applications/science/logic/hol_light/dmtcp_checkpoint.nix b/pkgs/applications/science/logic/hol_light/dmtcp_checkpoint.nix new file mode 100644 index 000000000000..9071d63c298a --- /dev/null +++ b/pkgs/applications/science/logic/hol_light/dmtcp_checkpoint.nix @@ -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; + }; +} diff --git a/pkgs/applications/science/logic/hol_light/dmtcp_selfdestruct.ml b/pkgs/applications/science/logic/hol_light/dmtcp_selfdestruct.ml new file mode 100644 index 000000000000..f85a7a6c5fdf --- /dev/null +++ b/pkgs/applications/science/logic/hol_light/dmtcp_selfdestruct.ml @@ -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";; diff --git a/pkgs/applications/science/logic/hol_light/parser_setup.patch b/pkgs/applications/science/logic/hol_light/parser_setup.patch new file mode 100644 index 000000000000..e327527882d6 --- /dev/null +++ b/pkgs/applications/science/logic/hol_light/parser_setup.patch @@ -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. *) diff --git a/pkgs/applications/science/logic/hol_light/restart_hol_light b/pkgs/applications/science/logic/hol_light/restart_hol_light deleted file mode 100644 index d4fe70368d97..000000000000 --- a/pkgs/applications/science/logic/hol_light/restart_hol_light +++ /dev/null @@ -1,3 +0,0 @@ -#!/bin/sh - -exec @DMTCP_RESTART@ --quiet @CKPT_FILE@ diff --git a/pkgs/applications/science/logic/hol_light/sources.nix b/pkgs/applications/science/logic/hol_light/sources.nix new file mode 100644 index 000000000000..497c3d8ff5fd --- /dev/null +++ b/pkgs/applications/science/logic/hol_light/sources.nix @@ -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"; + }; +} diff --git a/pkgs/applications/science/logic/hol_light/start_hol.ml b/pkgs/applications/science/logic/hol_light/start_hol.ml deleted file mode 100644 index c8f4b2279df2..000000000000 --- a/pkgs/applications/science/logic/hol_light/start_hol.ml +++ /dev/null @@ -1,37 +0,0 @@ -(* ========================================================================= *) -(* 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";; diff --git a/pkgs/applications/science/logic/hol_light/start_hol_light b/pkgs/applications/science/logic/hol_light/start_hol_light deleted file mode 100644 index 638cf8d3e772..000000000000 --- a/pkgs/applications/science/logic/hol_light/start_hol_light +++ /dev/null @@ -1,3 +0,0 @@ -#!/bin/sh - -exec @OCAML@/bin/ocaml -I @CAMLP5@/lib/ocaml/camlp5 -I @HOL_DIR@ "$@" |