Re: [isabelle] Emulating an Isabelle/ML toplevel



Excellent! Probably the issue came from using poly/ML 5.5.0, which
became clear as soon as "poly-5.5.2.ML" understandably failed to
typecheck....

For future ref, how can I reconstruct "canonical" order from the
sources? Is it (roughly) the bootstrap file, followed by Pure/ROOT.ML
?

On 7 October 2015 at 18:07, Makarius <makarius at sketis.net> wrote:
> 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




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