ci: reuse production build for Blueprint

.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

AGENTS.md

@@ -159,18 +159,17 @@ 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
 cd blueprint-verso
@@ -179,6 +178,12 @@ 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. 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
 removes fidelity tags from reader-facing HTML while retaining them in the validated manifest;

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,8 +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).
 
-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.
+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 run in GitHub Actions with the default `release` profile and omit fidelity tags from the
+reading view.
 
 ## Contributing
 

blueprint-verso/lake-manifest.json

@@ -1,5 +1,5 @@
 {"version": "1.2.0",
- "packagesDir": ".lake/packages",
+ "packagesDir": "../.lake/packages",
  "packages":
  [{"type": "path",
    "scope": "",

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⟩]
 
@@ -21,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" /

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}"
@@ -30,8 +32,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() {
@@ -47,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"