50 files changed, 7 insertions, 13 deletions
diff --git a/tests/coq/hashmap_on_disk/HashmapMain_Funs.v b/tests/coq/hashmap_main/HashmapMain_Funs.v
index f6467d5a..f6467d5a 100644
--- a/tests/coq/hashmap_on_disk/HashmapMain_Funs.v
+++ b/tests/coq/hashmap_main/HashmapMain_Funs.v
diff --git a/tests/coq/hashmap_on_disk/HashmapMain_FunsExternal.v b/tests/coq/hashmap_main/HashmapMain_FunsExternal.v
index fb5f23cd..fb5f23cd 100644
--- a/tests/coq/hashmap_on_disk/HashmapMain_FunsExternal.v
+++ b/tests/coq/hashmap_main/HashmapMain_FunsExternal.v
diff --git a/tests/coq/hashmap_on_disk/HashmapMain_FunsExternal_Template.v b/tests/coq/hashmap_main/HashmapMain_FunsExternal_Template.v
index 66835e8c..66835e8c 100644
--- a/tests/coq/hashmap_on_disk/HashmapMain_FunsExternal_Template.v
+++ b/tests/coq/hashmap_main/HashmapMain_FunsExternal_Template.v
diff --git a/tests/coq/hashmap_on_disk/HashmapMain_Types.v b/tests/coq/hashmap_main/HashmapMain_Types.v
index 5656bd9c..5656bd9c 100644
--- a/tests/coq/hashmap_on_disk/HashmapMain_Types.v
+++ b/tests/coq/hashmap_main/HashmapMain_Types.v
diff --git a/tests/coq/hashmap_on_disk/HashmapMain_TypesExternal.v b/tests/coq/hashmap_main/HashmapMain_TypesExternal.v
index 28651c14..28651c14 100644
--- a/tests/coq/hashmap_on_disk/HashmapMain_TypesExternal.v
+++ b/tests/coq/hashmap_main/HashmapMain_TypesExternal.v
diff --git a/tests/coq/hashmap_on_disk/HashmapMain_TypesExternal_Template.v b/tests/coq/hashmap_main/HashmapMain_TypesExternal_Template.v
index 391b2775..391b2775 100644
--- a/tests/coq/hashmap_on_disk/HashmapMain_TypesExternal_Template.v
+++ b/tests/coq/hashmap_main/HashmapMain_TypesExternal_Template.v
diff --git a/tests/coq/hashmap_on_disk/Makefile b/tests/coq/hashmap_main/Makefile
index 1a5aee4a..1a5aee4a 100644
--- a/tests/coq/hashmap_on_disk/Makefile
+++ b/tests/coq/hashmap_main/Makefile
diff --git a/tests/coq/hashmap_on_disk/Primitives.v b/tests/coq/hashmap_main/Primitives.v
index b29fce43..b29fce43 100644
--- a/tests/coq/hashmap_on_disk/Primitives.v
+++ b/tests/coq/hashmap_main/Primitives.v
diff --git a/tests/coq/hashmap_on_disk/_CoqProject b/tests/coq/hashmap_main/_CoqProject
index d73541d9..d73541d9 100644
--- a/tests/coq/hashmap_on_disk/_CoqProject
+++ b/tests/coq/hashmap_main/_CoqProject
diff --git a/tests/fstar/hashmap_on_disk/HashmapMain.Clauses.Template.fst b/tests/fstar/hashmap_main/HashmapMain.Clauses.Template.fst
index cdd73210..cdd73210 100644
--- a/tests/fstar/hashmap_on_disk/HashmapMain.Clauses.Template.fst
+++ b/tests/fstar/hashmap_main/HashmapMain.Clauses.Template.fst
diff --git a/tests/fstar/hashmap_on_disk/HashmapMain.Clauses.fst b/tests/fstar/hashmap_main/HashmapMain.Clauses.fst
index be5a4ab1..be5a4ab1 100644
--- a/tests/fstar/hashmap_on_disk/HashmapMain.Clauses.fst
+++ b/tests/fstar/hashmap_main/HashmapMain.Clauses.fst
diff --git a/tests/fstar/hashmap_on_disk/HashmapMain.Funs.fst b/tests/fstar/hashmap_main/HashmapMain.Funs.fst
index c88a746e..c88a746e 100644
--- a/tests/fstar/hashmap_on_disk/HashmapMain.Funs.fst
+++ b/tests/fstar/hashmap_main/HashmapMain.Funs.fst
diff --git a/tests/fstar/hashmap_on_disk/HashmapMain.FunsExternal.fsti b/tests/fstar/hashmap_main/HashmapMain.FunsExternal.fsti
index cc20d988..cc20d988 100644
--- a/tests/fstar/hashmap_on_disk/HashmapMain.FunsExternal.fsti
+++ b/tests/fstar/hashmap_main/HashmapMain.FunsExternal.fsti
diff --git a/tests/fstar/hashmap_on_disk/HashmapMain.Properties.fst b/tests/fstar/hashmap_main/HashmapMain.Properties.fst
index beb3dc2c..beb3dc2c 100644
--- a/tests/fstar/hashmap_on_disk/HashmapMain.Properties.fst
+++ b/tests/fstar/hashmap_main/HashmapMain.Properties.fst
diff --git a/tests/fstar/hashmap_on_disk/HashmapMain.Types.fst b/tests/fstar/hashmap_main/HashmapMain.Types.fst
index 85bcaeea..85bcaeea 100644
--- a/tests/fstar/hashmap_on_disk/HashmapMain.Types.fst
+++ b/tests/fstar/hashmap_main/HashmapMain.Types.fst
diff --git a/tests/fstar/hashmap_on_disk/HashmapMain.TypesExternal.fsti b/tests/fstar/hashmap_main/HashmapMain.TypesExternal.fsti
index 75747408..75747408 100644
--- a/tests/fstar/hashmap_on_disk/HashmapMain.TypesExternal.fsti
+++ b/tests/fstar/hashmap_main/HashmapMain.TypesExternal.fsti
diff --git a/tests/fstar/hashmap_on_disk/Makefile b/tests/fstar/hashmap_main/Makefile
index fa7d1f36..fa7d1f36 100644
--- a/tests/fstar/hashmap_on_disk/Makefile
+++ b/tests/fstar/hashmap_main/Makefile
diff --git a/tests/fstar/hashmap_on_disk/Primitives.fst b/tests/fstar/hashmap_main/Primitives.fst
index 9951ccc3..9951ccc3 100644
--- a/tests/fstar/hashmap_on_disk/Primitives.fst
+++ b/tests/fstar/hashmap_main/Primitives.fst
diff --git a/tests/hol4/hashmap_on_disk/Holmakefile b/tests/hol4/constants/Holmakefile
index 3c4b8973..3c4b8973 100644
--- a/tests/hol4/hashmap_on_disk/Holmakefile
+++ b/tests/hol4/constants/Holmakefile
diff --git a/tests/hol4/misc-constants/constantsScript.sml b/tests/hol4/constants/constantsScript.sml
index 40a319c6..40a319c6 100644
--- a/tests/hol4/misc-constants/constantsScript.sml
+++ b/tests/hol4/constants/constantsScript.sml
diff --git a/tests/hol4/misc-constants/constantsTheory.sig b/tests/hol4/constants/constantsTheory.sig
index 287ad5f5..287ad5f5 100644
--- a/tests/hol4/misc-constants/constantsTheory.sig
+++ b/tests/hol4/constants/constantsTheory.sig
diff --git a/tests/hol4/misc-constants/Holmakefile b/tests/hol4/external/Holmakefile
index 3c4b8973..3c4b8973 100644
--- a/tests/hol4/misc-constants/Holmakefile
+++ b/tests/hol4/external/Holmakefile
diff --git a/tests/hol4/misc-external/external_FunsScript.sml b/tests/hol4/external/external_FunsScript.sml
index f3692ee2..f3692ee2 100644
--- a/tests/hol4/misc-external/external_FunsScript.sml
+++ b/tests/hol4/external/external_FunsScript.sml
diff --git a/tests/hol4/misc-external/external_FunsTheory.sig b/tests/hol4/external/external_FunsTheory.sig
index 490f9d06..490f9d06 100644
--- a/tests/hol4/misc-external/external_FunsTheory.sig
+++ b/tests/hol4/external/external_FunsTheory.sig
diff --git a/tests/hol4/misc-external/external_OpaqueScript.sml b/tests/hol4/external/external_OpaqueScript.sml
index b5a6d91d..b5a6d91d 100644
--- a/tests/hol4/misc-external/external_OpaqueScript.sml
+++ b/tests/hol4/external/external_OpaqueScript.sml
diff --git a/tests/hol4/misc-external/external_OpaqueTheory.sig b/tests/hol4/external/external_OpaqueTheory.sig
index 7cd7a08c..7cd7a08c 100644
--- a/tests/hol4/misc-external/external_OpaqueTheory.sig
+++ b/tests/hol4/external/external_OpaqueTheory.sig
diff --git a/tests/hol4/misc-external/external_TypesScript.sml b/tests/hol4/external/external_TypesScript.sml
index d290c3f6..d290c3f6 100644
--- a/tests/hol4/misc-external/external_TypesScript.sml
+++ b/tests/hol4/external/external_TypesScript.sml
diff --git a/tests/hol4/misc-external/external_TypesTheory.sig b/tests/hol4/external/external_TypesTheory.sig
index 17e2e8e3..17e2e8e3 100644
--- a/tests/hol4/misc-external/external_TypesTheory.sig
+++ b/tests/hol4/external/external_TypesTheory.sig
diff --git a/tests/hol4/misc-external/Holmakefile b/tests/hol4/hashmap_main/Holmakefile
index 3c4b8973..3c4b8973 100644
--- a/tests/hol4/misc-external/Holmakefile
+++ b/tests/hol4/hashmap_main/Holmakefile
diff --git a/tests/hol4/hashmap_on_disk/hashmapMain_FunsScript.sml b/tests/hol4/hashmap_main/hashmapMain_FunsScript.sml
index c1e30aa6..c1e30aa6 100644
--- a/tests/hol4/hashmap_on_disk/hashmapMain_FunsScript.sml
+++ b/tests/hol4/hashmap_main/hashmapMain_FunsScript.sml
diff --git a/tests/hol4/hashmap_on_disk/hashmapMain_FunsTheory.sig b/tests/hol4/hashmap_main/hashmapMain_FunsTheory.sig
index d4e43d9a..d4e43d9a 100644
--- a/tests/hol4/hashmap_on_disk/hashmapMain_FunsTheory.sig
+++ b/tests/hol4/hashmap_main/hashmapMain_FunsTheory.sig
diff --git a/tests/hol4/hashmap_on_disk/hashmapMain_OpaqueScript.sml b/tests/hol4/hashmap_main/hashmapMain_OpaqueScript.sml
index f7221d92..f7221d92 100644
--- a/tests/hol4/hashmap_on_disk/hashmapMain_OpaqueScript.sml
+++ b/tests/hol4/hashmap_main/hashmapMain_OpaqueScript.sml
diff --git a/tests/hol4/hashmap_on_disk/hashmapMain_OpaqueTheory.sig b/tests/hol4/hashmap_main/hashmapMain_OpaqueTheory.sig
index f7373609..f7373609 100644
--- a/tests/hol4/hashmap_on_disk/hashmapMain_OpaqueTheory.sig
+++ b/tests/hol4/hashmap_main/hashmapMain_OpaqueTheory.sig
diff --git a/tests/hol4/hashmap_on_disk/hashmapMain_TypesScript.sml b/tests/hol4/hashmap_main/hashmapMain_TypesScript.sml
index 3f8ca9b9..3f8ca9b9 100644
--- a/tests/hol4/hashmap_on_disk/hashmapMain_TypesScript.sml
+++ b/tests/hol4/hashmap_main/hashmapMain_TypesScript.sml
diff --git a/tests/hol4/hashmap_on_disk/hashmapMain_TypesTheory.sig b/tests/hol4/hashmap_main/hashmapMain_TypesTheory.sig
index a3e770ea..a3e770ea 100644
--- a/tests/hol4/hashmap_on_disk/hashmapMain_TypesTheory.sig
+++ b/tests/hol4/hashmap_main/hashmapMain_TypesTheory.sig
diff --git a/tests/hol4/misc-loops/Holmakefile b/tests/hol4/loops/Holmakefile
index 3c4b8973..3c4b8973 100644
--- a/tests/hol4/misc-loops/Holmakefile
+++ b/tests/hol4/loops/Holmakefile
diff --git a/tests/hol4/misc-loops/loops_FunsScript.sml b/tests/hol4/loops/loops_FunsScript.sml
index 65cf77d4..65cf77d4 100644
--- a/tests/hol4/misc-loops/loops_FunsScript.sml
+++ b/tests/hol4/loops/loops_FunsScript.sml
diff --git a/tests/hol4/misc-loops/loops_FunsTheory.sig b/tests/hol4/loops/loops_FunsTheory.sig
index 63fe56c9..63fe56c9 100644
--- a/tests/hol4/misc-loops/loops_FunsTheory.sig
+++ b/tests/hol4/loops/loops_FunsTheory.sig
diff --git a/tests/hol4/misc-loops/loops_TypesScript.sml b/tests/hol4/loops/loops_TypesScript.sml
index e3e5b8d1..e3e5b8d1 100644
--- a/tests/hol4/misc-loops/loops_TypesScript.sml
+++ b/tests/hol4/loops/loops_TypesScript.sml
diff --git a/tests/hol4/misc-loops/loops_TypesTheory.sig b/tests/hol4/loops/loops_TypesTheory.sig
index c3e638d8..c3e638d8 100644
--- a/tests/hol4/misc-loops/loops_TypesTheory.sig
+++ b/tests/hol4/loops/loops_TypesTheory.sig
diff --git a/tests/hol4/misc-no_nested_borrows/Holmakefile b/tests/hol4/no_nested_borrows/Holmakefile
index 3c4b8973..3c4b8973 100644
--- a/tests/hol4/misc-no_nested_borrows/Holmakefile
+++ b/tests/hol4/no_nested_borrows/Holmakefile
diff --git a/tests/hol4/misc-no_nested_borrows/noNestedBorrowsScript.sml b/tests/hol4/no_nested_borrows/noNestedBorrowsScript.sml
index 1b2d6121..1b2d6121 100644
--- a/tests/hol4/misc-no_nested_borrows/noNestedBorrowsScript.sml
+++ b/tests/hol4/no_nested_borrows/noNestedBorrowsScript.sml
diff --git a/tests/hol4/misc-no_nested_borrows/noNestedBorrowsTheory.sig b/tests/hol4/no_nested_borrows/noNestedBorrowsTheory.sig
index 67368e38..67368e38 100644
--- a/tests/hol4/misc-no_nested_borrows/noNestedBorrowsTheory.sig
+++ b/tests/hol4/no_nested_borrows/noNestedBorrowsTheory.sig
diff --git a/tests/hol4/misc-paper/Holmakefile b/tests/hol4/paper/Holmakefile
index 3c4b8973..3c4b8973 100644
--- a/tests/hol4/misc-paper/Holmakefile
+++ b/tests/hol4/paper/Holmakefile
diff --git a/tests/hol4/misc-paper/paperScript.sml b/tests/hol4/paper/paperScript.sml
index 3ac5b6ca..3ac5b6ca 100644
--- a/tests/hol4/misc-paper/paperScript.sml
+++ b/tests/hol4/paper/paperScript.sml
diff --git a/tests/hol4/misc-paper/paperTheory.sig b/tests/hol4/paper/paperTheory.sig
index 2da80da1..2da80da1 100644
--- a/tests/hol4/misc-paper/paperTheory.sig
+++ b/tests/hol4/paper/paperTheory.sig
diff --git a/tests/hol4/misc-polonius_list/Holmakefile b/tests/hol4/polonius_list/Holmakefile
index 3c4b8973..3c4b8973 100644
--- a/tests/hol4/misc-polonius_list/Holmakefile
+++ b/tests/hol4/polonius_list/Holmakefile
diff --git a/tests/hol4/misc-polonius_list/poloniusListScript.sml b/tests/hol4/polonius_list/poloniusListScript.sml
index 06876ed4..06876ed4 100644
--- a/tests/hol4/misc-polonius_list/poloniusListScript.sml
+++ b/tests/hol4/polonius_list/poloniusListScript.sml
diff --git a/tests/hol4/misc-polonius_list/poloniusListTheory.sig b/tests/hol4/polonius_list/poloniusListTheory.sig
index 41f21df7..41f21df7 100644
--- a/tests/hol4/misc-polonius_list/poloniusListTheory.sig
+++ b/tests/hol4/polonius_list/poloniusListTheory.sig
diff --git a/tests/test_runner/run_test.ml b/tests/test_runner/run_test.ml
index 8f356365..5d77bf9e 100644
--- a/tests/test_runner/run_test.ml
+++ b/tests/test_runner/run_test.ml
@@ -104,18 +104,6 @@ let charon_options_for_test test_name =
       [ "--polonius"; "--opaque=betree_utils"; "--crate"; "betree_main" ]
   | _ -> []
 
