From 288f8c28bbdbdfb701ef2256fba6e19e5380795e Mon Sep 17 00:00:00 2001 From: zixiaowang17 Date: Thu, 1 Oct 2026 16:06:20 -0400 Subject: [PATCH] docs: explain the design-first contribution workflow --- README.md | 97 ++++++++++++++++++++++++++++++++++++++++++++++- roadmap/README.md | 10 +++-- 2 files changed, 103 insertions(+), 4 deletions(-) diff --git a/README.md b/README.md index 2d2a02a..37d58e0 100644 --- a/README.md +++ b/README.md @@ -1,3 +1,98 @@ # Statlib -Lean formalization project for probability and statistics. +[![Build and lint](https://github.com/stat-lib/statlib/actions/workflows/ci.yml/badge.svg)](https://github.com/stat-lib/statlib/actions/workflows/ci.yml) +[![Apache 2.0](https://img.shields.io/badge/license-Apache--2.0-blue.svg)](LICENSE) + +Statlib is a community-developed Lean 4 library for mathematical statistics. It builds on +[Mathlib](https://github.com/leanprover-community/mathlib4) to develop reusable statistical +definitions, theorems, and research infrastructure. + +Statlib is research-driven: its mathematical scope and APIs are developed jointly by statisticians +and Lean contributors. The project is under active development. + +[Website](https://stat-lib.github.io/) · +[Tutorial](https://stat-lib.github.io/tutorial/) · +[API documentation](https://stat-lib.github.io/docs/) · +[Roadmap](https://stat-lib.github.io/roadmap.html) · +[Contributing guide](https://stat-lib.github.io/contribute.html) · +[Zulip](https://leanprover.zulipchat.com/#narrow/channel/611809-Statlib) + +## Design before code + +A coherent library is more than a collection of independently formalized results. Definitions and +theorem statements establish vocabulary and conventions that later code will depend on. Choices +such as names, namespaces, representations, parameter order, typeclass assumptions, and boundary +behavior are expensive to change once a large API has been built around them. + +For a substantial new formalization or API, our workflow is: + +1. **Open an issue.** Describe the mathematical source, intended scope, central definitions and + results, and the parts of Mathlib or Statlib that the work should build on. +2. **Discuss the design specification in the issue.** Contributors should reach a shared direction + for the mathematical representation, level of generality, naming and code conventions, file + organization, and compatibility with Mathlib. +3. **Implement after the design direction is clear.** If implementation reveals that a design + choice should change, bring that decision back to the issue. The discussion remains the public + record and gives reviewers context for the resulting code. +4. **Open a pull request linked to the issue.** Keep the change reviewable and explain any departure + from the agreed design. + +This discussion is especially important before manually writing or generating a large amount of +code. Early agreement prevents incompatible parallel APIs, avoids locking in accidental naming or +representation choices, and makes later review and maintenance substantially easier. + +The proposed [design document template](roadmap/README.md) is a reference checklist, not a required +form. Use the sections that help clarify the project; the design discussion itself happens in the +GitHub issue. + +Small fixes, documentation improvements, and narrowly scoped lemmas do not need a full design +document. When in doubt, open an issue or ask in the +[Statlib Zulip channel](https://leanprover.zulipchat.com/#narrow/channel/611809-Statlib). + +## Current areas + +The library currently includes work on: + +- causal inference and potential responses; +- contiguity and local asymptotic theory; +- E-values and E-variables; +- quadratic mean differentiability and statistical inference; +- supporting measure-theoretic results intended for eventual contribution to Mathlib. + +See the [API documentation](https://stat-lib.github.io/docs/) for the current module tree and the +[roadmap](https://stat-lib.github.io/roadmap.html) for longer-term directions. + +## Build Statlib + +Install Lean using [elan](https://lean-lang.org/install/), then clone and build the repository: + +```sh +git clone https://github.com/stat-lib/statlib.git +cd statlib +lake exe cache get +lake build +``` + +A Lean file can import the whole library or an individual module: + +```lean +import Statlib +import Statlib.Contiguity.Def +``` + +## Contributing + +To propose a substantial project, start with a +[GitHub issue](https://github.com/stat-lib/statlib/issues/new/choose) and discuss its design before +opening a large code contribution. For pull-request expectations, the relationship with Mathlib, +and the project's policy on AI-assisted code, read the +[contributing guide](https://stat-lib.github.io/contribute.html). + +Statlib follows the +[Mathlib style guide](https://leanprover-community.github.io/contribute/style.html) by default. +Contributors are responsible for understanding, explaining, and maintaining every line they submit, +regardless of which tools were used to produce it. + +## License + +Statlib is released under the [Apache License 2.0](LICENSE). diff --git a/roadmap/README.md b/roadmap/README.md index 65af253..ac11846 100644 --- a/roadmap/README.md +++ b/roadmap/README.md @@ -1,7 +1,10 @@ -Proposed roadmap structure: +# Proposed design document template +This is a reference checklist, not a required format. Use the sections that are helpful for the +project you want to propose, and discuss the design itself in a GitHub issue before beginning a +large implementation. -# Roadmap: topic +# Project: topic ## 1. Goal What is your goal? Why is it important? @@ -38,4 +41,5 @@ Project/Area/Basic.lean Project/Area/Operations.lean Project/Area/MainTheorem.lean ``` -Any comments are welcome! This is just a proposed design doc — the goal is to reduce communication overhead and serve as a reference for anyone joining the project later. +The goal is to make important design choices explicit, reduce communication overhead, and leave a +useful record for contributors who join the project later.