Skip to content

developer_guide.md

Latest commit

 

History

History
74 lines (55 loc) · 3.11 KB

developer_guide.md

File metadata and controls

74 lines (55 loc) · 3.11 KB
Raw

Developer guide

Toolchain

Pin Location
Python ≥ 3.11 pyproject.toml + committed uv.lock (uv sync --frozen --all-extras)
Lean 4 stable v4.32.1 lean-toolchain (checkout) and src/leanverifier/resources/lean-project/lean-toolchain (wheel)
mathlib v4.32.1 lakefile.toml + committed lake-manifest.json

Never use Lean RC toolchains on supported branches. Run Lake commands from the repository root for development; installed wheels materialize the packaged Lake project into an isolated cache.

Layout

Path Role
LeanVerifier/ Supported Lean sources (checkout; keep in sync with packaged copy)
LeanVerifier.lean Root import (must not import experimental)
src/leanverifier/ Generator + CLI (src layout; avoids Windows case collision with LeanVerifier/)
src/leanverifier/resources/ Packaged schemas, Lean project, axiom-audit script (importlib.resources)
schemas/ Checkout mirror of packaged JSON schemas (must match resource hashes)
examples/affine_binary/ Canonical worked example
tests/ unit / schema / integration / mutation / security
experimental/ Legacy FormalVerifML — excluded from supported build
scripts/ audits, docs verification, wheel smoke, release scaffolding
docs/ User/developer guides + assurance case

Local checks

lake build
lake lint
uv sync --frozen --all-extras
uv run python scripts/audit_axioms.py
uv run python -m pytest
uv run ruff check src/leanverifier tests scripts
uv run mypy src/leanverifier
uv run python scripts/verify_docs.py
uv build && uv run python scripts/smoke_wheel.py --dist dist
git status --porcelain   # clean after build when .lake / caches are gitignored

After editing checkout schemas/ or Lean sources that ship in the wheel, refresh packaged copies and digests:

uv run python scripts/regen_resource_hashes.py

Digests are LF-canonical (see .gitattributes). Always regenerate on the machine that edited the files; do not hand-edit hashes.json.

Adding formal content

  1. Keep definitions exact over ℚ; no Array Float, bang indexing, getD, or silent zip truncate.
  2. Prove unit theorems with norm_num where helpful; include repeated-weight examples.
  3. Extend Audit/PublicAxioms.lean and ensure scripts/audit_axioms.py still passes.
  4. Update CLAIMS.md if the public claim surface changes.

Generator constraints

User-controlled values may appear only as rationals, lengths, digests, and comments. Generated modules import only supported LeanVerifier modules. Module names must match GeneratedModel_[0-9a-f]{16}.

CI

.github/workflows/ci.yml is SHA-pinned with permissions: contents: read by default. Do not use pull_request_target or workflow_run for untrusted tests.

RC release scaffolding lives in .github/workflows/release-rc.yml (see release-process.md).

Experimental tree

experimental/legacy-formalverifml/ retains FormalVerifML sources with a WARNING header. It is never a Lake dependency of LeanVerifier and is not installed by the Python package.