[isabelle] Using timeLimit with tactics



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





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