From 2cc5b57f756f2f9dd51dde85f1456fa8a60ac186 Mon Sep 17 00:00:00 2001 From: Asher Yan Date: Wed, 22 Jul 2026 02:22:27 -0400 Subject: [PATCH 1/4] ci: reuse production build for Blueprint --- .github/workflows/ci.yml | 36 +++++++++++++++++------------- AGENTS.md | 6 +++++ README.md | 6 +++-- blueprint-verso/lake-manifest.json | 2 +- blueprint-verso/lakefile.lean | 1 + blueprint-verso/scripts/site.sh | 6 +++-- 6 files changed, 37 insertions(+), 20 deletions(-) diff --git a/.github/workflows/ci.yml b/.github/workflows/ci.yml index 29838a1..5c584f1 100644 --- a/.github/workflows/ci.yml +++ b/.github/workflows/ci.yml @@ -2,9 +2,15 @@ name: CI on: push: + branches: + - main pull_request: workflow_dispatch: +concurrency: + group: ci-${{ github.workflow }}-${{ github.event.pull_request.number || github.ref }} + cancel-in-progress: true + permissions: contents: read @@ -41,21 +47,21 @@ jobs: uses: actions/cache@v4 with: path: | - blueprint-verso/.lake/packages/Cli/.lake/build - blueprint-verso/.lake/packages/LeanSearchClient/.lake/build - blueprint-verso/.lake/packages/MD4Lean/.lake/build - blueprint-verso/.lake/packages/Qq/.lake/build - blueprint-verso/.lake/packages/VersoBlueprint/.lake/build - blueprint-verso/.lake/packages/aesop/.lake/build - blueprint-verso/.lake/packages/batteries/.lake/build - blueprint-verso/.lake/packages/checkdecls/.lake/build - blueprint-verso/.lake/packages/illuminate/.lake/build - blueprint-verso/.lake/packages/importGraph/.lake/build - blueprint-verso/.lake/packages/plausible/.lake/build - blueprint-verso/.lake/packages/proofwidgets/.lake/build - blueprint-verso/.lake/packages/subverso/.lake/build - blueprint-verso/.lake/packages/verso/.lake/build - blueprint-verso/.lake/packages/verso-slides/.lake/build + .lake/packages/Cli/.lake/build + .lake/packages/LeanSearchClient/.lake/build + .lake/packages/MD4Lean/.lake/build + .lake/packages/Qq/.lake/build + .lake/packages/VersoBlueprint/.lake/build + .lake/packages/aesop/.lake/build + .lake/packages/batteries/.lake/build + .lake/packages/checkdecls/.lake/build + .lake/packages/illuminate/.lake/build + .lake/packages/importGraph/.lake/build + .lake/packages/plausible/.lake/build + .lake/packages/proofwidgets/.lake/build + .lake/packages/subverso/.lake/build + .lake/packages/verso/.lake/build + .lake/packages/verso-slides/.lake/build key: probability-blueprint-deps-${{ runner.os }}-${{ runner.arch }}-${{ hashFiles('blueprint-verso/lean-toolchain', 'blueprint-verso/lake-manifest.json') }} - name: Restore Blueprint project build cache uses: actions/cache@v4 diff --git a/AGENTS.md b/AGENTS.md index c8d719f..252e193 100644 --- a/AGENTS.md +++ b/AGENTS.md @@ -173,12 +173,18 @@ cd blueprint-verso During Blueprint editing, build the statement module before rendering the site: ```bash +lake --wfail build ProbabilityApproximation cd blueprint-verso lake build +ProbabilityApproximationBlueprint.NonuniformBerryEsseen lake build +ProbabilityApproximationBlueprint.ConvexSetApproximation lake build +ProbabilityApproximationBlueprint.References ``` +The Blueprint package shares the root `.lake/packages` directory. Its site driver checks +`@ProbabilityApproximation/ProbabilityApproximation` with `lake --no-build` before compiling the +documentation modules; missing or stale production artifacts are an error rather than an implicit +second library build. + `site.sh build release` runs the statement-style check, Blueprint library build, HTML render, strict manifest validator, `vbp check`, and PDF render. The release profile is the default and removes fidelity tags from reader-facing HTML while retaining them in the validated manifest; diff --git a/README.md b/README.md index 772abc5..106a822 100644 --- a/README.md +++ b/README.md @@ -118,8 +118,10 @@ mathematical text with complete statements, source citations, Lean declarations, graphs. The same text is available as a [downloadable PDF](https://probability.polarnova.site/berry-esseen-bounds.pdf). -Use `./scripts/site.sh serve dev` inside `blueprint-verso` to retain fidelity metadata during local -review. Public builds use the default `release` profile and omit those tags from the reading view. +Build `ProbabilityApproximation` at the repository root, then use `./scripts/site.sh serve dev` +inside `blueprint-verso` to retain fidelity metadata during local review. The Blueprint workspace +shares the root dependencies and refuses to rebuild a missing or stale production library. Public +builds use the default `release` profile and omit fidelity tags from the reading view. ## Contributing diff --git a/blueprint-verso/lake-manifest.json b/blueprint-verso/lake-manifest.json index d6a72a0..7bf8ea0 100644 --- a/blueprint-verso/lake-manifest.json +++ b/blueprint-verso/lake-manifest.json @@ -1,5 +1,5 @@ {"version": "1.2.0", - "packagesDir": ".lake/packages", + "packagesDir": "../.lake/packages", "packages": [{"type": "path", "scope": "", diff --git a/blueprint-verso/lakefile.lean b/blueprint-verso/lakefile.lean index d8662f8..bb83135 100644 --- a/blueprint-verso/lakefile.lean +++ b/blueprint-verso/lakefile.lean @@ -11,6 +11,7 @@ require VersoBlueprint from git "https://github.com/leanprover/verso-blueprint" require ProbabilityApproximation from ".." package ProbabilityApproximationBlueprint where + packagesDir := "../.lake/packages" precompileModules := false leanOptions := #[⟨`experimental.module, true⟩] diff --git a/blueprint-verso/scripts/site.sh b/blueprint-verso/scripts/site.sh index 27a6224..4ca3055 100755 --- a/blueprint-verso/scripts/site.sh +++ b/blueprint-verso/scripts/site.sh @@ -30,8 +30,10 @@ fi build_library() { cd "$root" python3 "$root/scripts/check_statement_style.py" - echo "Checking compiled Blueprint modules with Lake..." - "$lake_cmd" build ProbabilityApproximationBlueprint + echo "Reusing the checked production-library artifacts..." + "$lake_cmd" --no-build build @ProbabilityApproximation/ProbabilityApproximation + echo "Building the Blueprint modules..." + "$lake_cmd" build @/ProbabilityApproximationBlueprint } validate_site() { From d61be46dad00a77b7144171f3b1fdee35ab6fb5e Mon Sep 17 00:00:00 2001 From: Asher Yan Date: Wed, 22 Jul 2026 02:29:19 -0400 Subject: [PATCH 2/4] build: initialize Blueprint stamp directory --- blueprint-verso/lakefile.lean | 1 + 1 file changed, 1 insertion(+) diff --git a/blueprint-verso/lakefile.lean b/blueprint-verso/lakefile.lean index bb83135..51d38e6 100644 --- a/blueprint-verso/lakefile.lean +++ b/blueprint-verso/lakefile.lean @@ -22,6 +22,7 @@ input_file referencesBib where target referencesBibStamp pkg : System.FilePath := do let bibliography ← referencesBib.fetch let stamp := pkg.buildDir / "references.bib.stamp" + IO.FS.createDirAll pkg.buildDir buildFileAfterDep (text := true) stamp bibliography fun bibliographyPath => do let sourcesOlean := pkg.buildDir / "lib" / "lean" / From 721a3da149be23c2789d3b404e19b44ca04de46e Mon Sep 17 00:00:00 2001 From: Asher Yan Date: Wed, 22 Jul 2026 02:36:46 -0400 Subject: [PATCH 3/4] fix: resolve shared Blueprint package paths --- blueprint-verso/scripts/site.sh | 4 +++- 1 file changed, 3 insertions(+), 1 deletion(-) diff --git a/blueprint-verso/scripts/site.sh b/blueprint-verso/scripts/site.sh index 4ca3055..5d7ab78 100755 --- a/blueprint-verso/scripts/site.sh +++ b/blueprint-verso/scripts/site.sh @@ -3,6 +3,8 @@ set -euo pipefail root="$(cd "$(dirname "${BASH_SOURCE[0]}")/.." && pwd)" +packages_dir="$(jq -er '.packagesDir // ".lake/packages"' "$root/lake-manifest.json")" +packages_root="$(cd "$root/$packages_dir" && pwd)" output="$root/_out/site" book_output="$root/_out/book" profile="${2:-release}" @@ -49,7 +51,7 @@ build_site() { rm -rf -- "$output/html-multi" export PROBABILITY_APPROXIMATION_SOURCE_REVISION="${GITHUB_SHA:-$(git -C "$root/.." rev-parse HEAD)}" export MATHLIB_SOURCE_REVISION="$( - git -C "$root/.lake/packages/mathlib" rev-parse HEAD + git -C "$packages_root/mathlib" rev-parse HEAD )" "$lake_cmd" lean ProbabilityApproximationBlueprintMain.lean -- --run \ ProbabilityApproximationBlueprintMain.lean --output "$output" From bfc9416b5e7d5bdf573156d9bcda35d1077921f2 Mon Sep 17 00:00:00 2001 From: Asher Yan Date: Wed, 22 Jul 2026 02:44:37 -0400 Subject: [PATCH 4/4] docs: keep full builds in GitHub Actions --- AGENTS.md | 15 +++++++-------- README.md | 20 +++++++++++--------- 2 files changed, 18 insertions(+), 17 deletions(-) diff --git a/AGENTS.md b/AGENTS.md index 252e193..83e7577 100644 --- a/AGENTS.md +++ b/AGENTS.md @@ -159,21 +159,19 @@ lake update lake exe cache get ``` -During proof work, build the narrowest affected production module. Before handoff, run from the -repository root: +During proof work, build only the narrowest affected production module. Before handoff, run the +lightweight source audits locally and use the pull request's GitHub Actions result as the required +full-library, Blueprint, and PDF validation: ```bash -lake --wfail build ProbabilityApproximation ./.github/scripts/forbidden_tokens.sh ./.github/scripts/audit_axioms.sh -cd blueprint-verso -./scripts/site.sh build ``` -During Blueprint editing, build the statement module before rendering the site: +During Blueprint editing, a narrow statement-module build is optional local feedback after the +root production artifacts are current: ```bash -lake --wfail build ProbabilityApproximation cd blueprint-verso lake build +ProbabilityApproximationBlueprint.NonuniformBerryEsseen lake build +ProbabilityApproximationBlueprint.ConvexSetApproximation @@ -183,7 +181,8 @@ lake build +ProbabilityApproximationBlueprint.References The Blueprint package shares the root `.lake/packages` directory. Its site driver checks `@ProbabilityApproximation/ProbabilityApproximation` with `lake --no-build` before compiling the documentation modules; missing or stale production artifacts are an error rather than an implicit -second library build. +second library build. Resource-constrained local work must consume release caches where available; +full production, Blueprint, and publication builds belong in GitHub Actions. `site.sh build release` runs the statement-style check, Blueprint library build, HTML render, strict manifest validator, `vbp check`, and PDF render. The release profile is the default and diff --git a/README.md b/README.md index 106a822..5fc4f65 100644 --- a/README.md +++ b/README.md @@ -82,12 +82,12 @@ Then update and build: ```bash lake update lake exe cache get -lake build +lake build @ProbabilityApproximation:release ``` -Lake automatically downloads the matching precompiled ProbabilityApproximation release archive on -Linux x86-64 and macOS arm64. If an archive is unavailable for a platform, Lake falls back to the -same tagged source and builds it locally. +The explicit release target downloads the matching precompiled ProbabilityApproximation archive on +Linux x86-64 and macOS arm64 and fails if that verified platform asset is unavailable; it does not +silently replace the download with a local source build. Import all public declarations with: @@ -102,13 +102,14 @@ The principal declarations are: #check ProbabilityTheory.exists_bentkus_convex_set_constant ``` -To build the repository itself: +Full repository, Blueprint, and PDF builds run in GitHub Actions. For local proof development, +fetch Mathlib's cache and build only the affected production module, for example: ```bash git clone https://github.com/Polarnova/ProbabilityApproximation.git cd ProbabilityApproximation lake exe cache get -lake build ProbabilityApproximation +lake build ProbabilityApproximation.BerryEsseen ``` ## Blueprint @@ -118,10 +119,11 @@ mathematical text with complete statements, source citations, Lean declarations, graphs. The same text is available as a [downloadable PDF](https://probability.polarnova.site/berry-esseen-bounds.pdf). -Build `ProbabilityApproximation` at the repository root, then use `./scripts/site.sh serve dev` -inside `blueprint-verso` to retain fidelity metadata during local review. The Blueprint workspace +After the root production artifacts are current, `./scripts/site.sh serve dev` inside +`blueprint-verso` retains fidelity metadata for optional local review. The Blueprint workspace shares the root dependencies and refuses to rebuild a missing or stale production library. Public -builds use the default `release` profile and omit fidelity tags from the reading view. +builds run in GitHub Actions with the default `release` profile and omit fidelity tags from the +reading view. ## Contributing