Re: [isabelle] Using timeLimit with tactics



Am 18.05.2012 um 17:56 schrieb Ognjen Maric:

> I'm trying to limit the running time of tactics under Isabelle 2011-1, using 
> timeLimit. [...] Can anyone shed some 
> light on this for me? Or point me to some working examples?

Let me point you to a working example. In "src/HOL/TPTP/CASC_Setup.thy", there's a "SOLVE_TIMEOUT" tactical you can copy paste and use. I got the code from Stefan Berghofer. I won't claim it's 100% fool-proof, but it works well enough for me. ;)

fun SOLVE_TIMEOUT seconds name tac st =
  let
    val result =
      TimeLimit.timeLimit (Time.fromSeconds seconds)
        (fn () => SINGLE (SOLVE tac) st) ()
      handle TimeLimit.TimeOut => NONE
        | ERROR _ => NONE
  in
    (case result of
      NONE => (warning ("FAILURE: " ^ name); Seq.empty)
    | SOME st' => (warning ("SUCCESS: " ^ name); Seq.single st'))
  end

Regards,

Jasmin






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