Skip to content

quickstart.md

Latest commit

 

History

History
60 lines (42 loc) · 1.58 KB

quickstart.md

File metadata and controls

60 lines (42 loc) · 1.58 KB
Raw

Quickstart

1. Fresh Clone

git clone https://github.com/heathsanchez/mathgraph.git
cd mathgraph

2. Quick Release Check

python scripts/run_release_check.py --quick

3. Public Demo, Advisory Mode

python scripts/run_public_demo.py --out-dir demo_out

4. Public Demo, Live Verifier If Lean Is Available

python scripts/run_public_demo.py \
  --allow-execution \
  --allow-missing-verifier \
  --accept-verified-entries-in-memory \
  --out-dir demo_out

5. Colab / Local Test Drive

python scripts/run_colab_testdrive.py --use-current-checkout --quick-smoke

Optional: Curated Local Mathlib Demo

python scripts/run_real_mathlib_demo.py --ensure-examples
python scripts/run_real_mathlib_demo.py --config examples/real_mathlib_demo/curated_real_mathlib_demo_config.example.json --project-root /path/to/local/mathlib

The command is local-path-only and skips cleanly when no project path is available.

Optional selected-module verification:

python scripts/run_mathlib_module_verification.py --use-synthetic-request --project-root examples/mathlib_micro_subset
python scripts/run_real_mathlib_demo.py --project-root /path/to/mathlib4 --run-module-verification --execution-mode lake-env-lean --allow-execution --allow-missing-verifier

Use lake env lean mode for real Mathlib/Lake projects. Raw Lean mode is mainly for synthetic or simple projects.

6. Boundary Reminder

CLI success is not proof. Demo success is not proof. Only verifier, trusted importer, finite validator, or chain audit evidence promotes truth.