Contributor guide

Build and Maintain the Site

The site is a generated view of Lean source and reviewed route metadata, not a second proof database.

Build and certify

python3 website/scripts/lean_gate.py
python3 website/scripts/build_site.py
python3 website/scripts/check_site.py

The ignored gate record is valid only for the exact commit and Lean-source digest that passed the canonical ASTIS check.

Private preview

export ASTIS_PREVIEW_USER='reviewer'
export ASTIS_PREVIEW_PASSWORD='generated-outside-git'
python3 website/scripts/ide_server.py --port 8087

Credentials come only from environment variables. Forward the loopback port over SSH before opening a local Cloudflare Quick Tunnel; it is not a production deployment.

Contributing

This page documents site operations. The full contribution route covers mathematical scope, module ownership, source correspondence, Lean acceptance, review, and credit.

Open the contributor guide

Consistency checks

Registry formalizedLocal count equals the Tests baseline (393 at this build).
Every named Lean declaration and module appears in the inventory and search index.
Teaching and milestone metadata may reference only existing declarations.
Internal links and fragments, source links, formulas, Mermaid sources, and assets resolve.
A gate banner can say passed only when evidence matches the current source digest.
Public, clean, published sources use a commit SHA only when ASTIS_PUBLIC_SOURCE_LINKS=1; all other sources use checked local preview anchors.

Deployment

.github/workflows/blueprint-site.yml runs Lean and Tests before producing the Pages artifact. GitHub Pages must be enabled for Actions; a workflow file alone does not make a 404 deployment live.