Re: [isabelle] Emulating an Isabelle/ML toplevel



On Wed, 7 Oct 2015, Aleks Kissinger wrote:

It's mostly working, except Future.fork is throwing a mysterious
exception. The emulation is done via:

https://github.com/Quantomatic/quantomatic/blob/isabelle2015/core/isabelle_env.ML

Future.fork (fn() => 0);

Exception trace for exception - ERROR raised in library.ML line 257

PolyML.exception_trace to little effect

The exception trace is already in Simple_Thread.fork, but it does not print the exception value, only names. I've changed that temporarily to print General.exnMessage, and it reveals that some future worker thread complains about the absence of system option "threads_stack_limit".

Since there might be more subtle additions in Isabelle2015, I've carefully looked through isabelle_env.ML, after putting it into the canonical order of that release. The result is attached here.

More notes on your original version:

  * exception Interrupt was created afresh (!) independently on the one
    special exception SML90.Interrupt

  * the Poly/ML bootstrap file has a version, for Isabelle2015 it is
    "ML-Systems/polyml-5.5.2.ML"

  * tracing was unsynchronized, and in fact a duplicate from output.ML
    loaded later


	Makarius
(* Global version variable *)
val version = "Isabelle/IsaPlanner Library";

(*
 * Emulate the Isabelle toplevel environment
 *)
OS.FileSys.chDir "Pure";

fun exit st =
  OS.Process.exit
  (if st = 0 then OS.Process.success else OS.Process.failure);

use "ML-Systems/polyml-5.5.2.ML";
datatype ref = datatype Unsynchronized.ref;

use "General/basics.ML";
use "library.ML";
use "General/print_mode.ML";
use "General/alist.ML";
use "General/table.ML";

use "Concurrent/synchronized.ML";
if Multithreading.available then ()
else use "Concurrent/synchronized_sequential.ML";
use "Concurrent/counter.ML";

use "General/properties.ML";
use "General/output.ML";
use "PIDE/markup.ML";
use "General/scan.ML";
use "General/source.ML";
use "General/symbol.ML";
use "General/position.ML";
use "General/symbol_pos.ML";

use "General/integer.ML";
use "General/stack.ML";
use "General/queue.ML";
use "General/heap.ML";
use "General/ord_list.ML";
use "General/balanced_tree.ML";
use "General/buffer.ML";
use "General/pretty.ML";
use "PIDE/xml.ML";
use "General/path.ML";
use "General/url.ML";
use "General/file.ML";
use "General/long_name.ML";
use "General/binding.ML";
use "General/seq.ML";
use "General/timing.ML";

use "General/sha1.ML";

use "PIDE/yxml.ML";

use "General/graph.ML";

use "System/options.ML";

(* hard-coded options *)
val options =
  Options.empty
  |> Options.declare
      {pos = Position.none, name = "completion_limit", typ = Options.intT, value = "200"}
  |> Options.declare
      {pos = Position.none, name = "threads_stack_limit", typ = Options.realT, value = "0.25"};

Options.set_default options;


use "ML/exn_properties_polyml.ML";
use "ML/ml_statistics_polyml-5.5.0.ML";

use "Concurrent/simple_thread.ML";

use "Concurrent/single_assignment.ML";
if Multithreading.available then ()
else use "Concurrent/single_assignment_sequential.ML";

if Multithreading.available
then use "Concurrent/bash.ML"
else use "Concurrent/bash_sequential.ML";

use "Concurrent/par_exn.ML";
use "Concurrent/task_queue.ML";
use "Concurrent/future.ML";
use "Concurrent/event_timer.ML";

if ML_System.is_polyml then use "Concurrent/time_limit.ML" else ();

use "Concurrent/lazy.ML";
if Multithreading.available then ()
else use "Concurrent/lazy_sequential.ML";

use "Concurrent/par_list.ML";
if Multithreading.available then ()
else use "Concurrent/par_list_sequential.ML";

use "Concurrent/mailbox.ML";
use "Concurrent/cache.ML";


use "name.ML";
use "General/completion.ML";

val rootDir = OS.FileSys.getDir ();

OS.FileSys.chDir "..";


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