# HG changeset patch
# User wenzelm
# Date 1693596235 -7200
# Node ID 569135d7352a5d009ee4a59eff6e841571e6cbc7
# Parent  adf227c06812bbfe0e02820504cdad321f53ac19
more robust access to output file of external smt, notably for Windows 11, where transient ERROR_SHARING_VIOLATION has been seen;

diff -r adf227c06812 -r 569135d7352a src/Tools/cache_io.ML
--- a/src/Tools/cache_io.ML	Fri Sep 01 21:04:14 2023 +0200
+++ b/src/Tools/cache_io.ML	Fri Sep 01 21:23:55 2023 +0200
@@ -35,11 +35,19 @@
   redirected_output: string list,
   return_code: int}
 
+fun try_read_lines path =
+  let
+    fun loop n =
+      (case try File.read_lines path of
+        SOME lines => lines
+      | NONE => if n > 0 then (OS.Process.sleep (seconds 0.05); loop (n - 1)) else [])
+  in if File.exists path then loop (if ML_System.platform_is_windows then 20 else 0) else [] end
+
 fun raw_run make_cmd str in_path out_path =
   let
     val _ = File.write in_path str
     val (out2, rc) = Isabelle_System.bash_output (make_cmd in_path out_path)
-    val out1 = the_default [] (try File.read_lines out_path)
+    val out1 = try_read_lines out_path
   in {output = split_lines out2, redirected_output = out1, return_code = rc} end
 
 fun run make_cmd str =