[isabelle] General timeout for tactics · Mirror: Isabelle Users Mailing List

is it possible to have a general timeout for all tactics or for all apply and by commands?

lemma assumes A: "x = y" "y = x"
  shows "x = z"
  apply(fastforce simp add: A)

I often run into this problem when working on Isabelle code and simply changing a definition or a lemma. I then go through the failed proofs coming after the change. And often there is a metis or blast command simply clogging up the CPU and making my laptop unresponsive.

The documentation [1] says on page 97 in a footnote: “The lack of memoing and the strict nature of ML requires some care when working with low-level sequence operations, to avoid duplicate or premature evaluation of results. It also means that modified runtime behavior, such as timeout, is very hard to achieve for general tactics.”
Is there maybe a hack which I can activate when doing interactive proof development in Isabelle/jedit?

Email Gateway (Nov 03 2020 at 12:43):

There exists at least one example in Isabelle/HOL's source code: look
for atp_tac in atp_problem_import.ML. At some point in the past, I was able
to use it to implement a timeout for one of my own tactics (this was done
for experiments and debugging only, of course) using elements of the code
borrowed from the implementation of atp_tac.

Also, I would like to make note on the subject of debugging rules for
classical reasoner. In the past, I found it useful to use the single-step
tactics, as described in section 9.4.6 of the manual. However, I am sure
that you are aware of them already.

I hope you will find my comments useful. However, of course, this is not an
official reply and there may be a more canonical solution available.

Email Gateway (Nov 03 2020 at 12:48):

From: Manuel Eberl <eberlm@in.tum.de>
I know that problem well. Every once in a while, a rogue call of some
tactic (e.g. a heavily backgracking "transfer") loops and takes the
entire Isabelle/jEdit session with it.

Sometimes one can delete the offending tactic call and the session
recovers eventually, but most of the time it's faster to just kill it
and restart everything.

Email Gateway (Nov 03 2020 at 13:44):

It's not really relevant for this list, but in HOL Light
it is trivial to hack something like this together:

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;;

If you do (TIMED_TAC 3 (MESON_TAC[...])), it will run
(MESON_TAC[...]) but if that doesn't succeed in 3 seconds,
it will fail with a Timeout exception.

Email Gateway (Nov 03 2020 at 15:04):

I had a little bit more time now and implemented a rough sketch of a
plausible solution based on my own suggestion (its only purpose is to
demonstrate that the functionality that you seek can be implemented
easily). Of course, it will need to be refined for any
serious applications. Also, with some further work, it can be integrated in
the apply/by infrastructure:

(* timeout configuration *)
val timeout_cfg = Attrib.setup_config_int \<^binding>‹mtime› (K 0)

(* copied from HOL/TPTP/atp_problem_import.ML with minor amendments *)
fun SOLVE_TIMEOUT mseconds tac st =
let
val result =
Timeout.apply
(Time.fromMilliseconds mseconds) (fn () => SINGLE (SOLVE tac) st) ()
handle Timeout.TIMEOUT _ => NONE | ERROR _ => NONE
in
(
case result of
NONE => Seq.empty
| SOME st' => Seq.single st'
)
end

fun timeout_tac ctxt t m =
let
val tac = (Method.evaluate m ctxt) []
|> Context_Tactic.NO_CONTEXT_TACTIC ctxt
|> SOLVE_TIMEOUT t
in SIMPLE_METHOD tac end;

val _ = Theory.setup
(
Method.setup
\<^binding>‹timeout›
(timeout_parser >> process_timeout)
"higher order timeout method"
);

lemma
assumes A: "x = y" "y = x"
shows "x = z"
apply(timeout‹fastforce simp add: A›)
oops

Email Gateway (Nov 03 2020 at 19:58):

I have to admit that my previous replies were slightly rushed: I was trying
to do too many things at the same time after consuming a substantial amount
of caffeine :). Having had a look at my own replies, I noticed a few
typographical/style errors.

fun timeout_tac ctxt t m = Method.evaluate m ctxt []
|> Context_Tactic.NO_CONTEXT_TACTIC ctxt
|> SOLVE_TIMEOUT t;

fun process_timeout m ctxt =
SIMPLE_METHOD (timeout_tac ctxt (Config.get ctxt timeout_cfg) m);

val _ = Theory.setup
(
Method.setup
\<^binding>‹timeout›
(Method.text_closure >> process_timeout)
"higher order timeout method"
);

Email Gateway (Nov 04 2020 at 12:00):

From: Thomas Sewell <tals4@cam.ac.uk>
I just want to make sure that somebody points out the obvious issue.

Wrapping a timeout around fastforce, metis etc sounds like a good thing.
Failures are easier to find and address than divergence. However, it
would be a disaster if there were lots of proofs that mostly worked
but failed outright if some machine was running particularly slowly for
whatever reason.

So, it's easy enough to implement a timeout mechanism on a tactic or
method,
but it's probably not useful for the purpose you really want, which is
to
set timeouts throughout your theories by default.

Years ago I spent some time wondering whether there was some kind of
objective
timing that would make sense, e.g. the number of classical steps in a
fastforce/auto proof. Limiting those would be safer. I never got around
to
implementing anything though.

Email Gateway (Nov 04 2020 at 19:09):

Thank you for your remarks. It was never my intention to advocate the use
of this feature in production-level code. However, it can be useful for
debugging and experimentation (e.g. when designing a new
simpset/intro/dest/elim rules or a new tactic/proof method). Of course,
once a simpset/rule set/tactic/method is designed, the timeout should be
removed.

Email Gateway (Nov 04 2020 at 19:18):

From: Manuel Eberl <eberlm@in.tum.de>
Some users (perhaps including me) might find this very useful even as an
"always switched on" option in the IDE – although I am not sure how well
that works in practice.

The main use case would be to kill those rogue "transfer" calls that
block the entire system. But it's quite possible that after 10 seconds
(or whatever a suitable timeout would be) it might already have done too
much damage for the system to recover in a reasonable amount of time.

Thomas is of course right to point out that this is not something that
should run in batch mode because reproducibility goes completely out of
the window if you switch it on.

Stream: Mirror: Isabelle Users Mailing List

Topic: [isabelle] General timeout for tactics

Email Gateway (Nov 03 2020 at 12:16):