Re: [isabelle] installing Isabelle under polyml-5



On Wed, 27 Oct 2010, Jeremy Dawson wrote:

If each version of Isabelle only works with a specific (or sufficiently old) version of PolyML, then the old versions of PolyMl also need to be made available on the website together with the old Isabelle releases.

Full distributions in this sense are archived at http://isabelle.in.tum.de/download_past.html -- starting with Isabelle2008 only.

Really old Isabelle versions can be easily compiled using SML/NJ, instead of Poly/ML. While Poly/ML is still young and evolving fast, SML/NJ did never really change in the past 15 years. The only incompatibilty is the
update of the basis library definition in 2004.

Just a few days ago, I managed to get Isabelle98 work with current SML/NJ 110.72 on Mac OS X (Intel 64bit), which was easy due to the lack of Proof General in the 98 version. For the historical record, the relevant src/Pure/ML-Systems/smlnj.ML is included here.


	Makarius
(*  Title:      Pure/ML-Systems/smlnj.ML
    Author:     Carsten Clasohm and Markus Wenzel, TU Muenchen

Compatibility file for Standard ML of New Jersey versions 110.72.
*)

(** ML system related **)

(* restore old-style character / string functions *)

fun ord s = Char.ord (String.sub (s, 0));
val chr = str o Char.chr;
val explode = (map str) o String.explode;
val implode = String.concat;


(* New Jersey ML parameters *)

structure Compiler =
struct
  open Compiler;
  structure Control = Control;
  structure PrettyPrint = PrettyPrint;
  structure PPTable = CompilerPPTable;
  structure Interact = Backend.Interact;
end;

val _ =
 (Compiler.Control.Print.printLength := 1000;
  Compiler.Control.Print.printDepth := 350;
  Compiler.Control.Print.stringDepth := 250;
  Compiler.Control.Print.signatures := 2);


(* interrupts *)

exception Interrupt;

local

fun capture f x = ((f x): unit; NONE) handle exn => SOME exn;

fun release NONE = ()
  | release (SOME exn) = raise exn;

in

fun ignore_interrupt f x =
  let
    val old_handler = Signals.setHandler (Signals.sigINT, Signals.IGNORE);
    val result = capture f x;
    val _ = Signals.setHandler (Signals.sigINT, old_handler);
  in release result end;

fun raise_interrupt f x =
  let
    val interrupted = ref false;
    val result = ref NONE;
    val old_handler = Signals.inqHandler Signals.sigINT;
  in
    SMLofNJ.Cont.callcc (fn cont =>
      (Signals.setHandler (Signals.sigINT, Signals.HANDLER (fn _ => (interrupted := true; cont)));
      result := capture f x));
    Signals.setHandler (Signals.sigINT, old_handler);
    if ! interrupted then raise Interrupt else release (! result)
  end;

end;


(* basis library incompatibilities *)

structure TextIO =
struct
  open TextIO;

  fun inputLine is =
    (case TextIO.inputLine is of
      SOME str => str
    | NONE => "")
    handle IO.Io _ => raise Interrupt;
end;


(* Poly/ML emulation *)

fun quit () = exit 0;

(*limit the printing depth -- divided by 2 for comparibility with Poly/ML*)
fun print_depth n =
 (Compiler.Control.Print.printDepth := n div 2;
  Compiler.Control.Print.printLength := n);

(*Poly/ML-like prompts*)
Compiler.Control.primaryPrompt := "> ";
Compiler.Control.secondaryPrompt := "# ";


(** Compiler-independent timing functions **)

(*Note start point for timing*)
fun startTiming() =
  let val CPUtimer = Timer.startCPUTimer();
      val time = Timer.checkCPUTimer(CPUtimer)
  in  (CPUtimer,time)  end;

(*Finish timing and return string*)
fun endTiming (CPUtimer, {sys,usr}) =
  let open Time  (*...for Time.toString, Time.+ and Time.- *)
      val {sys=sys2,usr=usr2} = Timer.checkCPUTimer(CPUtimer)
  in  "User " ^ toString (usr2-usr) ^
      "  All "^ toString (sys2-sys + usr2-usr) ^
      " secs"
      handle Time => ""
  end;

fun checkTimer timer =
  let
    val {sys, usr} = Timer.checkCPUTimer timer;
    val gc = Timer.checkGCTime timer;    (* FIXME already included in usr? *)
  in (sys, usr, gc) end;


(* toplevel pretty printing (see also Pure/install_pp.ML) *)

fun make_pp path pprint =
  let
    open Compiler.PrettyPrint;

    fun pp pps obj =
      pprint obj
        (string pps, openHOVBox pps o Rel,
          fn wd => break pps {nsp=wd, offset=0}, fn () => newline pps,
          fn () => closeBox pps);
  in
    (path, pp)
  end;

fun install_pp (path, pp) = Compiler.PPTable.install_pp path pp;


(* ML command execution *)

val use_strings = Compiler.Interact.useStream o TextIO.openString o implode;



(** OS related **)

(* 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;


(* file handling *)

(*get time of last modification; if file doesn't exist return an empty string*)
fun file_info "" = ""		(* FIXME !? *)
  | file_info name = Time.toString (OS.FileSys.modTime name) handle _ => "";


(* getenv *)

fun getenv var =
  (case OS.Process.getEnv var of
    NONE => ""
  | SOME txt => txt);


(* non-ASCII input (see also Thy/use.ML) *)

val needs_filtered_use = false;


This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.