From 6bba17169d483d13ebb710642eaed7e235ca5059 Mon Sep 17 00:00:00 2001 From: Emilio Jesus Gallego Arias Date: Fri, 28 Aug 2026 15:16:34 +0200 Subject: [PATCH 1/5] refactor: simplify VBP generator execution --- scripts/run-lean-tests.sh | 2 + src/VersoBlueprint/VbpMain.lean | 63 ++++++++++--------- .../integration/check_vbp_failure_protocol.py | 58 +++++++++++++++++ 3 files changed, 94 insertions(+), 29 deletions(-) create mode 100644 tests/integration/check_vbp_failure_protocol.py diff --git a/scripts/run-lean-tests.sh b/scripts/run-lean-tests.sh index 487adfc3..62dd9e7a 100755 --- a/scripts/run-lean-tests.sh +++ b/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 diff --git a/src/VersoBlueprint/VbpMain.lean b/src/VersoBlueprint/VbpMain.lean index 1f3cf66f..e4c79d4a 100644 --- a/src/VersoBlueprint/VbpMain.lean +++ b/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,20 @@ def generatorModuleFromFile (path : FilePath) : String := text text.replace "/" "." -structure ProjectInfo where +private structure ProjectInfo 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 @@ -258,10 +267,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 +346,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 + (workspace : Lake.Workspace) (generatorFile : FilePath) (args : Array String) : IO UInt32 := do + try + let code ← workspace.evalLeanFile generatorFile args + unless code == 0 do + IO.eprintln s!"vbp build: generator run failed with exit code {code}: {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 +383,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 +private def generateSite (opts : BuildOptions) : IO UInt32 := do match ← projectInfo with - | .error err => pure (.error err) + | .error err => + IO.eprintln err + pure 1 | .ok info => - pure (.ok (info.workspace, { - generatorFile := info.generatorFile - generatorArgs := generatorLeanArgs info.generatorFile opts.output opts.verbose ++ pdfGeneratorArgs opts - })) + let args := generatorLeanArgs info.generatorFile opts.output opts.verbose ++ pdfGeneratorArgs opts + runGenerator info.workspace info.generatorFile args private def serveScript : String := String.intercalate "\n" [ "import functools, http.server, socketserver, sys", @@ -425,18 +435,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 diff --git a/tests/integration/check_vbp_failure_protocol.py b/tests/integration/check_vbp_failure_protocol.py new file mode 100644 index 00000000..9a8e7963 --- /dev/null +++ b/tests/integration/check_vbp_failure_protocol.py @@ -0,0 +1,58 @@ +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" + +LAKEFILE = """import Lake +open Lake DSL + +package BrokenBlueprint +""" + +GENERATOR = """import MissingBlueprintDependency + +-- PreviewManifest marks this file as the Blueprint generator fixture. +def main : IO Unit := pure () +""" + + +def main() -> int: + with tempfile.TemporaryDirectory(prefix="verso-blueprint-vbp-failure-") as tmp: + project = Path(tmp) + (project / "lean-toolchain").write_text(LEAN_TOOLCHAIN, encoding="utf-8") + (project / "lakefile.lean").write_text(LAKEFILE, encoding="utf-8") + (project / "BrokenBlueprintMain.lean").write_text(GENERATOR, encoding="utf-8") + + 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("vbp unexpectedly accepted a generator with a missing import") + if "vbp build: generator run failed" not in result.stderr: + raise SystemExit( + "vbp did not preserve its documented build-failure protocol\n" + f"stdout:\n{result.stdout}\n" + f"stderr:\n{result.stderr}" + ) + if "MissingBlueprintDependency" not in result.stdout + result.stderr: + raise SystemExit( + "vbp did not preserve the generator failure diagnostic\n" + f"stdout:\n{result.stdout}\n" + f"stderr:\n{result.stderr}" + ) + return 0 + + +if __name__ == "__main__": + raise SystemExit(main()) From b822e307810d6ede31e78ce9f4005836ba6cc465 Mon Sep 17 00:00:00 2001 From: Emilio Jesus Gallego Arias Date: Fri, 28 Aug 2026 15:16:40 +0200 Subject: [PATCH 2/5] doc: align VBP build descriptions --- README.md | 7 +++---- doc/GETTING_STARTED.md | 5 ++--- doc/MANUAL.md | 8 +++----- project_template/README.md | 5 ++--- scripts/README.md | 6 +++--- skills/verso-blueprint/references/vbp.md | 5 ++--- 6 files changed, 15 insertions(+), 21 deletions(-) diff --git a/README.md b/README.md index 66e25e91..9143288d 100644 --- a/README.md +++ b/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 diff --git a/doc/GETTING_STARTED.md b/doc/GETTING_STARTED.md index 96689f14..4dc1d787 100644 --- a/doc/GETTING_STARTED.md +++ b/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 diff --git a/doc/MANUAL.md b/doc/MANUAL.md index 4ca9dc6e..d60065ea 100644 --- a/doc/MANUAL.md +++ b/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 .lean -- --run .lean --output _out/site diff --git a/project_template/README.md b/project_template/README.md index 305b2e95..323ef480 100644 --- a/project_template/README.md +++ b/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: diff --git a/scripts/README.md b/scripts/README.md index e9164831..903b4911 100644 --- a/scripts/README.md +++ b/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 .lean -- --run .lean --output ...` -after building `+: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 diff --git a/skills/verso-blueprint/references/vbp.md b/skills/verso-blueprint/references/vbp.md index b6bde05f..ec2d0e9c 100644 --- a/skills/verso-blueprint/references/vbp.md +++ b/skills/verso-blueprint/references/vbp.md @@ -44,9 +44,8 @@ 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 .lean -- --run .lean --output From 304f9e70458860c93ad6e78dca81137f55935be2 Mon Sep 17 00:00:00 2001 From: Emilio Jesus Gallego Arias Date: Fri, 28 Aug 2026 15:44:58 +0200 Subject: [PATCH 3/5] refactor: normalize VBP generator context --- skills/verso-blueprint/references/vbp.md | 2 +- src/VersoBlueprint/VbpMain.lean | 31 ++--- .../integration/check_vbp_failure_protocol.py | 126 ++++++++++++++---- 3 files changed, 113 insertions(+), 46 deletions(-) diff --git a/skills/verso-blueprint/references/vbp.md b/skills/verso-blueprint/references/vbp.md index ec2d0e9c..952fdabd 100644 --- a/skills/verso-blueprint/references/vbp.md +++ b/skills/verso-blueprint/references/vbp.md @@ -52,7 +52,7 @@ lake lean .lean -- --run .lean --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 ` and `--pdf-runs ` are forwarded to the generator when the local project's `vbp` binary supports them; run `lake exe vbp --help` for the diff --git a/src/VersoBlueprint/VbpMain.lean b/src/VersoBlueprint/VbpMain.lean index e4c79d4a..d109183c 100644 --- a/src/VersoBlueprint/VbpMain.lean +++ b/src/VersoBlueprint/VbpMain.lean @@ -86,11 +86,9 @@ def generatorModuleFromFile (path : FilePath) : String := text text.replace "/" "." -private 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. @@ -192,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) @@ -206,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 @@ -231,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 @@ -384,13 +381,13 @@ private def pdfGeneratorArgs (opts : BuildOptions) : Array String := | none => args private def generateSite (opts : BuildOptions) : IO UInt32 := do - match ← projectInfo with + match ← generatorContext with | .error err => IO.eprintln err pure 1 - | .ok info => - let args := generatorLeanArgs info.generatorFile opts.output opts.verbose ++ pdfGeneratorArgs opts - runGenerator info.workspace info.generatorFile args + | .ok context => + let args := generatorLeanArgs context.generatorFile opts.output opts.verbose ++ pdfGeneratorArgs opts + runGenerator context.workspace context.generatorFile args private def serveScript : String := String.intercalate "\n" [ "import functools, http.server, socketserver, sys", diff --git a/tests/integration/check_vbp_failure_protocol.py b/tests/integration/check_vbp_failure_protocol.py index 9a8e7963..a5b34aa0 100644 --- a/tests/integration/check_vbp_failure_protocol.py +++ b/tests/integration/check_vbp_failure_protocol.py @@ -10,47 +10,117 @@ LEAN_LOW_PRIORITY = PACKAGE_ROOT / "scripts" / "lean-low-priority" VBP = PACKAGE_ROOT / ".lake" / "build" / "bin" / "vbp" -LAKEFILE = """import Lake +MISSING_IMPORT_LAKEFILE = """import Lake open Lake DSL -package BrokenBlueprint +package MissingImportBlueprint """ -GENERATOR = """import MissingBlueprintDependency +MISSING_IMPORT_GENERATOR = """import MissingBlueprintDependency -- PreviewManifest marks this file as the Blueprint generator fixture. def main : IO Unit := pure () """ +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 + +-- PreviewManifest marks this file as the Blueprint generator fixture. +def main : IO Unit := pure () +""" + + +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: - project = Path(tmp) - (project / "lean-toolchain").write_text(LEAN_TOOLCHAIN, encoding="utf-8") - (project / "lakefile.lean").write_text(LAKEFILE, encoding="utf-8") - (project / "BrokenBlueprintMain.lean").write_text(GENERATOR, encoding="utf-8") - - result = subprocess.run( - [str(LEAN_LOW_PRIORITY), "lake", "env", str(VBP), "build"], - cwd=project, - check=False, - text=True, - capture_output=True, + root = Path(tmp) + 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", + ) + + 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: build failed", + expected_diagnostic="missing-generator-input.txt", ) - if result.returncode == 0: - raise SystemExit("vbp unexpectedly accepted a generator with a missing import") - if "vbp build: generator run failed" not in result.stderr: - raise SystemExit( - "vbp did not preserve its documented build-failure protocol\n" - f"stdout:\n{result.stdout}\n" - f"stderr:\n{result.stderr}" - ) - if "MissingBlueprintDependency" not in result.stdout + result.stderr: - raise SystemExit( - "vbp did not preserve the generator failure diagnostic\n" - f"stdout:\n{result.stdout}\n" - f"stderr:\n{result.stderr}" - ) return 0 From fadd1b3d703575b8cb2bfafaac6a51ea744b77a0 Mon Sep 17 00:00:00 2001 From: Emilio Jesus Gallego Arias Date: Fri, 28 Aug 2026 15:56:05 +0200 Subject: [PATCH 4/5] refactor: pass VBP generator context directly --- src/VersoBlueprint/VbpMain.lean | 8 ++++---- tests/integration/check_vbp_failure_protocol.py | 4 +++- 2 files changed, 7 insertions(+), 5 deletions(-) diff --git a/src/VersoBlueprint/VbpMain.lean b/src/VersoBlueprint/VbpMain.lean index d109183c..5fc6708b 100644 --- a/src/VersoBlueprint/VbpMain.lean +++ b/src/VersoBlueprint/VbpMain.lean @@ -344,11 +344,11 @@ private def runAttached (cmd : String) (args : Array String) : IO UInt32 := do child.wait private def runGenerator - (workspace : Lake.Workspace) (generatorFile : FilePath) (args : Array String) : IO UInt32 := do + (context : GeneratorContext) (args : Array String) : IO UInt32 := do try - let code ← workspace.evalLeanFile generatorFile args + let code ← context.workspace.evalLeanFile context.generatorFile args unless code == 0 do - IO.eprintln s!"vbp build: generator run failed with exit code {code}: {generatorFile}" + 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}" @@ -387,7 +387,7 @@ private def generateSite (opts : BuildOptions) : IO UInt32 := do pure 1 | .ok context => let args := generatorLeanArgs context.generatorFile opts.output opts.verbose ++ pdfGeneratorArgs opts - runGenerator context.workspace context.generatorFile args + runGenerator context args private def serveScript : String := String.intercalate "\n" [ "import functools, http.server, socketserver, sys", diff --git a/tests/integration/check_vbp_failure_protocol.py b/tests/integration/check_vbp_failure_protocol.py index a5b34aa0..eddb01c3 100644 --- a/tests/integration/check_vbp_failure_protocol.py +++ b/tests/integration/check_vbp_failure_protocol.py @@ -95,6 +95,7 @@ def assert_build_failure( 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", @@ -107,6 +108,7 @@ def main() -> int: expected_diagnostic="MissingBlueprintDependency", ) + # A missing Lake input fails dependency preparation, so evalLeanFile throws. missing_need = write_project( root, "missing-need", @@ -118,7 +120,7 @@ def main() -> int: ) assert_build_failure( missing_need, - expected_protocol="vbp build: generator run failed: build failed", + expected_protocol="vbp build: generator run failed:", expected_diagnostic="missing-generator-input.txt", ) return 0 From 1c11317d110a1beb6af8f2603620e274e93be9be Mon Sep 17 00:00:00 2001 From: Emilio Jesus Gallego Arias Date: Fri, 28 Aug 2026 16:22:52 +0200 Subject: [PATCH 5/5] test: use a real VBP generator marker --- tests/integration/check_vbp_failure_protocol.py | 8 ++++---- 1 file changed, 4 insertions(+), 4 deletions(-) diff --git a/tests/integration/check_vbp_failure_protocol.py b/tests/integration/check_vbp_failure_protocol.py index eddb01c3..55d3cf4b 100644 --- a/tests/integration/check_vbp_failure_protocol.py +++ b/tests/integration/check_vbp_failure_protocol.py @@ -18,8 +18,8 @@ MISSING_IMPORT_GENERATOR = """import MissingBlueprintDependency --- PreviewManifest marks this file as the Blueprint generator fixture. -def main : IO Unit := pure () +def blueprintMain : IO Unit := pure () +def main : IO Unit := blueprintMain """ MISSING_NEED_LAKEFILE = """import Lake @@ -41,8 +41,8 @@ def main : IO Unit := pure () MISSING_NEED_GENERATOR = """import MissingInputBlueprint --- PreviewManifest marks this file as the Blueprint generator fixture. -def main : IO Unit := pure () +def blueprintMain : IO Unit := pure () +def main : IO Unit := blueprintMain """