From 82800a942085fc91d0e0635908e4d9116e054949 Mon Sep 17 00:00:00 2001 From: Moritz Firsching Date: Fri, 15 May 2026 08:15:37 +0200 Subject: [PATCH 1/4] feat(build-and-docs) quick -webtest branch --- .github/workflows/build-and-docs.yml | 100 +++++++++++++++++++++++++-- site/dev.sh | 85 +++++++++++++++++++++++ 2 files changed, 180 insertions(+), 5 deletions(-) create mode 100755 site/dev.sh diff --git a/.github/workflows/build-and-docs.yml b/.github/workflows/build-and-docs.yml index 9cb2261818..4797de1d33 100644 --- a/.github/workflows/build-and-docs.yml +++ b/.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,7 +44,23 @@ 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 @@ -45,6 +68,7 @@ jobs: 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 }} diff --git a/site/dev.sh b/site/dev.sh new file mode 100755 index 0000000000..cd90b0800d --- /dev/null +++ b/site/dev.sh @@ -0,0 +1,85 @@ +#!/usr/bin/env bash +# dev.sh — Quick local website development. +# +# Downloads the conjectures data from the live production site and builds the +# website locally, without needing to compile any Lean code. +# +# Requirements: Python 3, Node.js (or install via: conda install -c conda-forge nodejs) +# +# Usage: +# ./dev.sh # build and serve on port 8080 +# ./dev.sh --build-only # build without serving +# ./dev.sh --port 3000 # serve on a custom port + +set -euo pipefail +cd "$(dirname "$0")" + +LIVE_URL="https://google-deepmind.github.io/formal-conjectures" +PORT=8080 +SERVE=true + +# Parse arguments +while [[ $# -gt 0 ]]; do + case "$1" in + --build-only) SERVE=false; shift ;; + --port) PORT="$2"; shift 2 ;; + *) echo "Unknown option: $1"; echo "Usage: $0 [--build-only] [--port PORT]"; exit 1 ;; + esac +done + +# Check for Node.js +if ! command -v node &>/dev/null; then + echo "Error: Node.js not found." + echo "Install it via one of:" + echo " conda install -c conda-forge nodejs" + echo " sudo apt install nodejs" + echo " https://nodejs.org/" + exit 1 +fi + +echo "==> Downloading data from live site ($LIVE_URL) ..." +mkdir -p data + +curl -sfL "$LIVE_URL/data/conjectures.json" -o /tmp/fc_live_conjectures.json + +# Use Python for JSON conversion (always available) +python3 -c " +import json, sys + +with open('/tmp/fc_live_conjectures.json') as f: + data = json.load(f) + +# Convert processed conjectures back to raw extract_names format +problems = [] +for c in data.get('conjectures', []): + subjects = c.get('subjects', []) + problems.append({ + 'theorem': c['theorem'], + 'module': c['module'], + 'category': c['category'], + 'subjects': [s['code'] if isinstance(s, dict) else s for s in subjects], + 'formalProofKind': c.get('formalProofKind'), + 'formalProofLink': c.get('formalProofLink'), + 'hasSorryFreeProof': False, + }) + +with open('data/conjectures.json', 'w') as f: + json.dump({'problems': problems}, f) + +# Extract Verso fragments if present +if 'versoFragments' in data: + with open('data/verso-fragments.json', 'w') as f: + json.dump(data['versoFragments'], f) + +print(f' {len(problems)} conjectures converted.') +" + +echo "==> Building website ..." +node build.js + +echo "==> Done. Output in site/" + +if [[ "$SERVE" == "true" ]]; then + echo "==> Serving at http://localhost:${PORT} (Ctrl+C to stop)" + python3 -m http.server "$PORT" --directory site +fi From fdb404e9b9690b93d616cf4acac7bad00a7cffb4 Mon Sep 17 00:00:00 2001 From: Moritz Firsching Date: Fri, 15 May 2026 10:51:22 +0200 Subject: [PATCH 2/4] explain how it works in README --- site/README.md | 117 +++++++++++++++++++++++++++++++++---------------- 1 file changed, 80 insertions(+), 37 deletions(-) diff --git a/site/README.md b/site/README.md index 30824acce8..705f92e6cc 100644 --- a/site/README.md +++ b/site/README.md @@ -72,60 +72,103 @@ 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//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 +mkdir -p site/data +lake exe extract_names --exclude=statement,docstring,moduleDocstrings > site/data/conjectures.json -# 3. Build the site +# 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 my-feature-webtest ``` -Valid values for `category`: `"research open"`, `"research solved"`, `"research formally solved"`, `"textbook"`, `"test"`, `"API"`. +Your site will be live at `https://.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**. +To enable GitHub Pages, go to **Settings → Pages** and set the source to **GitHub Actions**. From 1ee9b2874fe5bd50ed05a4086e7a5b4e3bb6b30d Mon Sep 17 00:00:00 2001 From: Moritz Firsching Date: Fri, 15 May 2026 10:56:06 +0200 Subject: [PATCH 3/4] avoid duplicate explanations --- site/README.md | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/site/README.md b/site/README.md index 705f92e6cc..2ebdae9c45 100644 --- a/site/README.md +++ b/site/README.md @@ -171,4 +171,4 @@ The GitHub Actions workflow in `.github/workflows/build-and-docs.yml` triggers o **Deployment** happens on pushes to `main`, and on `*-webtest` branches when on a fork. -To enable GitHub Pages, 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. From 4a9ae5ef4eb97731709f214aad76aafea2cfbfd1 Mon Sep 17 00:00:00 2001 From: Moritz Firsching Date: Fri, 15 May 2026 11:02:40 +0200 Subject: [PATCH 4/4] also mention verso fragments --- site/README.md | 11 +++++++++++ 1 file changed, 11 insertions(+) diff --git a/site/README.md b/site/README.md index 2ebdae9c45..6311f5cc62 100644 --- a/site/README.md +++ b/site/README.md @@ -102,6 +102,17 @@ lake build 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/