On Sun, 9 Nov 2008, Lu Zhao wrote: > Can I use the thread support in PolyML to do this task? and how? I'd > like to run a ML function, which runs a HOL proof, for a certain amount > of time, say 20 seconds
See also the thread "Are timeouts possible in HOL (mosml or poly)?" on this list (August 2008): http://sourceforge.net/mailarchive/message.php?msg_name=E1KOtVj-0008Aq-00%40mta1.cl.cam.ac.uk When working with threads in Poly/M,L I do recommend the latest version 5.2.1. Before there is a problem with GC and internal wait that can produce a deadlock (very rarely). Other examples for working with Poly/ML threads are available here: http://isabelle.in.tum.de/repos/isabelle/file/tip/src/Pure/Concurrent/ Makarius ------------------------------------------------------------------------- This SF.Net email is sponsored by the Moblin Your Move Developer's challenge Build the coolest Linux based applications with Moblin SDK & win great prizes Grand prize is a trip for two to an Open Source event anywhere in the world http://moblin-contest.org/redirect.php?banner_id=100&url=/ _______________________________________________ hol-info mailing list [email protected] https://lists.sourceforge.net/lists/listinfo/hol-info
