On Wed, 10 Apr 2013, Michael Bradley wrote:
I am using PolyML 5.5 and I am using the Futures library in IsapLib:
https://github.com/iislucas/isaplib. All of the tasks are independent. I
haven't had the chance to look properly into the debugging yet
(revising!), but I'll let you know once I have.
It seems you are actually one of the maintainers of this spin-off library
of Isabelle/ML, which was started by Lucas Dixon some years ago.
If there is anything to be amended in the master sources within Isabelle,
I am ready to revisit certain fine points -- it has a natural bias towards
particular applications within the proof assistant. (I am not accepting
arbitrary patches, though, since these things are very delicate.)
Just keep us informed here about your findings -- it is very relevant for
any high-performance applications of Poly/ML.
Note that for further exploration, "Future.ML_statistics := true" produces
a property list with summary of the Poly/ML runtime status and Isabelle/ML
future task queue and worker thread farm every 0.5s -- it subsumes
PolyML.Statistics.getLocalStats in particular. To see any of the results,
you need to provide a suitable implementation of
Output.Private_Hooks.protocol_message_fn, e.g. to print it or store it
somewhere else.
These global protocol hooks are normally managed by the Isabelle/ML
session startup, so you have to imitate this manually. Alternatively, you
can run under regular Isabelle/ML with Isabelle/jEdit, and then use its
Monitor panel (the online chart-drawing of that data is still a bit
crude).
Yet another way is to run your own ML monitoring thread that uses
PolyML.Statistics.getLocalStats or similar peridically -- in Isabelle/ML
this is built into the "scheduler thread" of the future task farm.
Makarius
_______________________________________________
polyml mailing list
polyml@inf.ed.ac.uk
http://lists.inf.ed.ac.uk/mailman/listinfo/polyml
