# HG changeset patch
# User wenzelm
# Date 1621163656 -7200
# Node ID d83e7e444b4382a65834b397bd5c7fefee9d56fe
# Parent  908351c8c0b1f009eb3e2d1368a8ca82f324e61e
ignore session build timeout, notably in AFP;

diff -r 908351c8c0b1 -r d83e7e444b43 etc/options
--- a/etc/options	Sun May 16 13:06:13 2021 +0200
+++ b/etc/options	Sun May 16 13:14:16 2021 +0200
@@ -113,6 +113,9 @@
 option timeout : real = 0
   -- "timeout for session build job (seconds > 0)"
 
+option timeout_build : bool = true
+  -- "observe timeout for session build"
+
 option process_output_limit : int = 100
   -- "build process output limit (in million characters, 0 = unlimited)"
 
diff -r 908351c8c0b1 -r d83e7e444b43 src/HOL/Tools/Mirabelle/mirabelle.scala
--- a/src/HOL/Tools/Mirabelle/mirabelle.scala	Sun May 16 13:06:13 2021 +0200
+++ b/src/HOL/Tools/Mirabelle/mirabelle.scala	Sun May 16 13:14:16 2021 +0200
@@ -102,7 +102,7 @@
 
     if (build_results0.ok) {
       val build_options =
-        options + "parallel_presentation=false" +
+        options + "timeout_build=false" + "parallel_presentation=false" +
           ("mirabelle_actions=" + actions.mkString(";")) +
           ("mirabelle_theories=" + theories.mkString(","))
 
diff -r 908351c8c0b1 -r d83e7e444b43 src/Pure/Thy/sessions.scala
--- a/src/Pure/Thy/sessions.scala	Sun May 16 13:06:13 2021 +0200
+++ b/src/Pure/Thy/sessions.scala	Sun May 16 13:14:16 2021 +0200
@@ -502,7 +502,9 @@
 
     def dirs: List[Path] = dir :: directories
 
-    def timeout_ignored: Boolean = Time.seconds(options.real("timeout")) < Time.ms(1)
+    def timeout_ignored: Boolean =
+      !options.bool("timeout_build") || Time.seconds(options.real("timeout")) < Time.ms(1)
+
     def timeout: Time = Time.seconds(options.real("timeout") * options.real("timeout_scale"))
 
     def document_enabled: Boolean =