# HG changeset patch
# User wenzelm
# Date 1636399576 -3600
# Node ID df4449c6eff14ecb59dd32e9ad8bb8f73653f1f6
# Parent  0580ae467ecbb1eae7a04bc6c261904c7406f4a9
explicit option metric_argo_timeout, with reasonable default for Raspberry Pi;

diff -r 0580ae467ecb -r df4449c6eff1 src/HOL/Analysis/ex/Metric_Arith_Examples.thy
--- a/src/HOL/Analysis/ex/Metric_Arith_Examples.thy	Mon Nov 08 20:15:04 2021 +0100
+++ b/src/HOL/Analysis/ex/Metric_Arith_Examples.thy	Mon Nov 08 20:26:16 2021 +0100
@@ -54,7 +54,7 @@
   by metric
 
 lemma "dist a e \<le> dist a b + dist b c + dist c d + dist d e"
-  using [[argo_timeout = 25]] by metric
+  by metric
 
 lemma "max (dist x y) \<bar>dist x z - dist z y\<bar> = dist x y"
   by metric
diff -r 0580ae467ecb -r df4449c6eff1 src/HOL/Analysis/metric_arith.ML
--- a/src/HOL/Analysis/metric_arith.ML	Mon Nov 08 20:15:04 2021 +0100
+++ b/src/HOL/Analysis/metric_arith.ML	Mon Nov 08 20:26:16 2021 +0100
@@ -7,6 +7,7 @@
 signature METRIC_ARITH =
 sig
   val trace: bool Config.T
+  val argo_timeout: real Config.T
   val metric_arith_tac : Proof.context -> int -> tactic
 end
 
@@ -21,10 +22,15 @@
 fun trace_tac ctxt msg =
   if Config.get ctxt trace then print_tac ctxt msg else all_tac
 
-fun argo_trace_ctxt ctxt =
-  if Config.get ctxt trace
-  then Config.map (Argo_Tactic.trace) (K "basic") ctxt
-  else ctxt
+val argo_timeout = Attrib.setup_config_real \<^binding>\<open>metric_argo_timeout\<close> (K 20.0)
+
+fun argo_ctxt ctxt =
+  let
+    val ctxt1 =
+      if Config.get ctxt trace
+      then Config.map (Argo_Tactic.trace) (K "basic") ctxt
+      else ctxt
+  in Config.put Argo_Tactic.timeout (Config.get ctxt1 argo_timeout) ctxt1 end
 
 fun free_in v t =
   Term.exists_subterm (fn u => u aconv Thm.term_of v) (Thm.term_of t);
@@ -218,10 +224,8 @@
 
 (* decision procedure for linear real arithmetic *)
 fun lin_real_arith_tac ctxt metric_ty = CSUBGOAL (fn (goal, i) =>
-  let
-    val dist_thms = augment_dist_pos metric_ty goal
-    val ctxt' = argo_trace_ctxt ctxt
-  in Argo_Tactic.argo_tac ctxt' dist_thms i end)
+  let val dist_thms = augment_dist_pos metric_ty goal
+  in Argo_Tactic.argo_tac (argo_ctxt ctxt) dist_thms i end)
 
 fun basic_metric_arith_tac ctxt metric_ty =
   SELECT_GOAL (