From e985be857f176e1c8b65a3e3e79e4547abef294e Mon Sep 17 00:00:00 2001
From: Michael Norrish <michael.norrish@anu.edu.au>
Date: Mon, 11 Sep 2023 14:46:11 +1000
Subject: [PATCH] Parallelise many Holmake test cases

---
 .../Holmake/tests/parallel_tests/Holmakefile  | 38 +++++++++++++++++++
 tools/sequences/kernel                        | 31 +--------------
 2 files changed, 39 insertions(+), 30 deletions(-)
 create mode 100644 tools/Holmake/tests/parallel_tests/Holmakefile

diff --git a/tools/Holmake/tests/parallel_tests/Holmakefile b/tools/Holmake/tests/parallel_tests/Holmakefile
new file mode 100644
index 0000000000..26a6add864
--- /dev/null
+++ b/tools/Holmake/tests/parallel_tests/Holmakefile
@@ -0,0 +1,38 @@
+CLINE_OPTIONS = -r
+DIRNAMES = \
+  altquote1 \
+  brokenstrings \
+  clinevars \
+  holpathdb/proj2 \
+  holpathdb/proj2/proj2A \
+  depchain1/dir3 \
+  depchain2/dir1 \
+  holdep \
+  nullary_tgt \
+  phony_tgt \
+  quote-filter \
+  theorytarget \
+  commandmacros \
+  doublecrnl \
+  coproduct \
+  noprereqs/dir1 \
+  noprereqs/dir2 \
+  noprereqs/dir3 \
+  noprereqs/dir4 \
+  indepchildren \
+  empty_script \
+  deps_of_depthys \
+  gh604 \
+  ignore_errors/j1 \
+  qfreadTheoremsyntax
+
+ifdef POLY
+DIRNAMES += cheatspotting \
+            depchain_heap/ \
+            depchain_heap/dir2 \
+            ignore_errors/j4 \
+            hollogs
+endif
+
+
+INCLUDES = $(patsubst %,../%,$(DIRNAMES))
diff --git a/tools/sequences/kernel b/tools/sequences/kernel
index 6e00f43ca4..f6513c5d3f 100644
--- a/tools/sequences/kernel
+++ b/tools/sequences/kernel
@@ -29,35 +29,6 @@ src/1
 src/proofman
 [poly]bin/hol.bare
 !src/proofman/tests
-!tools/Holmake/tests/clinevars
-!tools/Holmake/tests/holpathdb/proj2
-!tools/Holmake/tests/holpathdb/proj2/proj2A
-!tools/Holmake/tests/depchain1/dir3
-!tools/Holmake/tests/depchain2/dir1
-!tools/Holmake/tests/altquote1
-!tools/Holmake/tests/brokenstrings
-!tools/Holmake/tests/holdep
-!tools/Holmake/tests/nullary_tgt
-!tools/Holmake/tests/phony_tgt
-!tools/Holmake/tests/quote-filter
-!tools/Holmake/tests/theorytarget
-!tools/Holmake/tests/commandmacros
-!tools/Holmake/tests/doublecrnl
-[poly]!tools/Holmake/tests/cheatspotting
-[poly]!tools/Holmake/tests/depchain_heap/
-[poly]!tools/Holmake/tests/depchain_heap/dir2
-!tools/Holmake/tests/coproduct
-!tools/Holmake/tests/noprereqs/dir1
-!tools/Holmake/tests/noprereqs/dir2
-!tools/Holmake/tests/noprereqs/dir3
-!tools/Holmake/tests/noprereqs/dir4
-!tools/Holmake/tests/indepchildren
-!tools/Holmake/tests/empty_script
-!tools/Holmake/tests/deps_of_depthys
-!tools/Holmake/tests/gh604
-!tools/Holmake/tests/ignore_errors/j1
-!tools/Holmake/tests/qfreadTheoremsyntax
 !tools/Holmake/tests/preexec
-[poly]!tools/Holmake/tests/ignore_errors/j4
-[poly]!tools/Holmake/tests/hollogs
+!tools/Holmake/tests/parallel_tests
 !src/1/theory_tests