Dear Mike,
>Does anyone know if it is possible to run a function
>(e.g. SIMP_CONV arith_ss []) for a fixed time and then
>fail on timeout. I vaguely remember that there was no way
>to do this, but want to double check.
For my upcoming new Mizar mode for HOL Light I just implemented
exception Timeout;;
Sys.set_signal Sys.sigalrm (Sys.Signal_handle (fun _ -> raise Timeout));;
let TIMED_TAC n tac g =
let _ = Unix.alarm n in
try
let gs = tac g in
let _ = Unix.alarm 0 in
gs
with x ->
let _ = Unix.alarm 0 in
raise x;;
which seems to work well for me. (Now that I look at this,
it really is generic and not related to tactics at all,
it really meaning "run this function on this argument for
n seconds". Maybe I should rename it?) So one can run
TIMED_TAC 3 (SIMP_TAC[...])
and if the tactic hasn't succeeded in 3 seconds it will
throw the Timeout exception. If the argument is 0, it will
not timeout at all. (That's just Unix "alarm" semantics.)
If you do two nested TIMED_TAC's, the innermost "wins". So
TIMED_TAC 3 (TIMED_TAC 5 (SIMP_TAC[...]))
will timeout in 5 seconds, and not in 3.
Whether something like this also is possible in other MLs
than ocaml, I don't know.
Freek
-------------------------------------------------------------------------
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
