[M1-4] Add docs/STYLE.md#287
Merged
Merged
Conversation
4 tasks
Adds a first draft of docs/STYLE.md documenting the conventions agda-algebras currently follows, with explicit flags for the axes where style decisions remain open (naming conventions, notation table, universe-level variable scope). The style guide is deliberately short at this stage. Applying and refining it across Setoid/ and Classical/ is tracked in M4-1, and the document will grow as specific decisions are settled. A premature full-length style guide would codify decisions that are properly made during the M4 sweep. Addresses #253 (M1-4).
williamdemeo
force-pushed
the
253-m1-4-project-style-guide
branch
2 times, most recently
from
8a97afb to
f606dd5
Compare
williamdemeo
force-pushed
the
253-m1-4-project-style-guide
branch
from
f606dd5 to
a0d092b
Compare
Replaces the initial stub with a full-length style guide that takes concrete positions on the axes previously flagged as open: + IsX vs is-X predicate naming is settled in favor of IsX (stdlib-compatible, already canonical in Setoid/Homomorphisms/ Basic and Demos/HSP). + Record-vs-Σ guidance: Algebra stays a record; classical structures are Σ-typed with record-typed bundle views for stdlib interop. + The canonical symbol table is populated (projections, levels, algebras, equivalence, orders, set-theoretic, products, interpretation, term algebra). + ∣_∣ / ∥_∥ are announced as deprecated in favor of proj₁ / proj₂; the mechanical migration is scoped to M4-1, with the rationale to land as an ADR under M1-6. Adds five guiding principles (one canonical form per concept, stdlib-compat when possible, proof terms as training data, Cubical portability by construction, document the mathematics) and concrete checklists for opening, reviewing, and auditing PRs. Paths referenced for Classical/, Cubical/, and Legacy/Base/ are forward-looking; a note at the top calls this out. Addresses #253 (M1-4).
williamdemeo
force-pushed
the
253-m1-4-project-style-guide
branch
from
a0d092b to
656abb9
Compare
Contributor
There was a problem hiding this comment.
Pull request overview
This PR turns the style guide draft into a full docs/STYLE_GUIDE.md document and updates existing docs to reference it consistently as the project’s canonical style guide.
Changes:
- Add a comprehensive
docs/STYLE_GUIDE.mdcovering formatting, naming, notation, levels, proof style, and deprecation policy. - Update the roadmap (
docs/GITHUB_PROJECT.md) and contributor-facing docs (README.md,CONTRIBUTING.md) to point todocs/STYLE_GUIDE.md. - Adjust README wording around the HSP reference and add a link reference for
Setoid.Varieties.HSP.
Reviewed changes
Copilot reviewed 4 out of 4 changed files in this pull request and generated 4 comments.
| File | Description |
|---|---|
| docs/STYLE_GUIDE.md | Adds the full project style guide (new file). |
| docs/GITHUB_PROJECT.md | Updates roadmap references from STYLE.md to STYLE_GUIDE.md. |
| README.md | Updates style-guide link + adjusts HSP pointer and adds a link definition. |
| CONTRIBUTING.md | Updates the style-guide reference to docs/STYLE_GUIDE.md. |
💡 Add Copilot custom instructions for smarter, more guided reviews. Learn how to get started.
Co-authored-by: Copilot <175728472+Copilot@users.noreply.github.com>
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
Add this suggestion to a batch that can be applied as a single commit.This suggestion is invalid because no changes were made to the code.Suggestions cannot be applied while the pull request is closed.Suggestions cannot be applied while viewing a subset of changes.Only one suggestion per line can be applied in a batch.Add this suggestion to a batch that can be applied as a single commit.Applying suggestions on deleted lines is not supported.You must change the existing code in this line in order to create a valid suggestion.Outdated suggestions cannot be applied.This suggestion has been applied or marked resolved.Suggestions cannot be applied from pending reviews.Suggestions cannot be applied on multi-line comments.Suggestions cannot be applied while the pull request is queued to merge.Suggestion cannot be applied right now. Please check back later.
Summary
Expands
docs/STYLE_GUIDE.mdfrom the initial stub to a full-length style guide that takes concrete positions on the axes previously flagged as open, and populates the canonical symbol table.Closes #253 (issue M1-4).
Approach
The style guide is opinionated: where the library had parallel conventions, the document picks one and justifies it. In particular:
IsXvsis-Xpredicate naming is settled in favor ofIsX. This matches the Agda stdlib idiom and is already the canonical form inSetoid/Homomorphisms/Basic.agdaandDemos/HSP.lagda. Theis-xhyphen-case form is preserved inLegacy/Base/(unchanged) and deprecated elsewhere during M4-1.Algebratype remains a record (named projections, inhabited many times). Classical algebraic structures are Σ-typed with record-typed "bundle views" for stdlib interop — this is the Signatures / Theories / Structures / Bundles / Small quintuple that M3-1 will formalize in ADR-002.∣_∣/∥_∥are announced as deprecated in favor ofproj₁/proj₂. The mechanical migration is scoped to M4-1 and the rationale will land as an ADR under M1-6. Existing call sites remain valid until the sweep.The document opens with five guiding principles (one canonical form per concept; stdlib-compat when possible; proof terms as training data; Cubical portability by construction; document the mathematics) and closes with three checklists — opening a PR, reviewing a PR, and auditing a module during the M4-1 sweep.
Notes for reviewers
src/Classical/,src/Cubical/,src/Legacy/Base/) do not yet exist in the tree. A note at the top of the file calls this out; the rules apply when those trees land in M2/M3/M5.CONTRIBUTING.md(from [M1-3] Add CONTRIBUTING.md, CHANGELOG.md, CODE_OF_CONDUCT.md #252) andREADME.mdalready link todocs/STYLE.md; those links now resolve to the substantive document.∣_∣/∥_∥deprecation is the single largest syntactic change announced for the 3.0 cycle. Library-wide rewrite is M4-1's scope; this PR only states the intent.CONTRIBUTING.md, and this document is a separate follow-up (the code uses--cubical-compatible --exact-split --safe; the docs currently document a different order).