Email Gateway (Aug 18 2022 at 19:46): Email Gateway (Aug 18 2022 at 19:46):From: Ognjen Maric <ognjen.maric@gmail.com>
Hi all,
I'm trying to limit the running time of tactics under Isabelle 2011-1, using
timeLimit. Both of the following examples work as I want them to:
ML_prf {*
fun loop_tac ctxt i = loop_tac ctxt i
*}
apply(tactic {*
TimeLimit.timeLimit (Time.fromMilliseconds 500) (loop_tac @{context}) 1
*})
apply(tactic {*
TimeLimit.timeLimit (Time.fromMilliseconds 50) ((auto_tac @{context}))
*}) [1]
i.e. they timeout after the appropriate time. However neither of the following
do anything:
apply(tactic {*
TimeLimit.timeLimit (Time.fromMilliseconds 500) loop_tac @{context} 1
*})
apply(tactic {*
TimeLimit.timeLimit (Time.fromMilliseconds 500) (auto_tac @{context})
*}) [1]
The difference is the grouping of the arguments in the first example (hence
changing the type of timeLimit's result), and increasing the limit in the
second example. I can't really make any sense of it. Can anyone shed some
light on this for me? Or point me to some working examples?
Thanks,
Ognjen
Email Gateway (Aug 18 2022 at 19:46):From: Jasmin Blanchette <jasmin.blanchette@gmail.com>
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
Email Gateway (Aug 18 2022 at 19:46):From: Ognjen Maric <ognjen.maric@gmail.com>
On Friday 18 May 2012 20:08:30 Jasmin Blanchette wrote:
Ah, that code makes a lot of sense, thanks - I doubt I would've been able to
come up with it on my own ;)
Best,
Ognjen
Email Gateway (Aug 18 2022 at 19:47):From: Tjark Weber <webertj@in.tum.de>
TimeLimit.timeLimit t f x applies f to x, raising a TimeOut if this
takes longer than t.
loop_tac is a curried function that takes two arguments. With the second
grouping, timeLimit limits the runtime of partially applying loop_tac to
one argument (@{context}). But this partial application (which yields
loop_tac @{context}, a function of one argument) takes (almost) no time
anyway.
Infinite recursion happens once you apply loop_tac @{context} to an
argument (i.e., 1). But with the second grouping, this application is no
longer guarded by timeLimit.
Best regards,
Tjark
Email Gateway (Aug 18 2022 at 19:47):From: Ognjen Maric <ognjen.maric@gmail.com>
On Saturday 19 May 2012 13:43:17 Tjark Weber wrote:
Yup, thanks. I guess the auto_tac timeout after 50ms stems from evaluating the
@{context} and whatever it is that mk_auto_tac does. However I probably
wouldn't have gotten the whole Seq and SINGLE thing to eagerly everything
properly without Jasmin's help.
Best,
Ognjen
Email Gateway (Aug 18 2022 at 19:47):From: Makarius <makarius@sketis.net>
Apart from partial application of context, subgoal number, goal state,
there are more degress of freedom that have not been mentioned yet: lazy
evaluation of results and potential backtracking over them. This is why
the SINGLE combinator is used in the CASC example, to ensure that there is
at most one result.
In summary, timeout on an arbitrary tactic is not well-defined. You need
to restrict yourself to certain situations. This also explains why there
is no tactical for that in the Isabelle/ML library. Conceptually, a
robust timeout works better for certain closed tactic applications, say
the 'apply' command in Isar or Goal.prove in ML.
BTW, the more recent Isabelle/ML function "seconds" helps to produce time
values without further ado.
Makarius
Last updated: Apr 25 2024 at 20:15 UTC