diff --git a/Auto/EvaluateAuto/TestAuto.lean b/Auto/EvaluateAuto/TestAuto.lean
index 5976ab7..351eb62 100644
--- a/Auto/EvaluateAuto/TestAuto.lean
+++ b/Auto/EvaluateAuto/TestAuto.lean
@@ -202,6 +202,11 @@ def Array.groupBySize (xs : Array α) (size : Nat) : Option (Array (Array α)) :
     let ret := Array.mk <| (List.range n).map (fun i => Array.mk <| (xs.toList.drop (size * i)).take size)
     some ret
 
+/--
+  This should be run after `import Mathlib, import Auto.EvaluateAuto.TestTactics`,
+  and should be run with a `cwd` where `lake env` creates an environment in which
+  `Mathlib` and `lean-auto` are available
+-/
 def evalAutoAtMathlibHumanTheorems (config : EvalAutoOnMathlibConfig) : CoreM Unit := do
   if !(← System.FilePath.isDir config.resultFolder) then
     IO.FS.createDir config.resultFolder
@@ -214,7 +219,7 @@ def evalAutoAtMathlibHumanTheorems (config : EvalAutoOnMathlibConfig) : CoreM Un
     evaluateFilesHandle.putStrLn (toString idx)
     evaluateFilesHandle.flush
     let evalProc ← EvalProc.create "lake" #["env", "lean", "--stdin"]
-    let logPath := config.resultFolder ++ toString idx
+    let logPath := config.resultFolder ++ "/" ++ toString idx
     evalProc.stdin.putStr (evalFile batch logPath)
     let (_, evalProc) ← evalProc.takeStdin
     running := running.push (idx, evalProc)
@@ -248,7 +253,7 @@ where
         "import Auto.Tactic",
         "open Lean EvalAuto",
         "",
-        "def thms : Std.HashSet Name := Std.HashSet.ofList ["
+        "def thms : Array Name := #["
       ] ++ thmsStrs ++ [
         "]",
         "",
diff --git a/Auto/EvaluateAuto/TestTactics.lean b/Auto/EvaluateAuto/TestTactics.lean
index 32700df..0994996 100644
--- a/Auto/EvaluateAuto/TestTactics.lean
+++ b/Auto/EvaluateAuto/TestTactics.lean
@@ -257,8 +257,9 @@ structure EvalTacticOnMathlibConfig where
   nthreads      : Nat
 
 /--
-  This should be run after `import Mathlib`, and should be run with a `cwd` where
-    `lake env` creates an environment in which `Mathlib` and `lean-auto` are available
+  This should be run after `import Mathlib` and `import Auto.EvaluateAuto.TestTactics`,
+  and should be run with a `cwd` where `lake env` creates an environment in which
+  `Mathlib` and `lean-auto` are available
 -/
 def evalTacticsAtMathlibHumanTheorems (config : EvalTacticOnMathlibConfig) : CoreM Unit := do
   let mms ← mathlibModules