refactor: simplify VBP generator execution

README.md

@@ -459,10 +459,9 @@ project discovery, build/serve previews, generated-data queries, and
 post-edit checks.
 
 `lake exe vbp build` is the normal Blueprint generation interface for projects.
-Once running, VBP loads the project workspace and reuses it for both generator
-discovery and Lake's Lean-file runner. Treat `vbp` query JSON as an unstable
-agent interface, not a public compatibility contract and not part of the
-documented integration API.
+It discovers the project generator and asks Lake to build its imports and run
+it. Treat `vbp` query JSON as an unstable agent interface, not a public
+compatibility contract and not part of the documented integration API.
 
 ### Maintainer CLI Split
 

doc/GETTING_STARTED.md

@@ -182,9 +182,8 @@ that the included GitHub Pages workflow uses. Internally that script uses:
 lake exe vbp build
 ```
 
-Once running, the project helper loads the Lake workspace and reuses it for
-generator discovery and Lake's Lean-file runner. The runner builds the
-generator's imports and executes it. The corresponding lower-level command is:
+The project helper discovers the generator, then uses Lake to build its imports
+and execute it. The corresponding lower-level command is:
 
 ```bash
 lake lean ProjectTemplateMain.lean -- --run ProjectTemplateMain.lean --output _out/site

doc/MANUAL.md

@@ -1163,11 +1163,9 @@ lake exe vbp build
 lake exe vbp build --serve
 ```
 
-Once running, it loads the project workspace and reuses it for generator
-discovery and Lake's Lean-file runner. The runner builds the generator's
-imports and executes it; VBP can then optionally serve the result. When a
-maintainer harness or advanced CI job cannot use `vbp`, the equivalent
-lower-level command is:
+It discovers the generator, then uses Lake to build its imports and execute it;
+VBP can optionally serve the result. When a maintainer harness or advanced CI
+job cannot use `vbp`, the equivalent lower-level command is:
 
 ```bash
 lake lean <GeneratorMain>.lean -- --run <GeneratorMain>.lean --output _out/site

project_template/README.md

