Re: [isabelle] Using timeLimit with tactics



On Sat, 19 May 2012, Ognjen Maric wrote:

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.

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





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