feat(build-and-docs) quick -webtest branch (#4008)

and a script to quickly build the website locally from the .json that is
served by the current website without running verso

Author: mo271

.github/workflows/build-and-docs.yml

@@ -18,7 +18,14 @@ on:
   push:
     branches:
       - main
+      - '*-webtest'
   pull_request:
+  workflow_dispatch:
+    inputs:
+      website_only:
+        description: 'Skip Lean build and use live site data (for website development)'
+        type: boolean
+        default: false
 
 # Sets permissions of the GITHUB_TOKEN to allow deployment to GitHub Pages
 permissions:
@@ -37,14 +44,31 @@ jobs:
         with:
           fetch-depth: 0
 
+      # Detect whether this is a website-only build (skip slow Lean compilation).
+      # Triggers:
+      #   - Branches ending in -webtest
+      #   - Manual workflow_dispatch with website_only=true
+      - name: Detect build mode
+        id: mode
+        run: |
+          if [[ "${{ inputs.website_only }}" == "true" ]] || \
+             [[ "${{ github.ref_name }}" == *-webtest ]]; then
+            echo "website_only=true" >> "$GITHUB_OUTPUT"
+            echo "::notice::Website-only build: skipping Lean compilation, downloading data from live site."
+          else
+            echo "website_only=false" >> "$GITHUB_OUTPUT"
+          fi
+
       - name: Install elan
+        if: steps.mode.outputs.website_only != 'true'
         run: |
           set -o pipefail
           curl -sSfL https://github.com/leanprover/elan/releases/download/v1.4.2/elan-x86_64-unknown-linux-gnu.tar.gz | tar xz
           ./elan-init -y --default-toolchain none
           echo "$HOME/.elan/bin" >> $GITHUB_PATH
 
       - name: Generate All.lean
+        if: steps.mode.outputs.website_only != 'true'
         run: |
           lake exe mk_all --lib FormalConjectures || true
           # Avoid including Test files from `Util/` to avoid inflating the
@@ -53,6 +77,7 @@ jobs:
           grep -v "FormalConjectures\.Util\." FormalConjectures.lean > FormalConjectures/All.lean
 
       - name: Restore ~/.cache/mathlib
+        if: steps.mode.outputs.website_only != 'true'
         uses: actions/cache/restore@v3
         with:
           path: ~/.cache/mathlib
@@ -62,15 +87,18 @@ jobs:
             oleans-
 
       - name: Get olean cache
+        if: steps.mode.outputs.website_only != 'true'
         run: |
           lake exe cache unpack
           lake exe cache get
 
       - name: Build project
+        if: steps.mode.outputs.website_only != 'true'
         run: |
           lake --wfail build
 
       - name: Build literate source pages
+        if: steps.mode.outputs.website_only != 'true'
         run: |
           cd docbuild
           # Some modules crash verso-literate (e.g. metaprogramming-heavy util files),
@@ -82,27 +110,32 @@ jobs:
           lake exe verso-html .lake/build/literate ../_literate_html || true
 
       - name: Post-process literate HTML
+        if: steps.mode.outputs.website_only != 'true'
         run: |
           python3 site/fix_literate_html.py _literate_html
 
       - name: Pack olean cache
+        if: steps.mode.outputs.website_only != 'true'
         run: |
           lake exe cache pack
           ls ~/.cache/mathlib
 
       - name: Save ~/.cache/mathlib
+        if: steps.mode.outputs.website_only != 'true'
         uses: actions/cache/save@v3
         with:
           path: ~/.cache
           key: oleans-${{ hashFiles('lake-manifest.json') }}-${{ hashFiles('**/*.lean') }}
 
       - name: Prepare documentation
+        if: steps.mode.outputs.website_only != 'true'
         run: |
           cd docbuild
           export MATHLIB_NO_CACHE_ON_UPDATE=1  # avoids "Failed to prune ProofWidgets cloud release: no such file or directory"
           lake update formal_conjectures
 
       - name: Cache documentation
+        if: steps.mode.outputs.website_only != 'true'
         uses: actions/cache@v5
         with:
           path: docbuild/.lake/build/doc
@@ -112,11 +145,13 @@ jobs:
             MathlibDoc-
 
       - name: Build documentation
+        if: steps.mode.outputs.website_only != 'true'
         run: |
           cd docbuild
           lake build FormalConjectures:docs
 
       - name: Extract documentation
+        if: steps.mode.outputs.website_only != 'true'
         run: |
           cd docbuild
           mkdir out
@@ -128,20 +163,24 @@ jobs:
           rsync -a --files-from=out-files.txt --relative .lake/build/doc ./out
 
       - name: Set up Python
+        if: steps.mode.outputs.website_only != 'true'
         uses: actions/setup-python@v6
         with:
           python-version: '3.12.9'
 
       - name: Install Python dependencies
+        if: steps.mode.outputs.website_only != 'true'
         run: |
           python -m pip install --upgrade pip
           pip install pandas==2.2.3 numpy==2.2.3 plotly==5.20.0 beautifulsoup4 lxml
 
       - name: Run plotting script
+        if: steps.mode.outputs.website_only != 'true'
         run: |
           python docbuild/scripts/plot_growth.py
 
       - name: Inject stats into index.html
+        if: steps.mode.outputs.website_only != 'true'
         shell: bash
         run: |
           cd docbuild
@@ -153,14 +192,58 @@ jobs:
           node-version: '18'
 
       - name: Generate conjectures data for website
+        if: steps.mode.outputs.website_only != 'true'
         run: |
           mkdir -p site/data
           lake exe extract_names --exclude=statement,docstring,moduleDocstrings > site/data/conjectures.json || true
 
       - name: Extract Verso fragments for website
+        if: steps.mode.outputs.website_only != 'true'
         run: |
           python3 site/extract_verso_fragments.py _literate_html site/data/verso-fragments.json
 
+      # In website-only mode, download data from the live production site
+      # instead of building it from scratch. The live site serves the processed
+      # format ({ conjectures, versoFragments, ... }), so we convert it back to
+      # the raw extract_names format ({ problems }) that build.js expects.
+      - name: Download live site data
+        if: steps.mode.outputs.website_only == 'true'
+        run: |
+          LIVE_URL="https://google-deepmind.github.io/formal-conjectures"
+          mkdir -p site/data _literate_html docbuild/out
+          echo "Downloading conjectures data from $LIVE_URL ..."
+          curl -sfL "$LIVE_URL/data/conjectures.json" -o /tmp/live_conjectures.json
+          node -e "
+            const fs = require('fs');
+            const data = JSON.parse(fs.readFileSync('/tmp/live_conjectures.json', 'utf8'));
+
+            // Convert processed conjectures back to raw extract_names format
+            const problems = (data.conjectures || []).map(c => ({
+              theorem: c.theorem,
+              module: c.module,
+              category: c.category,
+              subjects: (c.subjects || []).map(s =>
+                typeof s === 'object' ? s.code : s
+              ),
+              formalProofKind: c.formalProofKind || null,
+              formalProofLink: c.formalProofLink || null,
+              hasSorryFreeProof: false,
+            }));
+            fs.writeFileSync(
+              'site/data/conjectures.json',
+              JSON.stringify({ problems })
+            );
+
+            // Extract Verso fragments if present
+            if (data.versoFragments) {
+              fs.writeFileSync(
+                'site/data/verso-fragments.json',
+                JSON.stringify(data.versoFragments)
+              );
+            }
+            console.log('Converted ' + problems.length + ' conjectures to raw format.');
+          "
+
       - name: Build website
         run: |
           cd site
@@ -174,10 +257,14 @@ jobs:
           mkdir -p _deploy
           # Website goes at root
           cp -r site/site/* _deploy/
-          # Lean docs go under /doc
-          cp -r docbuild/out _deploy/doc
-          # Literate source pages go under /src
-          cp -r _literate_html _deploy/src
+          # Lean docs go under /doc (may not exist in website-only mode)
+          if [[ -d docbuild/out ]]; then
+            cp -r docbuild/out _deploy/doc
+          fi
+          # Literate source pages go under /src (may not exist in website-only mode)
+          if [[ -d _literate_html ]] && [[ -n "$(ls -A _literate_html 2>/dev/null)" ]]; then
+            cp -r _literate_html _deploy/src
+          fi
 
       - name: Upload deploy artifact
         id: deployment
@@ -187,7 +274,10 @@ jobs:
 
   # Deployment job
   deploy:
-    if: github.ref == 'refs/heads/main'
+    if: >-
+      github.ref == 'refs/heads/main' ||
+      (github.repository != 'google-deepmind/formal-conjectures' &&
+       endsWith(github.ref_name, '-webtest'))
     environment:
       name: github-pages
       url: ${{ steps.deployment.outputs.page_url }}

site/README.md

@@ -72,60 +72,114 @@ Individual theorem pages are rendered client-side from `data/conjectures.json` 
 
 ## Building locally
 
-**Requirements:** Node.js 18 or later (no npm packages needed).
+The quickest way to develop the website locally is using `dev.sh`, which downloads
+the conjectures data from the live production site (no Lean build needed):
+
+**Requirements:** Node.js 18+ and Python 3.
 
 ```bash
-# 1. Clone this repo
-git clone https://github.com/<org>/formal-conjectures-website
-cd formal-conjectures-website
+# Install Node.js if needed (e.g. via conda)
+conda install -c conda-forge nodejs
+
+# Build and serve
+cd site
+./dev.sh              # build + serve on http://localhost:8080
+./dev.sh --build-only # just build, no server
+./dev.sh --port 3000  # serve on a custom port
+```
+
+To iterate on templates or styles, re-run `./dev.sh --build-only` after each change
+and refresh the browser.
 
-# 2. (Optional) generate conjectures data from the formal-conjectures repo or create a placeholder dataset.
-cd path/to/formal-conjectures
+### Building with fresh data from a local Lean build
+
+If you need the site to reflect local Lean changes (new conjectures, etc.):
+
+```bash
+# In the formal-conjectures repo root
 lake exe cache get   # download prebuilt Mathlib oleans (first time only)
 lake build
-lake exe extract_names > path/to/formal-conjectures-website/data/conjectures.json
-cd path/to/formal-conjectures-website
-
-# 3. Build the site
+mkdir -p site/data
+lake exe extract_names --exclude=statement,docstring,moduleDocstrings > site/data/conjectures.json
+
+# (Optional) Generate Verso literate fragments for rendered docstrings.
+# Without this, theorem detail pages will lack formatted docstrings and source links.
+# Warning: the literate build step can take a long time (30+ minutes).
+cd docbuild
+lake build FormalConjectures:literate || true
+find .lake/build/literate -name "*.json" -empty -delete 2>/dev/null || true
+lake exe verso-html .lake/build/literate ../_literate_html || true
+cd ..
+python3 site/fix_literate_html.py _literate_html
+python3 site/extract_verso_fragments.py _literate_html site/data/verso-fragments.json
+
+# Build the site
+cd site
 node build.js        # output goes to site/
 
-# 4. Serve locally
+# Serve locally
 python3 -m http.server 8080 --directory site
-# then open http://localhost:8080
-
-# Alternative: serve with uv (no Python installation required)
-uv run --no-project python -m http.server 8080 --directory site
 ```
 
-To iterate on templates or styles, re-run `node build.js` after each change and refresh the browser. There is no watch mode, but Node's built-in `--watch` flag works:
+## Developing on a fork (sharing a live preview)
+
+To share a live preview of your website changes with others, you can deploy from
+a **`*-webtest`** branch on your GitHub fork. The CI workflow detects this naming
+convention and **skips the slow Lean build**, downloading data from the live
+production site instead.
+
+### One-time fork setup
+
+1. **Fork** the repository on GitHub.
+
+2. **Enable GitHub Pages:**
+   - Go to your fork's **Settings → Pages**
+   - Set **Source** to **GitHub Actions**
+
+3. **Allow webtest branches to deploy:**
+   - Go to **Settings → Environments → `github-pages`**
+   - Under **Deployment branches and tags**, click **Add deployment branch or tag rule**
+   - Add the pattern **`*-webtest`**
+   - Save
+
+### Development workflow
 
 ```bash
-node --watch build.js
-```
+# Create a webtest branch from main
+git checkout -b my-feature-webtest origin/main
 
-## Using a placeholder dataset for UI development
-
-If you don't have the formal-conjectures repo built locally, you can populate `data/conjectures.json` with a small synthetic dataset for UI testing. The expected JSON format is an array of objects:
-
-```json
-[
-  {
-    "theorem": "FormalConjectures.ErdosProblems.1.erdos_1",
-    "module": "FormalConjectures.ErdosProblems.1",
-    "category": "research open",
-    "subjects": ["5", "11"],
-    "statement": "∃ C > (0 : ℝ), ∀ (N : ℕ) ...",
-    "docstring": "Erdős Problem 1: ...",
-    "formalProofKind": null,
-    "formalProofLink": null
-  }
-]
+# Make your website changes (CSS, JS, templates, etc.)
+# ...
+
+# Push to your fork — CI builds and deploys automatically
+git push <your-fork> my-feature-webtest
 ```
 
-Valid values for `category`: `"research open"`, `"research solved"`, `"research formally solved"`, `"textbook"`, `"test"`, `"API"`.
+Your site will be live at `https://<username>.github.io/formal-conjectures/`
+once the Action completes (typically ~2 minutes for a website-only build).
+
+> **Note:** The naming convention `*-webtest` is what triggers the fast
+> website-only build. Branches without this suffix run the full Lean build.
+
+> **Note:** GitHub Pages serves one deployment at a time per repo. Deploying
+> from a webtest branch replaces what was deployed from `main`. This is fine
+> for a fork used for previewing.
+
+
 
 ## CI / deployment
 
-The GitHub Actions workflow in `.github/workflows/deploy.yml` triggers on any push to `main` that touches `data/conjectures.json`, `src/`, `build.js`, or `package.json`. It runs `node build.js` and deploys the `site/` directory to GitHub Pages using the standard `actions/upload-pages-artifact` + `actions/deploy-pages` actions.
+The GitHub Actions workflow in `.github/workflows/build-and-docs.yml` triggers on pushes to `main` and `*-webtest` branches, as well as on pull requests.
+
+**Build modes:**
+
+| Condition | Build mode | What happens |
+|-----------|-----------|--------------|
+| Push to `main` on upstream | Full build | Lean compilation + docs + website |
+| Push to `*-webtest` branch | Website-only | Downloads live data, builds website only (~2 min) |
+| Manual `workflow_dispatch` with `website_only=true` | Website-only | Same as above |
+| Pull request | Full build | Lean compilation + docs + website (no deploy) |
+
+**Deployment** happens on pushes to `main`, and on `*-webtest` branches when on a fork.
 
-To enable GitHub Pages for this repo, go to **Settings → Pages** and set the source to **GitHub Actions**.
+For GitHub Pages setup (including the environment rule needed for `*-webtest` branches), see [One-time fork setup](#one-time-fork-setup) above.