@@ -95,9 +95,8 @@ project helper:
 lake exe vbp build
 ```
 
-`vbp build` builds the Lean library artifacts, prepares the generator file, and
-then runs the generator through Lake's Lean wrapper without relying on a
-separate Lake executable target.
+`vbp build` discovers the generator, then uses Lake to build its imports and
+execute it without requiring a separate generator executable target.
 
 To build a PDF locally, run:
 

scripts/README.md

@@ -7,9 +7,9 @@ For package-facing usage, use `lake exe vbp build` or the project's Blueprint
 generator entry point, not the Python harness here. CI and Mathlib-heavy
 projects can run
 `lake lean <GeneratorMain>.lean -- --run <GeneratorMain>.lean --output ...`
-after building `+<BlueprintLibrary>:olean`. Keep the explicit OLean facet so
-generation cannot trigger native C builds of Mathlib dependencies. Start with
-the top-level [`README.md`](../README.md) and [`doc/MANUAL.md`](../doc/MANUAL.md).
+when they need to drive the generator explicitly; Lake builds the generator's
+imports as part of that command. Start with the top-level
+[`README.md`](../README.md) and [`doc/MANUAL.md`](../doc/MANUAL.md).
 
 For repository maintenance, the canonical workflow document is
 [`doc/MAINTAINER_GUIDE.md`](../doc/MAINTAINER_GUIDE.md). This README is

scripts/run-lean-tests.sh

@@ -6,5 +6,7 @@ package_root="$(cd "$(dirname "$0")/.." && pwd)"
 cd "$package_root"
 
 ./scripts/lean-low-priority lake test
+./scripts/lean-low-priority lake build vbp
 python3 tests/integration/check_lean_run_external_markup.py
 python3 tests/integration/check_embedded_asset_cache.py
+python3 tests/integration/check_vbp_failure_protocol.py

skills/verso-blueprint/references/vbp.md

@@ -44,16 +44,15 @@ Defaults:
 
 `discover` reports the Lake-backed package, generator entry point, generator module, generator source file, and default output paths. Fields ending in `Guess`, such as `topLevelBlueprintModuleGuess` and `chapterCandidateGuesses`, are convention-based hints for agents and may be null or incomplete. The JSON includes `"apiStability":"unstable"` and a `discoveryErrors` array. When Lake workspace discovery fails or no generator entry point can be found, package and generator fields are null and `discoveryErrors` explains why.
 
-Once running, `build` loads the project workspace and reuses it to discover the
-generator and invoke Lake's Lean-file runner. The runner builds the generator's
-imports and executes the generator through Lean's interpreter:
+`build` discovers the generator, then uses Lake's Lean-file runner to build its
+imports and execute it through Lean's interpreter:
 
 ```bash
 lake lean <GeneratorMain>.lean -- --run <GeneratorMain>.lean --output <output>
 ```
 
 `build --verbose` passes `--verbose` through to the generator run, enabling
-Blueprint generation phase progress after Lake has prepared the generator.
+Blueprint generation phase progress.
 Pass `--pdf` to build `_out/site/pdf/main.pdf` from the generated TeX output.
 `--pdf-engine <cmd>` and `--pdf-runs <n>` are forwarded to the generator when
 the local project's `vbp` binary supports them; run `lake exe vbp --help` for the

src/VersoBlueprint/VbpMain.lean

@@ -5,7 +5,8 @@ Author: Emilio J. Gallego Arias
 -/
 
 import VersoBlueprint.Vbp
-import Lake.CLI.Main
+import Lake.CLI.Actions
+import Lake.Load.Workspace
 
 open Lean
 open System
@@ -85,12 +86,18 @@ def generatorModuleFromFile (path : FilePath) : String :=
       text
   text.replace "/" "."
 
-structure ProjectInfo where
+private structure GeneratorContext where
   workspace : Lake.Workspace
-  packageName : String
   generatorFile : FilePath
-  generatorModule : String
 
+/--
+Resolve Lake relative to the Lean installation selected for the project.
+
+Unlike the `lake` executable, `vbp` is built inside the project, so Lake cannot
+discover a co-located Lean installation from `IO.appPath`. In an Elan toolchain,
+`LAKE_HOME` can also name Lean's sysroot, whose Lake layout is represented by
+`LakeInstall.ofLean` rather than the standalone Lake build layout.
+-/
 private def findLakeInstallForLean
     (leanInstall : Lake.LeanInstall) : BaseIO (Option Lake.LakeInstall) := do
   if let some home ← IO.getEnv "LAKE_HOME" then
@@ -183,7 +190,7 @@ private def findGeneratorFile? (cwd : FilePath) (packageName : String) : IO (Opt
       let rootFiles ← rootLeanFiles cwd
       firstGeneratorLikeFile? cwd rootFiles.toList
 
-private def projectInfo : IO (Except String ProjectInfo) := do
+private def generatorContext : IO (Except String GeneratorContext) := do
   let cwd ← IO.currentDir
   match ← loadWorkspace with
   | .error err => pure (.error err)
@@ -197,9 +204,7 @@ private def projectInfo : IO (Except String ProjectInfo) := do
       | some generatorFile =>
           pure (.ok {
             workspace,
-            packageName,
-            generatorFile,
-            generatorModule := generatorModuleFromFile generatorFile
+            generatorFile
           })
 
 private def chapterCandidates (cwd : FilePath) (packageName? : Option String) : IO (Array String) := do
@@ -222,12 +227,13 @@ private def chapterCandidates (cwd : FilePath) (packageName? : Option String) :
 
 def discover : IO UInt32 := do
   let cwd ← IO.currentDir
-  let info? ← projectInfo
-  let (packageName?, generator?, generatorModule?, discoveryErrors) :=
-    match info? with
-    | .ok info =>
-        (some info.packageName, some info.generatorFile, some info.generatorModule, #[])
-    | .error err => (none, none, none, #[err])
+  let context? ← generatorContext
+  let (packageName?, generator?, discoveryErrors) :=
+    match context? with
+    | .ok context =>
+        (some context.workspace.root.prettyName, some context.generatorFile, #[])
+    | .error err => (none, none, #[err])
+  let generatorModule? := generator?.map generatorModuleFromFile
   let topLevel? ←
     match generator? with
     | none => pure none
@@ -258,10 +264,6 @@ structure BuildOptions where
   serve : Bool := false
   port? : Option Nat := none
 
-structure BuildPlan where
-  generatorFile : FilePath
-  generatorArgs : Array String
-
 private def maxTcpPort : Nat := 65535
 
 private def parseTcpPort (raw : String) : Except String Nat :=
@@ -341,11 +343,16 @@ private def runAttached (cmd : String) (args : Array String) : IO UInt32 := do
   let child ← IO.Process.spawn { cmd, args }
   child.wait
 
-private def runGenerator (workspace : Lake.Workspace) (plan : BuildPlan) : IO UInt32 := do
-  let code ← workspace.evalLeanFile plan.generatorFile plan.generatorArgs
-  unless code == 0 do
-    IO.eprintln s!"vbp build: generator run failed with exit code {code}: {plan.generatorFile}"
-  pure code
+private def runGenerator
+    (context : GeneratorContext) (args : Array String) : IO UInt32 := do
+  try
+    let code ← context.workspace.evalLeanFile context.generatorFile args
+    unless code == 0 do
+      IO.eprintln s!"vbp build: generator run failed with exit code {code}: {context.generatorFile}"
+    pure code
+  catch err =>
+    IO.eprintln s!"vbp build: generator run failed: {err}"
+    pure 1
 
 /--
 Run a generator through Lake's Lean setup.
@@ -373,14 +380,14 @@ private def pdfGeneratorArgs (opts : BuildOptions) : Array String :=
   | some runs => args ++ #[Informal.PreviewManifest.pdfRunsFlag, toString runs]
   | none => args
 
-private def buildPlan (opts : BuildOptions) : IO (Except String (Lake.Workspace × BuildPlan)) := do
-  match ← projectInfo with
-  | .error err => pure (.error err)
-  | .ok info =>
-      pure (.ok (info.workspace, {
-        generatorFile := info.generatorFile
-        generatorArgs := generatorLeanArgs info.generatorFile opts.output opts.verbose ++ pdfGeneratorArgs opts
-      }))
+private def generateSite (opts : BuildOptions) : IO UInt32 := do
+  match ← generatorContext with
+  | .error err =>
+      IO.eprintln err
+      pure 1
+  | .ok context =>
+      let args := generatorLeanArgs context.generatorFile opts.output opts.verbose ++ pdfGeneratorArgs opts
+      runGenerator context args
 
 private def serveScript : String := String.intercalate "\n" [
   "import functools, http.server, socketserver, sys",
@@ -425,18 +432,13 @@ def build (args : List String) : IO UInt32 := do
           IO.eprintln err
           pure 2
       | .ok opts =>
-          match ← buildPlan opts with
-          | .error err =>
-              IO.eprintln err
-              pure 1
-          | .ok (workspace, plan) =>
-              let code ← runGenerator workspace plan
-              if code != 0 then
-                pure code
-              else if opts.serve then
-                serve opts.output opts.port?
-              else
-                pure 0
+          let code ← generateSite opts
+          if code != 0 then
+            pure code
+          else if opts.serve then
+            serve opts.output opts.port?
+          else
+            pure 0
 
 def query (args : List String) : IO UInt32 := do
   match parseSiteOptions args {} with

tests/integration/check_vbp_failure_protocol.py

@@ -0,0 +1,130 @@
+from __future__ import annotations
+
+import subprocess
+import tempfile
+from pathlib import Path
+
+
+PACKAGE_ROOT = Path(__file__).resolve().parents[2]
+LEAN_TOOLCHAIN = (PACKAGE_ROOT / "lean-toolchain").read_text(encoding="utf-8")
+LEAN_LOW_PRIORITY = PACKAGE_ROOT / "scripts" / "lean-low-priority"
+VBP = PACKAGE_ROOT / ".lake" / "build" / "bin" / "vbp"
+
+MISSING_IMPORT_LAKEFILE = """import Lake
+open Lake DSL
+
+package MissingImportBlueprint
+"""
+
+MISSING_IMPORT_GENERATOR = """import MissingBlueprintDependency
+
+def blueprintMain : IO Unit := pure ()
+def main : IO Unit := blueprintMain
+"""
+
+MISSING_NEED_LAKEFILE = """import Lake
+open Lake DSL
+
+package MissingInputBlueprint
+
+input_file missingGeneratorInput where
+  path := "missing-generator-input.txt"
+  text := true
+
+lean_lib MissingInputBlueprint where
+  roots := #[`MissingInputBlueprint]
+  needs := #[missingGeneratorInput]
+"""
+
+MISSING_NEED_MODULE = """def witness : Nat := 1
+"""
+
+MISSING_NEED_GENERATOR = """import MissingInputBlueprint
+
+def blueprintMain : IO Unit := pure ()
+def main : IO Unit := blueprintMain
+"""
+
+
+def write_project(
+    root: Path,
+    name: str,
+    lakefile: str,
+    files: dict[str, str],
+) -> Path:
+    project = root / name
+    project.mkdir()
+    (project / "lean-toolchain").write_text(LEAN_TOOLCHAIN, encoding="utf-8")
+    (project / "lakefile.lean").write_text(lakefile, encoding="utf-8")
+    for path, contents in files.items():
+        (project / path).write_text(contents, encoding="utf-8")
+    return project
+
+
+def assert_build_failure(
+    project: Path,
+    *,
+    expected_protocol: str,
+    expected_diagnostic: str,
+) -> None:
+    result = subprocess.run(
+        [str(LEAN_LOW_PRIORITY), "lake", "env", str(VBP), "build"],
+        cwd=project,
+        check=False,
+        text=True,
+        capture_output=True,
+    )
+    if result.returncode == 0:
+        raise SystemExit(f"vbp unexpectedly accepted invalid project {project.name}")
+    if expected_protocol not in result.stderr:
+        raise SystemExit(
+            f"vbp did not preserve its build-failure protocol for {project.name}; "
+            f"expected {expected_protocol!r}\n"
+            f"stdout:\n{result.stdout}\n"
+            f"stderr:\n{result.stderr}"
+        )
+    if expected_diagnostic not in result.stdout + result.stderr:
+        raise SystemExit(
+            f"vbp did not preserve the underlying diagnostic for {project.name}; "
+            f"expected {expected_diagnostic!r}\n"
+            f"stdout:\n{result.stdout}\n"
+            f"stderr:\n{result.stderr}"
+        )
+
+
+def main() -> int:
+    with tempfile.TemporaryDirectory(prefix="verso-blueprint-vbp-failure-") as tmp:
+        root = Path(tmp)
+        # An invalid import reaches Lean, which returns a nonzero process exit code.
+        missing_import = write_project(
+            root,
+            "missing-import",
+            MISSING_IMPORT_LAKEFILE,
+            {"MissingImportBlueprintMain.lean": MISSING_IMPORT_GENERATOR},
+        )
+        assert_build_failure(
+            missing_import,
+            expected_protocol="vbp build: generator run failed with exit code 1",
+            expected_diagnostic="MissingBlueprintDependency",
+        )
+
+        # A missing Lake input fails dependency preparation, so evalLeanFile throws.
+        missing_need = write_project(
+            root,
+            "missing-need",
+            MISSING_NEED_LAKEFILE,
+            {
+                "MissingInputBlueprint.lean": MISSING_NEED_MODULE,
+                "MissingInputBlueprintMain.lean": MISSING_NEED_GENERATOR,
+            },
+        )
+        assert_build_failure(
+            missing_need,
+            expected_protocol="vbp build: generator run failed:",
+            expected_diagnostic="missing-generator-input.txt",
+        )
+    return 0
+
+
+if __name__ == "__main__":
+    raise SystemExit(main())