avoid race condition wrt. ISABELLE_TMP, which is removed in Bash.cleanup() before Bash.result(progress_stdout);
authorwenzelm
Wed, 16 May 2018 21:36:59 +0200
changeset 68198 6710167e17af
parent 68197 7857817403e4
child 68199 f551dd2178ab
avoid race condition wrt. ISABELLE_TMP, which is removed in Bash.cleanup() before Bash.result(progress_stdout);
src/Pure/Tools/build.ML
src/Pure/Tools/build.scala
--- a/src/Pure/Tools/build.ML	Wed May 16 21:07:12 2018 +0200
+++ b/src/Pure/Tools/build.ML	Wed May 16 21:36:59 2018 +0200
@@ -98,10 +98,9 @@
         not (null args) andalso #1 (hd args) = Markup.idN
       then
         let
-          val path = Isabelle_System.create_tmp_path "export" "";
+          val path = Path.expand (Path.explode ("$ISABELLE_EXPORT_TMP/export" ^ serial_string ()));
           val _ = File.open_output (fn out => List.app (File.output out) output) path;
-          val file_name = Path.implode (Path.expand path);
-        in inline_message (#2 function) (tl args @ [(Markup.fileN, file_name)]) end
+        in inline_message (#2 function) (tl args @ [(Markup.fileN, Path.implode path)]) end
       else
         (case Markup.dest_loading_theory props of
           SOME name => writeln ("\floading_theory = " ^ name)
--- a/src/Pure/Tools/build.scala	Wed May 16 21:07:12 2018 +0200
+++ b/src/Pure/Tools/build.scala	Wed May 16 21:36:59 2018 +0200
@@ -195,6 +195,7 @@
     private val graph_file = Isabelle_System.tmp_file("session_graph", "pdf")
     isabelle.graphview.Graph_File.write(options, graph_file, deps(name).session_graph_display)
 
+    private val export_tmp_dir = Isabelle_System.tmp_dir("export")
     private val export_consumer = Export.consumer(SQLite.open_database(store.output_database(name)))
 
     private val future_result: Future[Process_Result] =
@@ -222,6 +223,7 @@
 
         val env =
           Isabelle_System.settings() +
+            ("ISABELLE_EXPORT_TMP" -> File.standard_path(export_tmp_dir)) +
             ("ISABELLE_ML_DEBUGGER" -> options.bool("ML_debugger").toString)
 
         def save_heap: String =
@@ -323,6 +325,8 @@
           case errs => result.errors(errs)
         }
 
+      Isabelle_System.rm_tree(export_tmp_dir)
+
       if (export_result.ok)
         Present.finish(progress, store.browser_info, graph_file, info, name)