diff --git a/CONTRIBUTING.md b/CONTRIBUTING.md index 8939907f2..fd1ed05ed 100644 --- a/CONTRIBUTING.md +++ b/CONTRIBUTING.md @@ -24,20 +24,24 @@ existing files in the same area. ### Formalize a paper Most contributions start by picking a paper from a subfield you know -and writing a study file under `Linglib/Phenomena/{Phenomenon}/Studies/{AuthorYear}.lean`. +and writing a study file at `Linglib/Studies/{AuthorYear}.lean` (study +files are flat, named author-year). A study file typically: -- Imports the relevant theory from `Linglib/Theories/`. +- Imports the relevant theory layer (`Linglib/Semantics/`, + `Linglib/Syntax/`, `Linglib/Pragmatics/`, …). - Imports any cross-linguistic data needed from `Linglib/Fragments/`. - Encodes the paper's model — definitions, denotations, constraint ranking, whatever the paper specifies — in Lean syntax. - Proves the predictions the paper claims, using the encoded model. - Cites the paper in the module docstring with `@cite{key}` (add the - BibTeX entry to `blog/data/references.bib` first). + BibTeX entry to `blog/references.bib` first). -Look at any existing file under `Linglib/Phenomena/*/Studies/` for a -template. `Phenomena/Definiteness/Studies/Jenks2018.lean` and -`Phenomena/Implicatures/Studies/` are reasonable starting points. +Look at any existing file under `Linglib/Studies/` for a template — +`Studies/Jenks2018.lean` (definiteness) and +`Studies/FrankGoodman2012PMF.lean` (an RSA implicature model) are +reasonable starting points. Theory-neutral empirical data lives +separately under `Linglib/Phenomena/{Phenomenon}/`. ### Add a Fragment @@ -54,7 +58,7 @@ fragment (e.g. `Fragments/Mayan/Tseltalan.lean`) for the schema. ### Pick something off the wishlist -The [wishlist](https://hawkrobe.github.io/linglib/wishlist/) is a +The [wishlist](https://linglib.io/wishlist/) is a curated list of theorems, papers, languages, and tools we'd love to see formalized — modeled on Lean's [1000+ theorems](https://leanprover-community.github.io/1000.html). @@ -95,9 +99,10 @@ module docstring placed *after* the `import` statements (Lean requires imports to come first). **Citations.** Cite papers with `@cite{key}`; never inline -`Author (Year)`. Add the BibTeX entry to `blog/data/references.bib` -first using `lastname-lastname-year` keys, then regenerate the -rendered bibliography via `python3 blog/scripts/gen_bibliography.py`. +`Author (Year)`. Add the BibTeX entry to `blog/references.bib` first +using `lastname-lastname-year` keys, and validate with +`python3 blog/scripts/gen_bibliography.py --check`. The rendered +bibliography is a build artifact (regenerated in CI) — don't commit it. **Proof style.** Prefer structural tactics (`exact`, `simp only`, `decide`, `omega`, `linarith`) over bare `simp` or `native_decide`. @@ -118,16 +123,16 @@ explicitly). Use `Type*` not `Type 0`. Prefer `Prop` with blanket. Cite the leaf file. Unnecessary imports slow builds and create false dependency edges. -**Changelog.** Bump `CHANGELOG.md` via -`python3 scripts/changelog_add.py` (not direct edits — the file is -large and concurrent edits race). - ## Pull requests - Branch from `main`, push to a fork, open a PR. - One coherent change per PR. Small is good. -- Keep commit messages short (~50–120 chars). -- The CHANGELOG entry tells the longer story (10–30 lines). +- The repo is **squash-merge only**, so the PR title becomes the commit + on `main` — write it in mathlib's `type(scope): subject` form + (lowercase imperative, ≤ 72 chars), e.g. + `feat(Studies): formalize Jenks 2018 definiteness`. +- Put the longer story in the PR description; declare cross-PR + dependencies with a `Depends on #NNNN` line. If you're not sure whether a contribution makes sense, open an issue first to discuss. Substantive feedback on direction is welcome before diff --git a/scripts/changelog_add.py b/scripts/changelog_add.py deleted file mode 100755 index ff61ebcc7..000000000 --- a/scripts/changelog_add.py +++ /dev/null @@ -1,115 +0,0 @@ -#!/usr/bin/env python3 -"""Atomically prepend an entry to CHANGELOG.md's `## [Unreleased]` section. - -CHANGELOG.md is ~34k lines and concurrent Claude sessions racing to -modify it have lost ~3 entries (0.230.575, 0.230.578, 0.230.586) to -read-then-edit collisions. This script narrows the race window to a -single open+truncate+rename cycle guarded by `flock`, and leaves the -file in a consistent state at every instant. - -Usage: - python3 scripts/changelog_add.py < entry.md - cat entry.md | python3 scripts/changelog_add.py - python3 scripts/changelog_add.py < int: - entry = sys.stdin.read().rstrip() - if not entry: - print("error: no entry provided on stdin", file=sys.stderr) - return 1 - if not entry.startswith("### "): - print( - "error: entry must begin with '### ' (markdown H3 heading)", - file=sys.stderr, - ) - return 1 - # Reject only if the marker appears as a standalone heading line — - # a prose mention (e.g., quoted in body text) is fine. - marker_as_heading = "\n" + MARKER + "\n" - if entry.startswith(MARKER + "\n") or marker_as_heading in entry: - print( - f"error: entry must NOT include the '{MARKER}' marker " - "as a heading line (the script preserves it)", - file=sys.stderr, - ) - return 1 - - # Acquire exclusive lock for the duration of read+write+rename. - # Cooperative: only blocks against other invocations of THIS script. - # Direct Edit calls will not honor the lock. - with open(LOCKFILE, "w") as lock: - fcntl.flock(lock.fileno(), fcntl.LOCK_EX) - - content = CHANGELOG.read_text(encoding="utf-8") - - marker_line = MARKER + "\n" - idx = content.find(marker_line) - if idx < 0: - print( - f"error: '{MARKER}' line not found in {CHANGELOG}", - file=sys.stderr, - ) - return 1 - - # Insert position: right after the marker line + the blank line - # that conventionally follows it. - insert_at = idx + len(marker_line) - if insert_at < len(content) and content[insert_at] == "\n": - insert_at += 1 - - new_content = ( - content[:insert_at] - + entry - + "\n\n" - + content[insert_at:] - ) - - # Atomic write: tmpfile in the same directory + rename. - # Same-filesystem rename is atomic on POSIX. - with tempfile.NamedTemporaryFile( - mode="w", - encoding="utf-8", - delete=False, - dir=CHANGELOG.parent, - prefix=".CHANGELOG.tmp.", - ) as tmp: - tmp.write(new_content) - tmp_path = Path(tmp.name) - - tmp_path.replace(CHANGELOG) - - return 0 - - -if __name__ == "__main__": - sys.exit(main())