From 95740823e5fcab1cda43d64a3516a71cc20f6d98 Mon Sep 17 00:00:00 2001
From: Wojciech Rozowski <wkroz@amazon.co.uk>
Date: Wed, 28 Oct 2026 12:11:21 +0000
Subject: [PATCH] Add Mantle and Pylate targets to lakefile.toml

The mirror from the internal StrataPythonFrontEnd package excludes
lakefile.toml, so the lean_lib/lean_exe declarations added alongside
Mantle (StrataMantle, StrataMantleTest, pymantle) and Pylate (Pylate,
PylateTests, pylate, pylateTests) never reached this repository, even
though their sources did.

Without a lean_lib owning the StrataMantle.* modules, Lake does not
build them and `lake build` fails on StrataPython.Mantle.Env with
"unknown module prefix 'StrataMantle'".

This ports those declarations (and the matching defaultTargets and
StrataPythonFrontEndTestMain needs) from the internal lakefile.
---
 lakefile.toml | 41 +++++++++++++++++++++++++++++++++++++++--
 1 file changed, 39 insertions(+), 2 deletions(-)

diff --git a/lakefile.toml b/lakefile.toml
index af8756c8..018e7537 100644
--- a/lakefile.toml
+++ b/lakefile.toml
@@ -1,6 +1,6 @@
 name = "StrataPython"
 version = "0.1.0"
-defaultTargets = ["StrataPython"]
+defaultTargets = ["StrataMantle", "StrataPython", "Pylate", "pylate", "pylateTests", "pyInterpret", "pymantle"]
 testDriver = "StrataPythonFrontEndTestMain"
 
 [leanOptions]
@@ -15,10 +15,37 @@ rev = "main"
 name = "PythonDialectIon"
 path = "Python/strata-python/dialects/Python.dialect.st.ion"
 
+[[lean_lib]]
+name = "StrataMantle"
+globs = ["StrataMantle.+"]
+
+[[lean_lib]]
+name = "StrataMantleTest"
+globs = ["StrataMantleTest.+"]
+
 [[lean_lib]]
 name = "StrataPython"
 extraDepTargets = ["PythonDialectIon"]
 
+# Pylate reads the Strata Python AST, so it needs the dialect (`Python_map`,
+# `Python.name`, `Command.ofAst`) from `StrataPython`, and the dialect Ion file
+# that `StrataPython` embeds -- hence the same `extraDepTargets` as that lib.
+[[lean_lib]]
+name = "Pylate"
+extraDepTargets = ["PythonDialectIon"]
+
+# Pylate's own Lean suites. They are a separate executable rather than the
+# package `testDriver`, because a package has exactly one and the host already
+# uses it for `StrataPythonFrontEndTestMain`.
+[[lean_lib]]
+name = "PylateTests"
+globs = ["Pylate.Tests.+"]
+
+[[lean_exe]]
+name = "pylateTests"
+root = "Pylate.Tests.Main"
+needs = ["Pylate", "StrataPython"]
+
 [[lean_lib]]
 name = "StrataPythonTest"
 globs = ["StrataPythonTest.+"]
@@ -29,7 +56,12 @@ globs = ["StrataPythonTestExtra.+"]
 
 [[lean_exe]]
 name = "StrataPythonFrontEndTestMain"
-needs = ["StrataPython", "StrataPythonTest"]
+needs = ["StrataPython", "StrataPythonTest", "StrataMantleTest", "pylateTests"]
+
+[[lean_exe]]
+name = "pylate"
+root = "Scripts.pylate"
+needs = ["Pylate", "StrataPython"]
 
 [[lean_exe]]
 name = "pyAnalyzeLaurel"
@@ -80,3 +112,8 @@ needs = ["StrataPython"]
 name = "strata"
 root = "StrataMain"
 needs = ["StrataPython"]
+
+[[lean_exe]]
+name = "pymantle"
+root = "Scripts.pymantle"
+needs = ["StrataPython"]