From d4a1e280bbb1b81b137157f98b7f3605666f4b23 Mon Sep 17 00:00:00 2001 From: Mark A. Hillebrand Date: Sun, 28 Dec 2008 11:57:17 +0100 Subject: [PATCH] Support Proof General 3.7.1 and Poly/ML 5.2.1 with Isabelle-2005: * Updated the Poly/ML runtime system version detection script lib/scripts/polyml-version to the version from the Isabelle-2008 distribution. * Updated the Poly/ML platform detection script lib/scripts/polyml-platform to the version from the Isabelle-2008 distribution. * Added Poly/ML 5.1/5.2 startup script lib/scripts/run-polyml-5.2 from the Isabelle-2008 distribution (known there as lib/scripts/run-polyml). * Added Poly/ML 5.2 compability file src/Pure/ML-Systems/polyml-5.2.ML thankfully provided by Makarius Wenzel. * Adapted etc/settings to Proof General 3.7, patch by Makarius Wenzel, see http://isabelle.in.tum.de/repos/isabelle/rev/9053fd546501 * Provided wrappers for Poly/ML 5.2.1 --- NEWS | 3 + etc/settings | 5 +- lib/scripts/polyml-platform | 15 ++- lib/scripts/polyml-version | 13 ++- lib/scripts/run-polyml-5.2 | 84 +++++++++++++ lib/scripts/run-polyml-5.2.1 | 3 + src/Pure/ML-Systems/polyml-5.2.1.ML | 5 + src/Pure/ML-Systems/polyml-5.2.ML | 224 +++++++++++++++++++++++++++++++++++ 8 files changed, 344 insertions(+), 8 deletions(-) create mode 100755 lib/scripts/run-polyml-5.2 create mode 100755 lib/scripts/run-polyml-5.2.1 create mode 100644 src/Pure/ML-Systems/polyml-5.2.1.ML create mode 100644 src/Pure/ML-Systems/polyml-5.2.ML diff --git a/NEWS b/NEWS index 4633194..e8806c5 100644 --- a/NEWS +++ b/NEWS @@ -970,6 +970,9 @@ generated HTML files. For example: *** System *** +* Default settings: PROOFGENERAL_OPTIONS no longer impose xemacs here +--- in accordance with Proof General 3.7, which prefers GNU emacs. + * Allow symlinks to all proper Isabelle executables (Isabelle, isabelle, isatool etc.). diff --git a/etc/settings b/etc/settings index 2d26da7..c2ef72e 100644 --- a/etc/settings +++ b/etc/settings @@ -155,10 +155,7 @@ ISABELLE_INTERFACE=$(choosefrom \ "$ISABELLE_INTERFACE") PROOFGENERAL_OPTIONS="" -#PROOFGENERAL_OPTIONS="-m no_brackets -m no_type_brackets -x true -p xemacs" - -type -path xemacs >/dev/null || \ - PROOFGENERAL_OPTIONS="-p emacs $PROOFGENERAL_OPTIONS" +#PROOFGENERAL_OPTIONS="-m no_brackets -m no_type_brackets -x true -p emacs22" # Automatic setup of remote fonts #XSYMBOL_INSTALLFONTS="xset fp+ tcp/isafonts.informatik.tu-muenchen.de:7200" diff --git a/lib/scripts/polyml-platform b/lib/scripts/polyml-platform index 1f63ca0..b8c281f 100755 --- a/lib/scripts/polyml-platform +++ b/lib/scripts/polyml-platform @@ -1,6 +1,6 @@ #!/usr/bin/env bash # -# $Id: polyml-platform,v 1.1 2005/08/01 17:20:48 wenzelm Exp $ +# $Id: polyml-platform,v 1.6 2007/11/08 19:07:58 wenzelm Exp $ # # polyml-platform --- determine Poly/ML's idea of current hardware and # operating system type @@ -18,6 +18,9 @@ case $(uname -s) in sparc) PLATFORM=sparc-solaris ;; + i?86) + PLATFORM=x86-solaris + ;; esac ;; esac @@ -44,6 +47,16 @@ case $(uname -s) in Power* | power* | ppc) PLATFORM=ppc-darwin ;; + i?86) + PLATFORM=x86-darwin + ;; + esac + ;; + CYGWIN_NT*) + case $(uname -m) in + i?86) + PLATFORM=x86-cygwin + ;; esac ;; Windows_NT) diff --git a/lib/scripts/polyml-version b/lib/scripts/polyml-version index 2b3f1f5..919ce77 100755 --- a/lib/scripts/polyml-version +++ b/lib/scripts/polyml-version @@ -1,12 +1,19 @@ #!/usr/bin/env bash # -# $Id: polyml-version,v 1.2 2005/09/15 15:18:57 wenzelm Exp $ +# $Id: polyml-version,v 1.5 2006/12/05 17:32:54 wenzelm Exp $ # # polyml-version --- determine Poly/ML runtime system version echo -n polyml if [ -x "$ML_HOME/poly" ]; then - "$ML_HOME/poly" -noDisplay -r /dev/null | head -n 1 | \ - sed -n 's,^Poly/ML RTS version [^ ]*\(-[^ ]*\).*$,\1,p' + if [ -x "$ML_HOME/polyimport" ]; then + env LD_LIBRARY_PATH="$ML_HOME:$ML_HOME/../lib:$LD_LIBRARY_PATH" \ + DYLD_LIBRARY_PATH="$ML_HOME:$ML_HOME/../lib:$DYLD_LIBRARY_PATH" \ + "$ML_HOME/poly" -v | \ + sed -n 's,^Poly/ML.*RTS version: [^ ]*\(-[^ ]*\).*$,\1,p' + else + "$ML_HOME/poly" -noDisplay -r /dev/null | head -n 1 | \ + sed -n 's,^Poly/ML RTS version [^ ]*\(-[^ ]*\).*$,\1,p' + fi fi diff --git a/lib/scripts/run-polyml-5.2 b/lib/scripts/run-polyml-5.2 new file mode 100755 index 0000000..c72370c --- /dev/null +++ b/lib/scripts/run-polyml-5.2 @@ -0,0 +1,84 @@ +#!/usr/bin/env bash +# +# $Id: run-polyml,v 1.43 2008/04/24 14:53:06 haftmann Exp $ +# Author: Makarius +# +# Poly/ML 5.1/5.2 startup script. + +export -n INFILE OUTFILE COPYDB COMPRESS MLTEXT TERMINATE NOWRITE + + +## diagnostics + +function fail_out() +{ + echo "Unable to create output heap file: \"$OUTFILE\"" >&2 + exit 2 +} + +function check_file() +{ + if [ ! -f "$1" ]; then + echo "Unable to locate $1" >&2 + echo "Please check your ML system settings!" >&2 + exit 2 + fi +} + + +## compiler executables and libraries + +POLY="$ML_HOME/poly" +check_file "$POLY" + +if [ "$(basename "$ML_HOME")" = bin ]; then + POLYLIB="$(cd "$ML_HOME"; cd "$(pwd -P)"; cd ../lib; pwd)" +else + POLYLIB="$ML_HOME" +fi + +export LD_LIBRARY_PATH="$POLYLIB:$LD_LIBRARY_PATH" +export DYLD_LIBRARY_PATH="$POLYLIB:$DYLD_LIBRARY_PATH" + + +## prepare databases + +if [ -z "$INFILE" ]; then + INIT="" + EXIT="fun exit 0 = (OS.Process.exit OS.Process.success): unit | exit _ = OS.Process.exit OS.Process.failure;" +else + check_file "$INFILE" + INIT="(Signal.signal (2, Signal.SIG_HANDLE (fn _ => Process.interruptConsoleProcesses ())); PolyML.SaveState.loadState \"$INFILE\" handle Fail msg => (TextIO.output (TextIO.stdErr, msg ^ \"\\n\"); OS.Process.exit OS.Process.failure));" + EXIT="" +fi + +if [ -z "$OUTFILE" ]; then + COMMIT='fun commit () = (TextIO.output (TextIO.stdErr, "Error - Database is not opened for writing.\n"); false);' +else + if [ -z "$COMPRESS" ]; then + COMMIT="fun commit () = (TextIO.output (TextIO.stdOut, \"Exporting $OUTFILE\n\"); PolyML.SaveState.saveState \"$OUTFILE\"; true);" + else + COMMIT="fun commit () = (PolyML.shareCommonData PolyML.rootFunction; TextIO.output (TextIO.stdOut, \"Exporting $OUTFILE\n\"); PolyML.SaveState.saveState \"$OUTFILE\"; true);" + fi + [ -f "$OUTFILE" ] && { chmod +w "$OUTFILE" || fail_out; } +fi + + +## run it! + +MLTEXT="$INIT $EXIT $COMMIT $MLTEXT" +MLEXIT="commit();" + +if [ -z "$TERMINATE" ]; then + FEEDER_OPTS="" +else + FEEDER_OPTS="-q" +fi + +"$ISABELLE_HOME/lib/scripts/feeder" -p -h "$MLTEXT" -t "$MLEXIT" $FEEDER_OPTS | \ + { read FPID; "$POLY" -q $ML_OPTIONS; RC="$?"; kill -HUP "$FPID"; exit "$RC"; } +RC="$?" + +[ -n "$OUTFILE" -a -f "$OUTFILE" -a -n "$NOWRITE" ] && chmod -w "$OUTFILE" + +exit "$RC" diff --git a/lib/scripts/run-polyml-5.2.1 b/lib/scripts/run-polyml-5.2.1 new file mode 100755 index 0000000..7e5eb5a --- /dev/null +++ b/lib/scripts/run-polyml-5.2.1 @@ -0,0 +1,3 @@ +#!/usr/bin/env bash +# Poly/ML 5.2.1 startup script. +exec "$ISABELLE_HOME/lib/scripts/run-polyml-5.2" "$@" diff --git a/src/Pure/ML-Systems/polyml-5.2.1.ML b/src/Pure/ML-Systems/polyml-5.2.1.ML new file mode 100644 index 0000000..24bafe3 --- /dev/null +++ b/src/Pure/ML-Systems/polyml-5.2.1.ML @@ -0,0 +1,5 @@ +(* Title: Pure/ML-Systems/polyml-5.2.1.ML + +Compatibility file for Poly/ML 5.2.1. +*) +use "ML-Systems/polyml-5.2.ML"; diff --git a/src/Pure/ML-Systems/polyml-5.2.ML b/src/Pure/ML-Systems/polyml-5.2.ML new file mode 100644 index 0000000..af888b4 --- /dev/null +++ b/src/Pure/ML-Systems/polyml-5.2.ML @@ -0,0 +1,224 @@ +(* Title: Pure/ML-Systems/polyml-5.2.ML + Author: Makarius + +Compatibility file for Poly/ML 5.2. +*) + +(** ML system and platform related **) + +(* Basis compatibility *) + +structure Posix = +struct + open Posix; + structure IO = + struct + open IO; + val mkReader = mkTextReader; + val mkWriter = mkTextWriter; + end; +end; + +structure TextIO = +struct + open TextIO; + fun inputLine is = Option.getOpt (TextIO.inputLine is, ""); +end; + +structure Substring = +struct + open Substring; + val all = full; +end; + +structure String = +struct + fun isSuffix s1 s2 = + let val n1 = size s1 and n2 = size s2 + in if n1 = n2 then s1 = s2 else n1 <= n2 andalso String.substring (s2, n2 - n1, n1) = s1 end; + open String; +end; + + +(* cygwin *) + +val cygwin_platform = String.isSuffix "cygwin" ml_platform; +fun if_cygwin f x = if cygwin_platform then f x else (); +fun unless_cygwin f x = if not cygwin_platform then f x else (); + + +(*low-level pointer equality*) +val pointer_eq = PolyML.pointerEq; + + +(* old Poly/ML emulation *) + +local + val orig_exit = exit; +in + open PolyML; + val exit = orig_exit; + fun quit () = exit 0; +end; + + +(* restore old-style character / string functions *) + +val ord = SML90.ord; +val chr = SML90.chr; +val explode = SML90.explode; +val implode = SML90.implode; + + +(* compiler-independent timing functions *) + +use "ML-Systems/cpu-timer-basis.ML"; + + +(* bounded time execution *) + +unless_cygwin + use "ML-Systems/polyml-time-limit.ML"; + + +(* prompts *) + +fun ml_prompts p1 p2 = (PolyML.Compiler.prompt1 := p1; PolyML.Compiler.prompt2 := p2); + + +(* toplevel pretty printing (see also Pure/install_pp.ML) *) + +fun make_pp _ pprint (str, blk, brk, en) _ _ obj = + pprint obj (str, fn ind => blk (ind, false), fn wd => brk (wd, 0), + fn () => brk (99999, 0), en); + + +(* ML command execution -- 'eval' *) + +local + +fun drop_newline s = + if String.isSuffix "\n" s then String.substring (s, 0, size s - 1) + else s; + +in + +fun use_text (print, err) verbose txt = + let + val current_line = ref 1; + val in_buffer = ref (String.explode txt); + val out_buffer = ref ([]: string list); + fun output () = drop_newline (implode (rev (! out_buffer))); + + fun get () = + (case ! in_buffer of + [] => NONE + | c :: cs => + (in_buffer := cs; if c = #"\n" then current_line := ! current_line + 1 else (); SOME c)); + fun put s = out_buffer := s :: ! out_buffer; + fun str_of_line line = " (line " ^ Int.toString line ^ ")"; + fun message (msg, is_err, line) = + (if is_err then "Error: " else "Warning: ") ^ drop_newline msg ^ str_of_line line ^ "\n"; + + val parameters = + [PolyML.Compiler.CPOutStream put, + PolyML.Compiler.CPLineNo (fn () => ! current_line), + PolyML.Compiler.CPErrorMessageProc (put o message)]; + + val _ = + (while not (List.null (! in_buffer)) do + PolyML.compiler (get, parameters) ()) + handle exn => + (put ("Exception- " ^ General.exnMessage exn ^ " raised"); + err (output ()); raise exn); + in if verbose then print (output ()) else () end; + +end; + + + +(** interrupts **) + +exception Interrupt = SML90.Interrupt; + +local + +fun capture f x = ((f x): unit; NONE) handle exn => SOME exn; + +fun release NONE = () + | release (SOME exn) = raise exn; + +val sig_int = 2; + +fun change_signal new_handler f x = + let + (*RACE wrt. other signals*) + val old_handler = Signal.signal (sig_int, new_handler); + val result = capture f x; + val _ = Signal.signal (sig_int, old_handler); + in release result end; + +val default_handler = Signal.SIG_HANDLE (fn _ => Process.interruptConsoleProcesses ()); + +in + +val _ = Signal.signal (sig_int, default_handler); + +fun ignore_interrupt f = change_signal Signal.SIG_IGN f; +fun raise_interrupt f = change_signal default_handler f; + +end; + + + +(** OS related **) + +unless_cygwin + use "ML-Systems/polyml-posix.ML"; + + +(* system command execution *) + +(*execute Unix command which doesn't take any input from stdin and + sends its output to stdout; could be done more easily by Unix.execute, + but that function doesn't use the PATH*) +fun execute command = + let + val tmp_name = OS.FileSys.tmpName (); + val is = (OS.Process.system (command ^ " > " ^ tmp_name); TextIO.openIn tmp_name); + val result = TextIO.inputAll is; + in + TextIO.closeIn is; + OS.FileSys.remove tmp_name; + result + end; + +(*plain version; with return code*) +fun system cmd = + if OS.Process.isSuccess (OS.Process.system cmd) then 0 else 1; + + +(* getenv *) + +fun getenv var = + (case OS.Process.getEnv var of + NONE => "" + | SOME txt => txt); + + +(* profile execution *) + +local + +fun no_profile () = + RunCall.run_call1 RuntimeCalls.POLY_SYS_profiler 0; + +in + +fun profile 0 f x = f x + | profile n f x = + (RunCall.run_call1 RuntimeCalls.POLY_SYS_profiler n; + let val y = f x handle exn => (no_profile (); raise exn) + in no_profile (); y end); + +end; -- 1.5.6.5