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..977bc108cc
--- /dev/null
+++ b/holproject.toml
@@ -0,0 +1,27 @@
+[holbuild]
+schema = 2
+minimum_version = "0.7.0"
+
+[project]
+name = "cakeml-compiler"
+version = "0.1.1"
+
+[build]
+roots = ["compiler/proofs/compilerProofScript.sml"]
+exclude = ["candle/*",
+           "compiler/benchmarks/*",
+           "compiler/bootstrap/*",
+           "translator/other-examples/*",
+           "unverified/*",
+           "tutorial/*",
+           "examples/*"]
+tactic_timeout = 180
+
+[dependencies.hol]
+git = "https://github.com/HOL-Theorem-Prover/HOL.git"
+rev = "d456022724bd61e57303339e998313b6580c592d"
+
+[dependencies.holextra]
+from = "hol"
+path = "."
+manifest = "holextra.manifest.toml"