From f00a14a96cdcc5e1eb0d5b7388f474a507bb2b6d Mon Sep 17 00:00:00 2001 From: Codex Date: Sun, 6 Sep 2026 05:13:13 +0800 Subject: [PATCH] fix(verso): route project output to isolated fragment --- ...-project-finalizers-and-branch-assembly.md | 6 ++ sdk/verso/README.md | 6 ++ sdk/verso/src/verso_build_sdk/commands.py | 11 ++- sdk/verso/src/verso_build_sdk/config.py | 15 ++++ sdk/verso/tests/test_sdk.py | 89 ++++++++++++++++++- tests/test_repository_scripts.py | 50 +++++++++-- 6 files changed, 168 insertions(+), 9 deletions(-) diff --git a/docs/decisions/0006-project-finalizers-and-branch-assembly.md b/docs/decisions/0006-project-finalizers-and-branch-assembly.md index 29068fae5..380a44f3b 100644 --- a/docs/decisions/0006-project-finalizers-and-branch-assembly.md +++ b/docs/decisions/0006-project-finalizers-and-branch-assembly.md @@ -43,6 +43,12 @@ reinterpret an in-flight branch job. It emits an identity-bound route/module inventory, does not rewrite branch-wide source overviews or README files, and does not claim the shared root catalog. +- A project fragment's disjoint Verso output is part of the executable + contract, not merely a post-build assertion. The generic Verso SDK passes + the normalized absolute directory to `lake exe --output ` + and rejects non-executable targets or a second explicit `--output`. This + keeps the generated files and the fragment manifest under the same worker- + owned root instead of silently accepting Verso's shared `_site` default. - A project worker gets a private mutable finalizer workspace. The immutable branch Lean cache remains read-only. No two project workers share a mutable Lake/Web directory or branch result path. diff --git a/sdk/verso/README.md b/sdk/verso/README.md index 792ccf019..25db26fd1 100644 --- a/sdk/verso/README.md +++ b/sdk/verso/README.md @@ -54,6 +54,12 @@ Useful environment settings use the `VERSO_` prefix: `VERSO_TOOLCHAIN`, explicit build environment variable. Credentials and platform-specific values are intentionally outside this SDK. +When `VERSO_OUTPUT_DIR` or `--output-dir` is set, the SDK resolves it to an +absolute path and passes it to Verso as `--output`; the environment variable is +not consumed by the generated Lean executable itself. Do not also put an +explicit `--output` in `VERSO_TARGETS`: the SDK rejects that ambiguous +combination instead of relying on option order. + `verso-literate` accepts `REASBOOK_BUILD_LAKE_BIN`, `REASBOOK_LITERATE_JOBS`, `REASBOOK_LITERATE_VALIDATION_JOBS`, `REASBOOK_LITERATE_CHUNK_SIZE`, and diff --git a/sdk/verso/src/verso_build_sdk/commands.py b/sdk/verso/src/verso_build_sdk/commands.py index 7f23a73a3..8e134a2bd 100644 --- a/sdk/verso/src/verso_build_sdk/commands.py +++ b/sdk/verso/src/verso_build_sdk/commands.py @@ -59,9 +59,14 @@ def pipeline(config: VersoBuildConfig) -> tuple[CommandSpec, ...]: generator_cwd = config.generator_cwd or config.web_root if config.generator: commands.append(CommandSpec("generate", config.generator, generator_cwd)) - commands.append( - CommandSpec("build", lake_argv(config, *config.targets), config.web_root) - ) + targets = config.targets + if config.output_dir is not None: + # ``Verso.Genre.Blog.blogMain`` accepts this option after the Lake + # executable target. Passing it explicitly is essential for + # concurrent project finalizers: an environment variable alone is not + # consumed by the generated Lean executable. + targets = (*targets, "--output", str(config.output_dir)) + commands.append(CommandSpec("build", lake_argv(config, *targets), config.web_root)) return tuple(commands) diff --git a/sdk/verso/src/verso_build_sdk/config.py b/sdk/verso/src/verso_build_sdk/config.py index 05c5e9846..295462a95 100644 --- a/sdk/verso/src/verso_build_sdk/config.py +++ b/sdk/verso/src/verso_build_sdk/config.py @@ -151,6 +151,21 @@ def validate(self) -> None: raise VersoBuildError("lake_bin and elan_bin must be non-empty") if not self.targets: raise VersoBuildError("at least one Lake target is required") + if self.output_dir is not None: + if ( + len(self.targets) < 2 + or self.targets[0] != "exe" + or not self.targets[1] + or self.targets[1].startswith("-") + ): + raise VersoBuildError( + "output_dir requires targets to start with 'exe' and an " + "executable name" + ) + if "--output" in self.targets: + raise VersoBuildError( + "output_dir may not be combined with an explicit --output target" + ) for value in (*self.targets, *self.generator, self.lake_bin, self.elan_bin): if any(char in value for char in "\x00\r\n"): raise VersoBuildError( diff --git a/sdk/verso/tests/test_sdk.py b/sdk/verso/tests/test_sdk.py index 669b6d417..9123f628b 100644 --- a/sdk/verso/tests/test_sdk.py +++ b/sdk/verso/tests/test_sdk.py @@ -12,7 +12,7 @@ discover_project, lake_argv, ) -from verso_build_sdk.errors import CommandExecutionError +from verso_build_sdk.errors import CommandExecutionError, VersoBuildError class RecordingRunner: @@ -35,6 +35,21 @@ def run(self, command: Command): ) +class SimulatedVersoRunner(RecordingRunner): + """Model Verso's CLI output selection without invoking Lean.""" + + def run(self, command: Command): + self.calls.append((tuple(command.argv), command.cwd)) + argv = tuple(command.argv) + output = command.cwd / "_site" + if "--output" in argv: + option = argv.index("--output") + output = Path(argv[option + 1]) + output.mkdir(parents=True) + (output / "index.html").write_text("site\n", encoding="utf-8") + return CommandResult(argv=command.argv, command=command, returncode=0) + + class VersoSdkTests(unittest.TestCase): def project(self, root: Path) -> None: (root / "lakefile.lean").write_text( @@ -113,6 +128,78 @@ def test_dry_run_does_not_execute(self) -> None: self.assertTrue(result.dry_run) self.assertEqual(runner.calls, []) + def test_configured_output_dir_is_passed_to_verso_executable(self) -> None: + with tempfile.TemporaryDirectory() as temp: + root = Path(temp) / "web" + root.mkdir() + self.project(root) + output = ( + Path(temp) / "artifacts with spaces" / "project" / "site" + ).resolve() + runner = SimulatedVersoRunner() + + result = VersoBuilder( + VersoBuildConfig( + web_root=root, + output_dir=output, + verify_output=True, + ), + runner=runner, + ).run() + + self.assertEqual(result.output_dir, output) + self.assertTrue((output / "index.html").is_file()) + self.assertFalse((root / "_site").exists()) + self.assertEqual(runner.calls[-1][0][-2:], ("--output", str(output))) + + def test_dry_run_plans_the_resolved_output_dir(self) -> None: + with tempfile.TemporaryDirectory() as temp: + root = Path(temp) / "web" + root.mkdir() + self.project(root) + output = (Path(temp) / "artifacts" / "site").resolve() + runner = RecordingRunner() + + result = VersoBuilder( + VersoBuildConfig(web_root=root, output_dir=output), + runner=runner, + ).run(dry_run=True) + + self.assertEqual(result.output_dir, output) + self.assertEqual(result.commands[-1].argv[-2:], ("--output", str(output))) + self.assertEqual(runner.calls, []) + + def test_output_dir_rejects_an_explicit_output_target(self) -> None: + with tempfile.TemporaryDirectory() as temp: + root = Path(temp) / "web" + root.mkdir() + self.project(root) + output = (Path(temp) / "configured-site").resolve() + + with self.assertRaisesRegex(VersoBuildError, "output_dir.*--output"): + VersoBuilder( + VersoBuildConfig( + web_root=root, + output_dir=output, + targets=("exe", "site", "--output", str(root / "other-site")), + ) + ).plan() + + def test_output_dir_requires_a_verso_executable_target(self) -> None: + with tempfile.TemporaryDirectory() as temp: + root = Path(temp) / "web" + root.mkdir() + self.project(root) + + with self.assertRaisesRegex(VersoBuildError, "output_dir requires targets"): + VersoBuilder( + VersoBuildConfig( + web_root=root, + output_dir=Path(temp) / "site", + targets=("build", "site"), + ) + ).plan() + def test_runner_failure_is_reported(self) -> None: with tempfile.TemporaryDirectory() as temp: root = Path(temp) diff --git a/tests/test_repository_scripts.py b/tests/test_repository_scripts.py index 28cfa2108..02dfe584a 100644 --- a/tests/test_repository_scripts.py +++ b/tests/test_repository_scripts.py @@ -1318,14 +1318,39 @@ def test_verso_project_fragment_writes_validated_disjoint_manifest(self) -> None build = verso_bin / "verso-build" build.write_text( "#!/usr/bin/env bash\nset -eu\n" - 'mkdir -p "$VERSO_OUTPUT_DIR/books/selected/book"\n' - 'mkdir -p "$VERSO_OUTPUT_DIR/books/selected"\n' - ': > "$VERSO_OUTPUT_DIR/index.html"\n' - ': > "$VERSO_OUTPUT_DIR/books/selected/index.html"\n' - ': > "$VERSO_OUTPUT_DIR/books/selected/book/index.html"\n', + 'exec "$REASBOOK_TEST_PYTHON" -m verso_build_sdk "$@"\n', encoding="utf-8", ) build.chmod(0o755) + executable_argv = Path(temp) / "verso-executable-argv" + fake_elan = repo / "fake-elan" + fake_elan.write_text( + "#!/usr/bin/env bash\nset -euo pipefail\n" + 'printf \'%s\\n\' "$@" > "$VERSO_EXECUTABLE_ARGV"\n' + 'output=""\n' + 'while [[ "$#" -gt 0 ]]; do\n' + ' if [[ "$1" == --output ]]; then\n' + ' [[ "$#" -ge 2 ]] || exit 9\n' + ' output="$2"\n' + " shift 2\n" + " else\n" + " shift\n" + " fi\n" + "done\n" + '[[ -n "$output" && "$output" == /* ]] || exit 8\n' + 'mkdir -p "$output/books/selected/book"\n' + ': > "$output/index.html"\n' + ': > "$output/books/selected/index.html"\n' + ': > "$output/books/selected/book/index.html"\n', + encoding="utf-8", + ) + fake_elan.chmod(0o755) + (web / "lakefile.lean").write_text( + 'import Lake\npackage "demo-site" where\n', encoding="utf-8" + ) + (web / "lean-toolchain").write_text( + "leanprover/lean4:v4.30.0\n", encoding="utf-8" + ) generator = repo / "generator.py" generator.write_text( "import json, os\nfrom pathlib import Path\n" @@ -1339,6 +1364,12 @@ def test_verso_project_fragment_writes_validated_disjoint_manifest(self) -> None encoding="utf-8", ) fragments = Path(temp) / "fragments" + pythonpath = os.pathsep.join( + ( + str(ROOT / "sdk" / "common" / "src"), + str(ROOT / "sdk" / "verso" / "src"), + ) + ) result = subprocess.run( ["bash", str(scripts / "verso.sh")], @@ -1350,6 +1381,10 @@ def test_verso_project_fragment_writes_validated_disjoint_manifest(self) -> None "REASBOOK_INCLUDE_PROJECTS": "books/Selected", "REASBOOK_PROJECT_FRAGMENT_ROOT": str(fragments), "REASBOOK_VERSO_GENERATOR": str(generator), + "REASBOOK_TEST_PYTHON": sys.executable, + "VERSO_ELAN_BIN": str(fake_elan), + "VERSO_EXECUTABLE_ARGV": str(executable_argv), + "PYTHONPATH": pythonpath, }, capture_output=True, text=True, @@ -1366,6 +1401,11 @@ def test_verso_project_fragment_writes_validated_disjoint_manifest(self) -> None self.assertTrue( (root / "site" / "books" / "selected" / "index.html").is_file() ) + arguments = executable_argv.read_text(encoding="utf-8").splitlines() + self.assertEqual(arguments.count("--output"), 1) + output_option = arguments.index("--output") + self.assertEqual(arguments[output_option + 1], str(root / "site")) + self.assertFalse((web / "_site").exists()) def test_pages_assembly_normalizes_docs_and_generates_landing_page(self) -> None: project = {