Stream: Mirror: Isabelle Users Mailing List

Topic: [isabelle] General timeout for tactics


view this post on Zulip Email Gateway (Nov 03 2020 at 12:16):

From: Max Haslbeck <max.haslbeck@gmx.de>
Hi,

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

For example, fastforce loops in the following proof:

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

Can I just have it timeout after 10 seconds?

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?

Gruß
Max

[1]: https://isabelle.in.tum.de/dist/Isabelle2020/doc/implementation.pdf

view this post on Zulip Email Gateway (Nov 03 2020 at 12:43):

From: Mikhail Chekhov <mikhail.chekhov.w@gmail.com>
Dear Max Haslbeck,

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.

Kind Regards,
Mikhail Chekhov

view this post on Zulip 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.

Manuel

view this post on Zulip Email Gateway (Nov 03 2020 at 13:44):

From: Freek Wiedijk <freek@cs.ru.nl>
Dear all,

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

exception Timeout;;

Sys.set_signal Sys.sigalrm (Sys.Signal_handle (fun _ -> raise Timeout));;

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.

Freek

view this post on Zulip Email Gateway (Nov 03 2020 at 15:04):

From: Mikhail Chekhov <mikhail.chekhov.w@gmail.com>
Dear All,

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:

theory Scratch
imports
Main
begin

ML‹

val timeout_parser = Method.text_closure

fun process_timeout ctxt m = ctxt

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

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

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

declare[[mtime=1]]

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

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

end

Kind Regards,
Mikhail Chekhov

view this post on Zulip Email Gateway (Nov 03 2020 at 19:58):

From: Mikhail Chekhov <mikhail.chekhov.w@gmail.com>
Dear All,

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.

  1. The first sentence of the second paragraph of the first email should
    read "Also, I would like to make a note on the subject of debugging of the
    rules for certain proof methods for classical reasoning."

  2. The ML part of the code in the second email was meant to look like the
    code shown below (more specifically, I noticed that a wrong naming
    convention was used for the function for the specification of the method
    and there were a few redundancies). Keep in mind, this is still only a
    sketch.

ML‹

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 = 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"
);

Kind Regards,
Mikhail Chekhov

view this post on Zulip 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.

Best regards,
Thomas.

view this post on Zulip Email Gateway (Nov 04 2020 at 19:09):

From: Mikhail Chekhov <mikhail.chekhov.w@gmail.com>
Dear Thomas Sewell/All,

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.

Kind Regards,
Mikhail Chekhov

view this post on Zulip 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.

Manuel


Last updated: Sep 25 2021 at 09:17 UTC