Email Gateway (Aug 22 2022 at 11:42): Email Gateway (Aug 22 2022 at 11:42):From: Aleks Kissinger <aleks0@gmail.com>
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
Email Gateway (Aug 22 2022 at 11:42):From: Makarius <makarius@sketis.net>
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
isabelle_env.ML
Email Gateway (Aug 22 2022 at 11:42):From: Aleks Kissinger <aleks0@gmail.com>
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
?
Email Gateway (Aug 22 2022 at 11:43):From: Makarius <makarius@sketis.net>
Yes, Pure/ROOT.ML defines the order. It is often re-shuffled in subtle
ways as years are coming and going.
I merely walked through your isabelle_env.ML, and re-ordered it according
to what was written in Isabelle2015/ROOT.ML.
Makarius
Last updated: Apr 24 2024 at 12:33 UTC