merged
authorpaulson
Fri, 13 Jan 2023 11:05:48 +0000
changeset 76947 20ab27bc1f3b
parent 76945 fcd1df8f48fc (diff)
parent 76946 5df58a471d9e (current diff)
child 76948 f33df7529fed
merged
--- a/NEWS	Thu Jan 12 17:12:36 2023 +0000
+++ b/NEWS	Fri Jan 13 11:05:48 2023 +0000
@@ -180,6 +180,9 @@
       multp_mono_strong
       wfP_subset_mset[simp]
 
+* Mirabelle:
+  - Added session to output directory structure. Minor INCOMPATIBILITY.
+
 
 *** ML ***
 
--- a/src/HOL/Tools/Mirabelle/mirabelle_sledgehammer.ML	Thu Jan 12 17:12:36 2023 +0000
+++ b/src/HOL/Tools/Mirabelle/mirabelle_sledgehammer.ML	Fri Jan 13 11:05:48 2023 +0000
@@ -305,12 +305,14 @@
     exhaustive_preplay proof_method_from_msg thy_index trivial pos st =
   let
     val thy = Proof.theory_of st
-    val thy_name = Context.theory_name thy
+    val thy_long_name = Context.theory_long_name thy
+    val session_name = Long_Name.qualifier thy_long_name
+    val thy_name = Long_Name.base_name thy_long_name
     val triv_str = if trivial then "[T] " else ""
     val keep =
       if keep_probs orelse keep_proofs then
         let val subdir = StringCvt.padLeft #"0" 4 (string_of_int thy_index) ^ "_" ^ thy_name in
-          Path.append output_dir (Path.basic subdir)
+          Path.append (Path.append output_dir (Path.basic session_name)) (Path.basic subdir)
           |> Isabelle_System.make_directory
           |> Path.implode
           |> (fn dir => SOME (dir, keep_probs, keep_proofs))