-(* The default subdirectory in which to store the outputs. *)
-(* This reproduces the file layout that was set by the old Makefile. FIXME: cleanup *)
-let test_subdir backend test_name =
-  match (backend, test_name) with
-  | Backend.Lean, _ -> "."
-  | _, "hashmap_main" -> "hashmap_on_disk"
-  | ( Backend.HOL4,
-      ( "constants" | "external" | "loops" | "no_nested_borrows" | "paper"
-      | "polonius_list" ) ) ->
-      "misc-" ^ test_name
-  | _ -> test_name
-
 (* The data for a specific test input *)
 module Input = struct
   type kind = SingleFile | Crate
@@ -131,6 +119,10 @@ module Input = struct
     subdirs : string BackendMap.t;
   }
 
+  (* The default subdirectory in which to store the outputs. *)
+  let default_subdir backend test_name =
+    match backend with Backend.Lean -> "." | _ -> test_name
+
   (* Parse lines that start `//@`. Each of them modifies the options we use for the test.
      Supported comments:
        - `skip`: don't process the file;
@@ -199,7 +191,9 @@ module Input = struct
     in
     let actions = BackendMap.make (fun _ -> Normal) in
     let charon_options = charon_options_for_test name in
-    let subdirs = BackendMap.make (fun backend -> test_subdir backend name) in
+    let subdirs =
+      BackendMap.make (fun backend -> default_subdir backend name)
+    in
     let aeneas_options =
       BackendMap.make (fun backend -> aeneas_options_for_test backend name)
     in