From 34498197cb94e3eb07794d4bc7bcfc75f63d661d Mon Sep 17 00:00:00 2001
From: Ramana Kumar <ramana@member.fsf.org>
Date: Mon, 15 Jun 2026 18:58:59 +0100
Subject: [PATCH 1/3] Start drafting a holbuild-supported HOL project

Currently only for the compilerProof theory and its dependencies
---
 .gitignore             |  1 +
 holextra.manifest.toml | 22 ++++++++++++++++++++++
 holproject.toml        | 27 +++++++++++++++++++++++++++
 3 files changed, 50 insertions(+)
 create mode 100644 holextra.manifest.toml
 create mode 100644 holproject.toml

diff --git a/.gitignore b/.gitignore
index 7e23da29f5..2bffe7c21d 100644
--- a/.gitignore
+++ b/.gitignore
@@ -9,6 +9,7 @@
 .hol
 .HOLMK
 .hollogs
+.holbuild
 
 # TacticToe
 *Script_ttt.sml
diff --git a/holextra.manifest.toml b/holextra.manifest.toml
new file mode 100644
index 0000000000..c18f98b720
--- /dev/null
+++ b/holextra.manifest.toml
@@ -0,0 +1,22 @@
+[holbuild]
+schema = 2
+
+[project]
+name = "holextra"
+version = "0.1.0"
+
+[build]
+members = [
+  "src/transfer/examples",
+  "examples/formal-languages",
+  "examples/algorithms",
+  "examples/data-structures",
+  "examples/pl-semantics/lprefix_lub",
+  "examples/machine-code/multiword",
+  "examples/machine-code/hoare-triple",
+  "examples/l3-machine-code"
+]
+exclude = [
+  "examples/l3-machine-code/monadic-arm/*",
+  "*/selftest.sml"
+]
diff --git a/holproject.toml b/holproject.toml
new file mode 100644
index 0000000000..b577c573e8
--- /dev/null
+++ b/holproject.toml
@@ -0,0 +1,27 @@
+[holbuild]
+schema = 2
+required_version = "0.6.2"
+
+[project]
+name = "cakeml-compiler"
+version = "0.1.0"
+
+[build]
+roots = ["compiler/proofs/compilerProofScript.sml"]
+exclude = ["candle/*",
+           "compiler/benchmarks/*",
+           "compiler/bootstrap/*",
+           "translator/other-examples/*",
+           "unverified/*",
+           "tutorial/*",
+           "examples/*"]
+tactic_timeout = 90
+
+[dependencies.hol]
+git = "https://github.com/HOL-Theorem-Prover/HOL.git"
+rev = "9d7499d9bd45579524e6a8bb982571208b67a905"
+
+[dependencies.holextra]
+from = "hol"
+path = "."
+manifest = "holextra.manifest.toml"

From ee950602dd3d885c73d100d1172daeac0e386fe9 Mon Sep 17 00:00:00 2001
From: Ramana Kumar <ramana@member.fsf.org>
Date: Tue, 16 Jun 2026 11:42:54 +0100
Subject: [PATCH 2/3] Increase tactic timeout

---
 holproject.toml | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/holproject.toml b/holproject.toml
index b577c573e8..de2fb4f745 100644
--- a/holproject.toml
+++ b/holproject.toml
@@ -15,7 +15,7 @@ exclude = ["candle/*",
            "unverified/*",
            "tutorial/*",
            "examples/*"]
-tactic_timeout = 90
+tactic_timeout = 180
 
 [dependencies.hol]
 git = "https://github.com/HOL-Theorem-Prover/HOL.git"

From 059d8ec5cae03f6d1abbaf558ad8ebc123218767 Mon Sep 17 00:00:00 2001
From: Ramana Kumar <ramana@member.fsf.org>
Date: Wed, 17 Jun 2026 16:40:49 +0100
Subject: [PATCH 3/3] Bump versions

---
 holproject.toml | 6 +++---
 1 file changed, 3 insertions(+), 3 deletions(-)

diff --git a/holproject.toml b/holproject.toml
index de2fb4f745..977bc108cc 100644
--- a/holproject.toml
+++ b/holproject.toml
@@ -1,10 +1,10 @@
 [holbuild]
 schema = 2
-required_version = "0.6.2"
+minimum_version = "0.7.0"
 
 [project]
 name = "cakeml-compiler"
-version = "0.1.0"
+version = "0.1.1"
 
 [build]
 roots = ["compiler/proofs/compilerProofScript.sml"]
@@ -19,7 +19,7 @@ tactic_timeout = 180
 
 [dependencies.hol]
 git = "https://github.com/HOL-Theorem-Prover/HOL.git"
-rev = "9d7499d9bd45579524e6a8bb982571208b67a905"
+rev = "d456022724bd61e57303339e998313b6580c592d"
 
 [dependencies.holextra]
 from = "hol"