diff --git a/.github/ISSUE_TEMPLATE/bug_report.yml b/.github/ISSUE_TEMPLATE/bug_report.yml new file mode 100644 index 00000000..b4b0f20c --- /dev/null +++ b/.github/ISSUE_TEMPLATE/bug_report.yml @@ -0,0 +1,65 @@ +name: Bug report +description: Report something that's broken in agda-algebras. +labels: ["bug"] +body: + - type: markdown + attributes: + value: | + Thanks for taking the time to report a bug. Please fill in the fields below so we can reproduce and diagnose the issue quickly. + + - type: textarea + id: what-happened + attributes: + label: What happened? + description: A clear description of the problem. What did you do? What did you expect? What happened instead? + placeholder: I ran `make check` and got error X on module Y... + validations: + required: true + + - type: textarea + id: reproduction + attributes: + label: Minimal reproduction + description: The smallest Agda snippet or set of commands that reproduces the issue. If the issue is environmental, describe your setup. + render: shell + validations: + required: true + + - type: input + id: agda-version + attributes: + label: Agda version + description: Output of `agda --version`. + placeholder: "Agda version 2.8.0" + validations: + required: true + + - type: input + id: stdlib-version + attributes: + label: Standard-library version + placeholder: "2.3" + validations: + required: true + + - type: input + id: agda-algebras-commit + attributes: + label: agda-algebras commit + description: Output of `git rev-parse --short HEAD`. + placeholder: "e.g. a1b2c3d" + validations: + required: false + + - type: dropdown + id: install-method + attributes: + label: Installation method + options: + - Nix (`nix develop`) + - Agda Python installer + - Prebuilt binary from Agda releases + - Cabal from Hackage + - Other (describe in reproduction section) + validations: + required: true diff --git a/.github/ISSUE_TEMPLATE/config.yml b/.github/ISSUE_TEMPLATE/config.yml new file mode 100644 index 00000000..a6f02cf4 --- /dev/null +++ b/.github/ISSUE_TEMPLATE/config.yml @@ -0,0 +1,5 @@ +blank_issues_enabled: false +contact_links: + - name: Project roadmap + url: https://github.com/ualib/agda-algebras/blob/master/docs/GITHUB_PROJECT.md + about: See the milestone plan to check whether your contribution fits an existing track before filing an issue. diff --git a/.github/ISSUE_TEMPLATE/design_discussion.yml b/.github/ISSUE_TEMPLATE/design_discussion.yml new file mode 100644 index 00000000..41443c6b --- /dev/null +++ b/.github/ISSUE_TEMPLATE/design_discussion.yml @@ -0,0 +1,42 @@ +name: Design discussion +description: Propose or debate a design decision. +labels: ["design-discussion"] +body: + - type: markdown + attributes: + value: | + Design-discussion issues are for questions that need to be settled before code is written — should X be a record or a Σ-type? Which of two naming conventions should we adopt? Does Y belong in `Setoid/` or `Classical/`? + + For reference, ratified design decisions are recorded in `docs/adr/` (Architecture Decision Records). + + - type: textarea + id: question + attributes: + label: The question + description: What decision needs to be made? + validations: + required: true + + - type: textarea + id: options + attributes: + label: Options under consideration + description: List the options with their tradeoffs. If you have a preferred option, say which and why. + validations: + required: true + + - type: textarea + id: constraints + attributes: + label: Constraints and stakeholders + description: Who is affected by this decision? What downstream code depends on it? Are there backwards-compatibility concerns? + validations: + required: false + + - type: textarea + id: proposal + attributes: + label: Proposed resolution + description: If you have a specific resolution in mind, sketch it here. If you want to leave it open for discussion, that's fine too. + validations: + required: false diff --git a/.github/ISSUE_TEMPLATE/feature_request.yml b/.github/ISSUE_TEMPLATE/feature_request.yml new file mode 100644 index 00000000..96ce48d8 --- /dev/null +++ b/.github/ISSUE_TEMPLATE/feature_request.yml @@ -0,0 +1,58 @@ +name: Feature request +description: Suggest a new definition, theorem, or capability for the library. +labels: ["enhancement"] +body: + - type: markdown + attributes: + value: | + Thanks for suggesting something for agda-algebras. Before you fill this out, please check the project roadmap in [`docs/GITHUB_PROJECT.md`](https://github.com/ualib/agda-algebras/blob/master/docs/GITHUB_PROJECT.md) — the change you're proposing may already be planned. + + - type: textarea + id: what + attributes: + label: What are you proposing? + description: A clear description of the definition, theorem, or capability you'd like to see added. + validations: + required: true + + - type: textarea + id: why + attributes: + label: Why is this useful? + description: What can users do with this that they can't do now? What does it enable downstream? + validations: + required: true + + - type: textarea + id: mathematical-context + attributes: + label: Mathematical context + description: If this is a formalization of existing mathematics, cite the source (textbook and page, or paper and theorem number). If it's novel, say so. + validations: + required: false + + - type: dropdown + id: tree + attributes: + label: Which tree does this belong in? + options: + - "Setoid/ (canonical for 3.0)" + - "Classical/ (planned; specific algebraic theories)" + - "Cubical/ (planned; long-term 4.0 target)" + - "Base/ (legacy; new code not accepted here)" + - "Not sure" + validations: + required: true + + - type: dropdown + id: milestone-fit + attributes: + label: Does this fit an existing milestone? + options: + - "M3 — Classical structures" + - "M6 — FLRP prerequisites" + - "M7 — CSP (finite templates)" + - "M9 — Applications of continuous relations" + - Other / none + validations: + required: false diff --git a/.github/PULL_REQUEST_TEMPLATE.md b/.github/PULL_REQUEST_TEMPLATE.md new file mode 100644 index 00000000..4def08db --- /dev/null +++ b/.github/PULL_REQUEST_TEMPLATE.md @@ -0,0 +1,40 @@ + + +## Summary + + + +## Related issues + +Closes # + + + +## Type of change + +- [ ] Bug fix +- [ ] New definition, theorem, or feature +- [ ] Refactoring / cleanup (no user-facing change) +- [ ] Documentation +- [ ] Infrastructure (CI, Nix, build) +- [ ] Other + +## Checklist + +- [ ] `make check` passes locally under `nix develop`. +- [ ] New public definitions have prose comment blocks. +- [ ] Commits are coherent and have explanatory messages. +- [ ] If this PR touches the `src/` tree, the change is targeted at `Base/`, `Setoid/`, or the shared `Overture/` foundation. +- [ ] If this PR introduces new notation, it doesn't conflict with notation already used elsewhere in the library. + +## Notes for reviewers + + + + diff --git a/CHANGELOG.md b/CHANGELOG.md new file mode 100644 index 00000000..de5cd546 --- /dev/null +++ b/CHANGELOG.md @@ -0,0 +1,52 @@ +# Changelog + +All notable changes to agda-algebras are documented in this file. + +The format follows [Keep a Changelog](https://keepachangelog.com/en/1.1.0/) and this project aspires to [Semantic Versioning](https://semver.org/spec/v2.0.0.html). + +## [Unreleased] — 3.0 development + +The 3.0 release is a major reconstruction of agda-algebras building on the Setoid-based redevelopment that shipped in v2.0.1 (December 2021). Work is organized into milestones tracked in [`docs/GITHUB_PROJECT.md`](docs/GITHUB_PROJECT.md). + +### Added + ++ **Setoid-canonical tree.** `src/Setoid/` is the canonical development tree for 3.0. ++ **Nix flake** at the repo root pinning Agda 2.8.0 and standard-library 2.3, so `nix develop` provides a reproducible development environment. ++ **`INSTALL.md`** as the canonical installation guide. ++ **GitHub Actions CI** (`.github/workflows/ci.yml`) that type-checks the library on every push and pull request. ++ **Community-health files**: `CONTRIBUTING.md`, `CODE_OF_CONDUCT.md`, issue templates, pull-request template. ++ **Dual license**: Apache 2.0 for source code under `src/`, CC BY 4.0 for documentation under `docs/`. + +### Changed + ++ **Agda target**: 2.6.2 → 2.8.0. ++ **Standard library target**: 1.7 → 2.3. ++ **Pragma**: `--without-K` → `--cubical-compatible` across the tree. See `docs/lagda/Overture/Basic.lagda` for the reasoning. ++ **Documentation directory**: `doc/` → `docs/` following modern conventions. ++ **README**: rewritten for the 3.0 line. + +### Deprecated + ++ **`docs/INSTALL_AGDA.md`** superseded by `INSTALL.md`. Retained with a deprecation banner; will be removed in a future release. + +### Removed + +Nothing removed yet in this cycle. + +### Fixed + +Nothing to report. 3.0 is a forward-looking reconstruction rather than a bug-fix release. + +--- + +## [2.0.1] — 2021-12-07 + +Archival release coinciding with the TYPES 2021 submission. This version was the first to use the Setoid-based formulation, reconstructed from the earlier UALib project. Archived on Zenodo: [DOI 10.5281/zenodo.5765793](https://doi.org/10.5281/zenodo.5765793). + +Targets Agda 2.6.2 and standard-library 1.7. + +--- + +## [1.x and earlier] + +The earlier UALib library (GitLab-hosted) and the pre-v2.0.1 agda-algebras work. No per-version changelog was maintained; see the git log and the related papers for details. diff --git a/CODE_OF_CONDUCT.md b/CODE_OF_CONDUCT.md new file mode 100644 index 00000000..47f60ab3 --- /dev/null +++ b/CODE_OF_CONDUCT.md @@ -0,0 +1,71 @@ +# Contributor Covenant Code of Conduct + +## Our Pledge + +We pledge to make our community welcoming, safe, and equitable for all. + +We are committed to fostering an environment that respects and promotes the dignity, rights, and contributions of all individuals, regardless of characteristics including race, ethnicity, national origin, language, sex, gender identity and expression, sexual orientation, disability, neurotype, physical appearance, body size, caste, age, religion, citizenship, migratory status, economic status, ability level, and any other dimension of diversity. + +By embracing these values and committing to our ethical responsibilities, we create an environment that welcomes all people to participate in, contribute to, and benefit from our project. + +## Encouraged Behaviors + +Community members are encouraged to engage in the following behaviors: + ++ Demonstrating empathy and kindness toward other people. ++ Communicating respectfully, welcoming differing viewpoints and experiences. ++ Giving and gracefully accepting constructive feedback. ++ Accepting responsibility for our mistakes, apologizing to those affected, and learning from the experience. ++ Focusing on what is best not just for us as individuals, but for the community as a whole. ++ Using welcoming and inclusive language. + +## Restricted Behaviors + +The following behaviors are unacceptable within our community: + ++ **Engaging in bigotry.** Expressing animosity toward or derogating people based on a social characteristic, as described in the Pledge above, will not be tolerated. ++ **Harassing others.** Harassment includes sustained or willful disruption; stalking; publishing private information without permission; sexual attention or contact without clear consent; trolling, insulting, or derogatory comments; and sustained disruption of community discussion. ++ **Abusing power.** Power includes institutional, social, and informal power. Manipulation, coercion, retaliation, and exploitation of power imbalances are unacceptable. ++ **Endangering others.** Threats, incitement of violence, and doxxing are unacceptable. + +## Reporting an Issue + +If you experience or witness behavior that violates this Code of Conduct, please report it by emailing [williamdemeo at gmail](mailto:williamdemeo@gmail.com). + +Reports will be reviewed by the project maintainers. We will keep reports confidential to the extent possible while still enabling an appropriate response, and we will respond to the reporter within one week. + +If your report concerns a maintainer, you may contact [Jacques Carette](https://www.cas.mcmaster.ca/~carette/) as an alternative. + +## Addressing and Repairing Harm + +Community moderators will determine consequences for violations based on the nature and severity of the violation, using the following guidelines: + +### Correction + +*Community impact*: use of inappropriate language or other behavior deemed unprofessional or unwelcome. +*Consequence*: a private, written warning from the maintainers providing clarity around the nature of the violation and why the behavior was inappropriate. A public apology may be requested. + +### Warning + +*Community impact*: a violation through a single incident or series of actions. +*Consequence*: a warning with consequences for continued behavior. No interaction with the people involved, including unsolicited interaction with those enforcing the Code of Conduct, for a specified period of time. Violating these terms may lead to a temporary or permanent ban. + +### Temporary Ban + +*Community impact*: a serious violation of community standards, including sustained inappropriate behavior. +*Consequence*: a temporary ban from any sort of interaction or public communication with the community for a specified period of time. + +### Permanent Ban + +*Community impact*: demonstrating a pattern of violation of community standards, including sustained inappropriate behavior or harassment of an individual, or aggression toward or disparagement of classes of individuals. +*Consequence*: a permanent ban from any sort of public interaction within the community. + +## Scope + +This Code of Conduct applies within all community spaces (issues, pull requests, discussions, and any related communication channels), and also applies when an individual is officially representing the community in public spaces. + +## Attribution + +This Code of Conduct is adapted from the [Contributor Covenant 3.0](https://www.contributor-covenant.org/version/3/0/code_of_conduct/), authored by the Organization for Ethical Source. + + diff --git a/CONTRIBUTING.md b/CONTRIBUTING.md new file mode 100644 index 00000000..1d10c095 --- /dev/null +++ b/CONTRIBUTING.md @@ -0,0 +1,136 @@ +# Contributing to agda-algebras + +Thank you for your interest in contributing to `agda-algebras`. This document explains how to set up a development environment, the workflow we use, and the conventions that make contributions easier to review and merge. + +The library is currently under active reconstruction for the 3.0 release. Expect some rough edges; please report them via GitHub issues. + +--- + +## Before you start + +`agda-algebras` is organized around a specific set of design principles that shape how we review contributions: + ++ **Proof terms are first-class training data.** We intend this library to serve as a high-quality corpus for machine-learning work on formal proofs. Contributions should be written with that in mind: prefer small focused theorems over large ones, named helper lemmas over opaque rewrite chains, and rich natural-language comments alongside formal statements. ++ **One canonical form per concept.** If a concept is already defined somewhere in the library, please use or re-export the existing definition rather than defining a parallel version with slightly different notation. When in doubt, open a design-discussion issue first. ++ **Stable public APIs with deprecation cycles.** Breaking changes to names or signatures in publicly-used definitions should go through at least one minor-version deprecation cycle. Internal helpers (not re-exported, not documented) can change without notice. ++ **The Setoid tree is canonical.** `src/Setoid/` is the canonical active development tree for 3.0. `src/Base/` contains the pre-3.0 original development and shared foundations still in use; parts of it will be frozen as `Legacy/Base/` during the 3.0 reconstruction (see M2). The planned `Classical/` tree (specific algebraic theories, tracked in M3) and `Cubical/` tree (long-term 4.0 target, tracked in M5) do not yet exist. New contributions usually belong in `Setoid/`; if you're not sure where something fits, open a design-discussion issue first. + +See [`docs/GITHUB_PROJECT.md`](docs/GITHUB_PROJECT.md) for the milestone roadmap. + +--- + +## Development environment + +### Recommended: Nix + +```bash +git clone https://github.com/ualib/agda-algebras.git +cd agda-algebras +nix develop +make check +``` + +This pins Agda 2.8.0 and standard-library 2.3 automatically via the repository's flake. See [`INSTALL.md`](INSTALL.md) for a walkthrough and non-Nix alternatives. + +### Editor + +We recommend Emacs with `agda-mode` or VSCode with the `banacorn.agda-mode` extension. Launch your editor from inside `nix develop` so the pinned Agda is on `PATH`. + +--- + +## Contribution workflow + +Standard [fork-and-pull-request](https://gist.github.com/Chaser324/ce0505fbed06b947d962) workflow. + +1. Fork the repository to your GitHub account. +2. Clone your fork and create a topic branch: `git checkout -b NNN-short-description`, where `NNN` is the issue number you're addressing. +3. Make commits that each do one coherent thing. Each commit message should have a single-line summary followed by an explanatory paragraph when the change is non-trivial. Reference the issue in the commit message with `Part of #NNN`. +4. Run `make check` locally. Your PR must type-check. +5. Open a pull request against `master`. The PR title should match the issue title (e.g. `[M1-3] Add community-health files`). +6. Be prepared to iterate based on review feedback. + +### Commits vs. pull requests + +Small, single-concern PRs are much easier to review than large ones. If a change naturally decomposes into independent pieces, consider opening a sequence of smaller PRs rather than one big one — even if they land on the same branch, they can often be split for reviewability. + +### Working against issues + +If no issue exists for the change you want to make, **please open one first**, especially for non-trivial changes. This gives maintainers a chance to flag design concerns before you invest time writing code. The issue templates under `.github/ISSUE_TEMPLATE/` are there to help. + +--- + +## Code conventions + +### File pragma + +Every `.agda` source file begins with: + +```agda +{-# OPTIONS --cubical-compatible --safe --exact-split #-} +``` + +plus `module X.Y.Z where` on the next non-comment line. + +As of the 3.0 reconstruction, all of `src/` uses `--cubical-compatible`. When the 3.0 consolidation freezes pre-reconstruction content as `Legacy/Base/` (see M2), the frozen tree will retain its historical `--without-K` pragma for stability, but new contributions will not land there. + + +### Naming + ++ **Definitions** are named in the `lowerCamelCase` or `hyphen-case` style depending on local convention in the surrounding module. ++ **Types** start with an uppercase letter. ++ **Predicates** are typically named `IsX` for "X-ness of a single thing" (e.g. `IsHomomorphism`) and `X` for "the type of things with property X" (e.g. `Homomorphism`). ++ Avoid synonyms. If the concept is already called `Hom` elsewhere, call it `Hom` here too. + +A proper style guide, `docs/STYLE.md`, is tracked in M1-4 and will land shortly. Until then, the convention is "follow the style of the surrounding code, and when in doubt ask in the PR." + +### Comments + +Every public definition should have a prose comment block immediately above it explaining what the definition is and why one would use it. For example: + +```agda +-- | `Hom 𝑨 𝑩` is the type of homomorphisms from 𝑨 to 𝑩. A homomorphism +-- | is a function on carriers that commutes with every basic operation +-- | of the signature. See also: `IsHomomorphism` for the predicate +-- | form, and `Base.Homomorphisms.Isomorphisms` for the isomorphism +-- | variant. +Hom : (𝑨 : Algebra α) (𝑩 : Algebra β) → Type _ +Hom 𝑨 𝑩 = ... +``` + +These comments are not decoration — they are part of the training corpus we hope agda-algebras will become. Think of each one as a short paragraph that would help a mathematician approaching this concept for the first time. + +### Module organization + ++ One concept per module where feasible. ++ Module headers name the mathematical object being developed, not the technical construction (prefer `Setoid.Algebras.Congruences` over `Setoid.Algebras.Records.QuotientRecords`). + +### Imports + ++ Tight `using (...)` clauses, not bare `open import X`. ++ Group imports into blocks: stdlib first, then our own modules, with a blank line between. + +--- + +## Mathematical contributions + +If you're adding a theorem or definition that's more than a trivial rearrangement: + ++ Cite the mathematical source in a comment. Textbook and page number, or paper and theorem number. This helps future readers and provides provenance for the training corpus. ++ If the theorem has a well-known name (Birkhoff's HSP theorem, Jónsson's theorem, etc.), use it. ++ If it's novel — as opposed to a formalization of existing mathematics — say so explicitly in the comment, and consider coordinating with a maintainer before the PR. + +--- + +## Questions + ++ **Technical question about Agda or the library**: open a GitHub discussion or ask in the PR itself. ++ **Design-level question** ("should this be a record or a Σ-type?"): open an issue with the `design-discussion` label. ++ **Just want to chat**: the Agda Zulip server has an `#agda-algebras` channel (informal, low-traffic). + +--- + +## Code of Conduct + +By contributing, you agree to abide by the [Code of Conduct](CODE_OF_CONDUCT.md). + + diff --git a/README.md b/README.md index 2b62fdcb..364c7933 100644 --- a/README.md +++ b/README.md @@ -8,7 +8,7 @@ A formalization of universal algebra in [Agda](https://wiki.portal.chalmers.se/agda/pmwiki.php), built on the [Agda standard library](https://github.com/agda/agda-stdlib). -**Status.** Version 2.0 is under active development on `master`. The library currently targets Agda 2.8.0 and standard-library 2.3. Expect breaking changes until 2.0 is released; see [docs/GITHUB_PROJECT.md](docs/GITHUB_PROJECT.md) for the milestone plan. +**Status.** Version 3.0 is under active development on `master`. The library currently targets Agda 2.8.0 and standard-library 2.3. Expect breaking changes until 3.0 is released; see [docs/GITHUB_PROJECT.md](docs/GITHUB_PROJECT.md) for the milestone plan. The **previous** version (called `UALib`, built against [TypeTopology](https://github.com/martinescardo/TypeTopology)) is no longer maintained but remains available: @@ -60,11 +60,7 @@ Older versions of either component are **not** supported on the `master` branch. ## Contributing -Contributions are welcome via the standard -[fork-clone-pull-request](https://gist.github.com/Chaser324/ce0505fbed06b947d962) -workflow. Please read the contributor documentation in `CONTRIBUTING.md` and the -style guide in `docs/STYLE.md` (both currently being drafted as part of Milestone 1; -see the GitHub project board). +Contributions are welcome. See [`CONTRIBUTING.md`](CONTRIBUTING.md) for the development workflow and conventions, and [`CODE_OF_CONDUCT.md`](CODE_OF_CONDUCT.md) for community standards. The style guide ([`docs/STYLE.md`](docs/STYLE.md)) is being drafted as part of Milestone 1; see [`docs/GITHUB_PROJECT.md`](docs/GITHUB_PROJECT.md) for the full roadmap. For questions about mathematical content or large design changes, open a GitHub issue labeled `design-discussion` before writing code. diff --git a/docs/GITHUB_PROJECT.md b/docs/GITHUB_PROJECT.md index c2a50987..fa094597 100644 --- a/docs/GITHUB_PROJECT.md +++ b/docs/GITHUB_PROJECT.md @@ -2,7 +2,7 @@ # agda-algebras — GitHub Project Roadmap -**Project Title**: agda-algebras 2.0 — Infrastructure, Consolidation, Classical Structures, Applications +**Project Title**: agda-algebras 3.0 — Infrastructure, Consolidation, Classical Structures, Applications **Repository**: `ualib/agda-algebras` @@ -10,17 +10,24 @@ --- -## Short Description +## Summary Modernization of agda-algebras in 9 milestones: tooling upgrade/infra (M1), consolidate Base/Setoid (M2), classical structures (M3), style/naming uniformity (M4), Cubical Agda (M5), FLRP (M6), complexity/CSP module (M7), training corpus/LLM (M8), novel-research apps of `Continuous` relation API (M9). +--- -## Project Description +## Description A structured plan to modernize the agda-algebras library. The work is organized into nine milestones: tooling upgrade and infrastructure (M1), consolidation of the Base/Setoid fork (M2), introduction of the long-missing classical structures layer (M3), style and naming uniformity (M4), a Cubical Agda proof-of-concept as the canonical long-term target (M5), prerequisites for work on the Finite Lattice Representation Problem (M6), an extension of the existing algebraic complexity / CSP module for finite templates (M7), publication of a training corpus for language-model work (M8), and novel-research applications of the `Continuous` relation API (M9). After M1 lands, the remaining milestones run largely in parallel. --- +## Note on version numbering + +agda-algebras was released as v2.0.1 in December 2021 ([Zenodo DOI 10.5281/zenodo.5765793](https://doi.org/10.5281/zenodo.5765793)) as an archival artifact for the TYPES 2021 submission. The current reconstruction is a major version bump past that release and is planned as v3.0. The planned Cubical-canonical successor, in which `src/Cubical/` becomes the default development tree, is planned as v4.0. + +--- + ## Labels - `milestone-1-infra` (0075ca) — Milestone 1: Infrastructure health. @@ -45,7 +52,7 @@ A structured plan to modernize the agda-algebras library. The work is organized ### Milestone 1 — Infrastructure health (BLOCKING) -**Description**. Modernize the library's tooling, establish baseline project hygiene, and unblock every subsequent milestone. The library is currently pinned to Agda 2.6.2 / stdlib 1.7; it must move to Agda 2.8.0 / stdlib v2.3 with `--cubical-compatible` replacing `--without-K`. Standard community-health files (CONTRIBUTING, CHANGELOG, CODE_OF_CONDUCT, STYLE) must land. GitHub Actions CI must stand up. README and installation docs must be rewritten for the 2.0 line. +**Description**. Modernize the library's tooling, establish baseline project hygiene, and unblock every subsequent milestone. The library is currently pinned to Agda 2.6.2 / stdlib 1.7; it must move to Agda 2.8.0 / stdlib v2.3 with `--cubical-compatible` replacing `--without-K`. Standard community-health files (CONTRIBUTING, CHANGELOG, CODE_OF_CONDUCT, STYLE) must land. GitHub Actions CI must stand up. README and installation docs must be rewritten for the 3.0 line. **Exit criterion**. `make check` passes under GitHub Actions CI against Agda 2.8.0 / stdlib v2.3; CONTRIBUTING.md, docs/STYLE.md, ROADMAP.md, CHANGELOG.md are merged; README documents the new install path. @@ -53,7 +60,7 @@ A structured plan to modernize the agda-algebras library. The work is organized ### Milestone 2 — Consolidation -**Description**. Resolve the parallel Base/Setoid fork by freezing `Base/` and moving it to `Legacy/Base/`. `Setoid/` is the canonical development tree for 2.0. Within Legacy, consolidate redundant `Base.Structures` implementations and remove abandoned experimental modules. Designate a single canonical proof of Birkhoff's HSP theorem while preserving the pedagogical demonstration variants. +**Description**. Resolve the parallel Base/Setoid fork by freezing `Base/` and moving it to `Legacy/Base/`. `Setoid/` is the canonical development tree for 3.0. Within Legacy, consolidate redundant `Base.Structures` implementations and remove abandoned experimental modules. Designate a single canonical proof of Birkhoff's HSP theorem while preserving the pedagogical demonstration variants. **Exit criterion**. `src/Base/` is in `src/Legacy/Base/` with a deprecation note; `Setoid.Varieties.HSP.Birkhoff` is designated canonical; ADR-001 (Setoid as canonical) is merged; no duplicate implementations of the same concept remain in `Setoid/` or `Legacy/Base/`. @@ -61,7 +68,7 @@ A structured plan to modernize the agda-algebras library. The work is organized ### Milestone 3 — Classical structures layer -**Description**. Introduce the long-missing tower of classical algebraic structures as Σ-typed specific theories over the universal-algebra framework, with record-typed bundle views matching the stdlib `Algebra.Bundles` idiom. Each structure ships as a Signatures / Theories / Structures / Bundles / Small quintuple. Designed so that the underlying equivalence (Setoid in 2.0) can be mechanically substituted for a Cubical path type in 3.0. +**Description**. Introduce the long-missing tower of classical algebraic structures as Σ-typed specific theories over the universal-algebra framework, with record-typed bundle views matching the stdlib `Algebra.Bundles` idiom. Each structure ships as a Signatures / Theories / Structures / Bundles / Small quintuple. Designed so that the underlying equivalence used in the Setoid-based 3.0 line can be mechanically replaced by a Cubical path type when the 4.0 Cubical track becomes canonical. Phase 1: Magma, Semigroup, CommutativeSemigroup, Monoid, CommutativeMonoid, Group, AbelianGroup, Semilattice, Lattice. @@ -89,7 +96,7 @@ Phase 2: Ring, CommutativeRing, Field, Module, DistributiveLattice, BooleanAlgeb ### Milestone 6 — Toward the Finite Lattice Representation Problem -**Description**. Build the specialized universal-algebraic infrastructure needed to tackle the Finite Lattice Representation Problem: "Does every finite lattice occur as the congruence lattice of a finite algebra?" Near-term prerequisites include `Con 𝑨` and `Sub 𝑨` as complete lattices, subdirect products, subdirectly irreducible algebras, and basic Maltsev conditions relevant to lattice representations. *Medium-term*. Jónsson's theorem, Day's theorem. Long-term (out of scope for 2.0): tame congruence theory, commutator theory, explicit representations of small lattices. +**Description**. Build the specialized universal-algebraic infrastructure needed to tackle the Finite Lattice Representation Problem: "Does every finite lattice occur as the congruence lattice of a finite algebra?" Near-term prerequisites include `Con 𝑨` and `Sub 𝑨` as complete lattices, subdirect products, subdirectly irreducible algebras, and basic Maltsev conditions relevant to lattice representations. *Medium-term*. Jónsson's theorem, Day's theorem. Long-term (out of scope for 3.0): tame congruence theory, commutator theory, explicit representations of small lattices. **Exit criterion**. `Con 𝑨` is a complete lattice; subdirect products and subdirectly irreducible algebras are defined with basic properties proven; at least one Maltsev condition (congruence permutability via the Maltsev term characterization) is proven. @@ -185,7 +192,7 @@ The library is currently pinned to Agda 2.6.2 / stdlib 1.7. The Agda ecosystem - [ ] Library type-checks under Agda 2.8.0 / stdlib v2.3. - [ ] `make check` succeeds locally. - [ ] No file still declares `--without-K`. -- [ ] Once 2.0 is stable, consider adding a CI job against Agda 2.9/dev to catch forward-compatibility issues early. +- [ ] Once 3.0 is stable, consider adding a CI job against Agda 2.9/dev to catch forward-compatibility issues early. --- @@ -225,12 +232,12 @@ The library has no CI. Contributors can break type-checking without maintainers ## Description -Standard community-health files are missing. Drafts of CONTRIBUTING and STYLE exist from the 2.0 planning cycle and can be merged after review. +Standard community-health files are missing. Drafts of CONTRIBUTING and STYLE exist from the 3.0 planning cycle and can be merged after review. ## Tasks - [ ] Add `CONTRIBUTING.md` (draft from planning cycle). -- [ ] Add `CHANGELOG.md` seeded with the 2.0 milestone entry. +- [ ] Add `CHANGELOG.md` seeded with the 3.0 milestone entry. - [ ] Add `CODE_OF_CONDUCT.md` (Contributor Covenant 2.1). - [ ] Add `.github/ISSUE_TEMPLATE/` with bug-report, feature-request, and design-discussion templates. - [ ] Add `.github/PULL_REQUEST_TEMPLATE.md`. @@ -264,7 +271,7 @@ Create `docs/STYLE.md` documenting file format, module structure, naming convent --- -### Issue M1-5: Rewrite README and Preface for the 2.0 release +### Issue M1-5: Rewrite README and Preface for the 3.0 release **Labels**: `milestone-1-infra`, `documentation` @@ -272,7 +279,7 @@ Create `docs/STYLE.md` documenting file format, module structure, naming convent ## Description -The current `README.md` and `docs/lagda/Preface.lagda` are 1.x-era: wrong Agda versions, obsolete installation paths, pre-consolidation library structure. They need a rewrite aligned with the 2.0 release. Depends on M1-1 through M1-4 and M2-1. +The current `README.md` and `docs/lagda/Preface.lagda` are 1.x-era: wrong Agda versions, obsolete installation paths, pre-consolidation library structure. They need a rewrite aligned with the 3.0 release. Depends on M1-1 through M1-4 and M2-1. ## Tasks @@ -305,7 +312,7 @@ As the library evolves, design decisions (Setoid vs Base canonicality, record vs - [ ] Create `docs/adr/` directory. - [ ] Add `docs/adr/README.md` explaining the ADR format. - [ ] Add `docs/adr/000-template.md`. -- [ ] Seed with decisions ratified in 2.0: +- [ ] Seed with decisions ratified in 3.0: - `001-setoid-as-canonical.md` (from M2-1); - `002-classical-layer-design.md` (from M3-1); - `003-cubical-canonical-target.md` (from M5-1). @@ -319,7 +326,7 @@ As the library evolves, design decisions (Setoid vs Base canonicality, record vs ### Milestone 1 Dependencies -M1-5 is the integration node: the new README / Preface needs all the other M1 deliverables to exist before it can refer to them. M1-6 (docs/adr/) is structurally independent but is gated on M1-1 because it references the 2.0 release. +M1-5 is the integration node: the new README / Preface needs all the other M1 deliverables to exist before it can refer to them. M1-6 (docs/adr/) is structurally independent but is gated on M1-1 because it references the 3.0 release. ```mermaid graph TD @@ -353,11 +360,11 @@ graph TD ## Description -The decision is ratified: `Setoid/` is the canonical development tree for 2.0; `Base/` is frozen and moved to `Legacy/Base/`. Rationale: `Setoid/` is fully constructive (no extensionality postulates); it matches the stdlib `Algebra.Bundles` idiom which simplifies bridges; maintaining two trees indefinitely doubles every theorem's cost; `Setoid/` already contains the definitive HSP proof. +The decision is ratified: `Setoid/` is the canonical development tree for 3.0; `Base/` is frozen and moved to `Legacy/Base/`. Rationale: `Setoid/` is fully constructive (no extensionality postulates); it matches the stdlib `Algebra.Bundles` idiom which simplifies bridges; maintaining two trees indefinitely doubles every theorem's cost; `Setoid/` already contains the definitive HSP proof. Note: `Base/` remains in the repo — frozen, not deleted — for posterity and as a reference. Parts may be ported back to `Setoid/` or `Cubical/` as needed. -This is a breaking change for downstream users of `Base/`. Announce prominently in the 2.0 CHANGELOG. +This is a breaking change for downstream users of `Base/`. Announce prominently in the 3.0 CHANGELOG. ## Tasks @@ -493,7 +500,7 @@ Ratified design decisions (to be recorded in `docs/adr/002-classical-layer.md`): 1. Each classical structure `X` is Σ-typed at the core: `X α ρ = Σ[ 𝑨 ∈ Algebra 𝑆ₓ α ρ ] 𝑨 ⊨ Eₓ`. The mathematical reading "X *is* an algebra equipped with a proof it satisfies the X-theory" motivates Σ over record for classical structures. The core `Algebra` type stays a record. 2. A parallel record-typed "bundle view" in `Classical/Bundles/X` matches the stdlib `Algebra.Bundles` idiom for interop. 3. Built on `Setoid/` (not `Base/`). A helper `fromPropEq : Type α → ... → X α α` lets users build classical structures from propositional-equality-based definitions without explicit Setoid wrapping. -4. Designed for Cubical portability. Equations stated purely in terms of `Algebra.Domain`'s equivalence — never reaching for Setoid-specific features without a Cubical analog. When `Cubical/` becomes canonical in 3.0, the port should be mechanical. +4. Designed for Cubical portability. Equations stated purely in terms of `Algebra.Domain`'s equivalence — never reaching for Setoid-specific features without a Cubical analog. When `Cubical/` becomes canonical in 4.0, the port should be mechanical. 5. Two levels of specificity per structure: polymorphic core (`Classical.Structures.X`) and level-fixed veneer (`Classical.Small.Structures.X`) for the common `ℓ₀` case. ## Tasks @@ -816,7 +823,7 @@ Every record, type family, and top-level function in the public API should have ## Description -Cubical Agda is the canonical long-term target for this library. This issue establishes the path: port the core algebra types, prove the structure identity principle (SIP), and demonstrate end-to-end workflow by porting Monoid from the Setoid-based Classical layer to a Cubical counterpart. The ultimate goal is for Cubical to become the default development track in version 3.0, with `Setoid/` moving to Legacy. +Cubical Agda is the canonical long-term target for this library. This issue establishes the path: port the core algebra types, prove the structure identity principle (SIP), and demonstrate end-to-end workflow by porting Monoid from the Setoid-based Classical layer to a Cubical counterpart. The ultimate goal is for Cubical to become the default development track in version 4.0. Design implication for M3: the Classical layer must be designed so that the Setoid-to-Cubical port is mechanical — equations stated purely in terms of the `Algebra` record's Domain equivalence, no Setoid-specific gadgets in the definitions of classical structures themselves. @@ -826,7 +833,7 @@ Design implication for M3: the Classical layer must be designed so that the Seto - [ ] `Cubical/Algebras/SIP.agda`: structure identity principle. Port or adapt from the `cubical` or `1Lab` library. - [ ] Prove: `≅` as defined for Cubical algebras is equivalent to path equality (the central "transport does what we want" result). - [ ] End-to-end port: take `Classical/Structures/Monoid.agda` from the Setoid-based version (post M3-4) and produce the Cubical analog. Verify that equations transport by substitution alone. -- [ ] Write `docs/adr/003-cubical-canonical-target.md` explicitly planning the 3.0 transition and the criteria for promoting Cubical from experimental to canonical. +- [ ] Write `docs/adr/003-cubical-canonical-target.md` explicitly planning the 4.0 transition and the criteria for promoting Cubical from experimental to canonical. ## Acceptance criteria diff --git a/flake.nix b/flake.nix index ab7fa056..c76a5b6f 100644 --- a/flake.nix +++ b/flake.nix @@ -6,7 +6,7 @@ # Goals: # # 1. `nix develop` from the repo root drops you in a shell with exactly the -# Agda / stdlib versions agda-algebras 2.0 targets. No ~/.config/agda +# Agda / stdlib versions agda-algebras 3.0 targets. No ~/.config/agda # configuration required (or consulted). # 2. Reproducibility via flake.lock. The nixpkgs input pin *is* the Agda/ # stdlib pin.