diff --git a/.githooks/pre-push b/.githooks/pre-push new file mode 100755 index 0000000..e8d4068 --- /dev/null +++ b/.githooks/pre-push @@ -0,0 +1,6 @@ +#!/usr/bin/env bash +# Pre-push hook: runs the same lint.sh that CI runs. +# Blocks push if any check fails. + +echo "Running pre-push lint check..." +bash "$(git rev-parse --show-toplevel)/scripts/lint.sh" diff --git a/CONTRIBUTING.md b/CONTRIBUTING.md index 61c02e8..608a2dc 100644 --- a/CONTRIBUTING.md +++ b/CONTRIBUTING.md @@ -1,137 +1,48 @@ # Contributing to ProofAtlas -## Using ProofAtlas in your own Lean 4 project +## Setup -Add to your `lakefile.toml`: - -```toml -[[require]] -name = "proofatlas" -git = "https://github.com/MathNetwork/ProofAtlas" -rev = "main" -subDir = "lean" +```bash +git clone https://github.com/MathNetwork/ProofAtlas.git +cd ProofAtlas +git config core.hooksPath .githooks +cd lean +lake exe cache get +lake build ``` -Then in any `.lean` file: +The `git config` line enables the pre-push hook, which runs +`scripts/lint.sh` before every push — same checks as CI. -```lean -import ProofAtlas +## Branch strategy -#atlas.graph Nat.add_zero -#atlas.resistance Nat.add_zero Nat.succ_eq_add_one ``` - -`lake update && lake build` and the `#atlas.*` commands work in your -infoview. Your `lean-toolchain` should match the one in -`lean/lean-toolchain` of this repo. - -For a local checkout, use the path form instead: - -```toml -[[require]] -name = "proofatlas" -path = "/absolute/path/to/hypergraph-geo/lean" +main ← production, sorry-free, only accepts PRs from development +development ← research, sorry allowed, accepts PRs from feature branches +feat/xxx ← your work, cut from development ``` -## Exporting geometric reports +1. `git checkout development && git checkout -b feat/your-topic` +2. Write code, commit +3. `git push origin feat/your-topic` +4. Open PR → `development` (not main) +5. CI passes → merge +6. When development has verified work ready for production: PR `development` → `main` + +## Before pushing -For shell pipelines, CI snapshots, or external analysis, dump a -declaration's geometric report as JSON via the `atlas-export` binary: +The pre-push hook runs `bash scripts/lint.sh` automatically. You +can also run it manually: ```bash -lake exe atlas-export Nat.add_zero -lake exe atlas-export Nat.add_zero Nat.add_comm # glued -lake exe atlas-export --out report.json Nat.succ_eq_add_one +bash scripts/lint.sh ``` -Without `--out` the JSON goes to stdout, so it pipes into -anything. The schema matches `Pipeline/Export.lean`'s -`ToJson HypergraphReport`: incidence data, resistance matrix, -δ-hyperbolicity, and root indices (one per input declaration). - -The companion binary `lake exe atlas-export-demos` writes the -landing-page demo set under `site/data/atlas-demos.json`; re-run -it whenever the seed declarations or the pipeline change shape. - -## Architecture Decision Records - -Some choices in the codebase aren't obvious from the diff alone — -e.g. *why* we picked Mathlib's `Digraph` over `Quiver`, or *which* -2-section convention `toSimpleGraph` uses. Those choices live in -`docs/adr/` so they survive a change of maintainer. - -You don't need an ADR for every PR. Write one when your change -involves any of these: - -- **Choosing an external dependency or target type** for a new - public API (e.g. "use type `X` from package `Y` here"). -- **Defining new public-API semantics** where two reasonable - readings exist (e.g. "full 2-section vs input-output 2-section"). -- **Naming or layout conventions** that affect more than one file. -- **Cross-file architectural decisions** (layer boundaries, - spec-vs-instance splits, new directory conventions). - -Bug fixes, refactors that preserve the public API, and single-file -implementations with self-contained reasoning don't need an ADR. - -To add one: copy `docs/adr/template.md` to -`docs/adr/NNNN-your-title.md`, fill it in, link it from the PR. The -template and the trigger list are explained in detail in -[`docs/adr/README.md`](docs/adr/README.md). - -## Where to read next - -- **First-time user?** Run through the - [tutorial](docs/tutorial.md) (5 minutes, end-to-end). -- **Want the big picture?** The - [architecture document](docs/architecture.md) explains the four - layers and what each one owns. -- **Want to add a feature?** Two recipes: - - [How to add a new mapping](docs/how-to/add-a-mapping.md) — - extract a hypergraph from some Lean object. - - [How to add a new metric](docs/how-to/add-a-metric.md) — - register a new `IsHypergraphMetric` instance. -- **Want to track progress?** [STATUS.md](docs/STATUS.md) is the - transparent checklist; [ROADMAP.md](docs/ROADMAP.md) is the - forward direction. - -The short version of "how to add a new metric": - -1. Define your metric in `ProofAtlas/Metric/YourMetric/Basic.lean` -2. Prove `IsHypergraphMetric` in `ProofAtlas/Metric/YourMetric/Instance.lean` -3. Register the metric in `scripts/check_metric_instances.sh` -4. Run `#atlas.status yourMetricDist` — it should show ✓ -5. CI will check automatically - -## Open tasks - -For scoped, beginner-friendly entry points, see the -[good first issue tracker](https://github.com/MathNetwork/ProofAtlas/labels/good%20first%20issue). -Each one is sized for under a day's work and covers documentation, -code, or infrastructure. - -The list below is the longer-horizon work that doesn't yet have a -specific issue. Each task is self-contained — pick one and open a -PR. - -### IsHypergraphMetric instances (discharge `sorry`) -- [ ] `jsDist_isHypergraphMetric` — needs JS triangle inequality (Endres–Schindelin 2003) -- [ ] `diffusionDist_isHypergraphMetric` — needs diffusion metric axioms +## Architecture decisions -### Float compute paths (new) -- [ ] Float commute time in `Pipeline/` — enables `#atlas.commute` -- [ ] Float JS distance in `Pipeline/` — enables `#atlas.jsd` -- [ ] Float eigensolver in `Pipeline/` — enables `#atlas.spectrum` and `#atlas.cluster` +Write an ADR in `docs/adr/` for cross-file architectural changes. +See [`docs/adr/README.md`](docs/adr/README.md). -### Command language (new) -- [ ] `#atlas.commute` — compute commute time distance -- [ ] `#atlas.jsd` — compute JS distance -- [ ] `#atlas.diffusion` — compute diffusion distance at scale `t` -- [ ] `#atlas.spectrum` — spectral decomposition of `L_κ` -- [ ] `#atlas.cluster` — spectral clustering -- [ ] `#atlas.delta.ns!` — Monte-Carlo δ sampler for large namespaces +## License -### Documentation -- [ ] Metrics page: intuition + math + Lean code for each metric -- [ ] Theory page: δ-hyperbolicity, spectral decomposition, Hausdorff, GH -- [ ] How-to: fill an open `sorry` +Apache 2.0 (see `LICENSE`).