[isabelle] Emulating an Isabelle/ML toplevel



I maintain a graph rewriting library that can run either inside of
Isabelle or standalone. In the latter case, it needs to emulate a
fragment of the Isabelle/ML toplevel in poly/ML. I'm currently in the
process of updating this for Isabelle 2015.

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

which expects the "Pure" directory from Isabelle 2015 to be a
subdirectory. Here's what happens:

$ ML_SYSTEM=polyml ML_PLATFORM=unknown poly --use isabelle_env.ML

...

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

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

End of trace

val it =
   Future
    {task =
     Task
      {id = 3, pos = Pos ((0, 0, 0), []), pri = SOME 0, name = "fork",
       group =
       Group
        {id = 2, parent = NONE, status =
         Var {var = ref NONE, cond = ?, lock = ?, name = "group_status"}},
       timing = NONE}, result =
     Var {var = ref NONE, cond = ?, lock = ?, name = "future"}, promised =
     false}: int future


Any ideas? Also, is there some way to coerce Future.fork to give a
more informative stacktrace? I've tried various combinations with
PolyML.exception_trace to little effect. I assume this has to do with
how futures capture exceptions until they are join'ed.



Aleks




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