[M1-3] Add community-health files and renumber 2.0 → 3.0#286
Merged
Conversation
7 tasks
williamdemeo
force-pushed
the
252-m1-3-add-contributing-docs
branch
2 times, most recently
from
53a98a2 to
bf256a2
Compare
The archival release v2.0.1 was published in December 2021 for the TYPES 2021 submission (Zenodo DOI 10.5281/zenodo.5765793) and is referenced in published papers and downstream projects. That version number is now part of the scholarly record; the current reconstruction is a major version bump past it. Call the current line 3.0 throughout: planning documents, README, documentation files, and internal cross-references. The forthcoming Cubical-canonical development (previously "3.0" in the planning docs) is renumbered to 4.0 accordingly. No change to the v2.0.1 BibTeX entry: that reference stays verbatim as citation for the 2021 archival deposit. Part of #252 (M1-3).
+ CONTRIBUTING.md documents the development workflow, Nix-based toolchain setup, and the library-specific conventions that shape how we review contributions (library-as-training-corpus considerations, the Setoid/Classical/Cubical tree split, stable public APIs with deprecation cycles). + CODE_OF_CONDUCT.md adopts the Contributor Covenant 3.0 (the current version, superseding the 2.1 mentioned in #252). Fills in the "Addressing and Repairing Harm" section with concrete reporting contacts for this project. + CHANGELOG.md seeded in Keep-a-Changelog format with the in-progress 2.0 entry. Prior versions are acknowledged in a "1.x" stub that points at the git log; retroactively reconstructing per-version changelogs for the 1.x era is not in scope. Part of #252 (M1-3).
+ .github/ISSUE_TEMPLATE/bug_report.yml collects reproduction information plus pinned Agda/stdlib versions and installation method, which are the primary axes of environmental variation. + .github/ISSUE_TEMPLATE/feature_request.yml asks for the mathematical context (paper / textbook citation) of proposed additions, supporting provenance in the training corpus, and prompts for which tree (Setoid/Classical/Cubical) and which milestone the proposal targets. + .github/ISSUE_TEMPLATE/design_discussion.yml provides scaffolding for the "should X be record or Σ" questions that come up often in a library going through active reconstruction. + .github/ISSUE_TEMPLATE/config.yml disables blank issues and points to the project roadmap and (if enabled) GitHub Discussions. + .github/PULL_REQUEST_TEMPLATE.md provides a lightweight PR checklist — keep it short because a long template gets ignored. Part of #252 (M1-3).
Part of #252 (M1-3).
williamdemeo
force-pushed
the
252-m1-3-add-contributing-docs
branch
from
bf256a2 to
5c46190
Compare
Contributor
There was a problem hiding this comment.
Pull request overview
This PR adds standard GitHub community-health collateral (contributing guide, code of conduct, changelog, issue/PR templates) and updates repository documentation references to reflect the 3.0 reconstruction line (renumbering from 2.0 → 3.0).
Changes:
- Add community-health files:
CONTRIBUTING.md,CODE_OF_CONDUCT.md,CHANGELOG.md,.github/issue templates, and a PR template. - Renumber “2.0” references to “3.0” in key repo docs (roadmap, README, Nix flake comment).
- Seed an “Unreleased / 3.0 development” changelog entry and preserve the archival
2.0.1release section.
Reviewed changes
Copilot reviewed 11 out of 11 changed files in this pull request and generated 10 comments.
Show a summary per file
| File | Description |
|---|---|
| flake.nix | Updates top-level comment to refer to 3.0 target environment. |
| docs/GITHUB_PROJECT.md | Renumbers roadmap references and adjusts milestone text for 3.0. |
| README.md | Updates status line and refreshes contributing links. |
| CONTRIBUTING.md | Adds contributor workflow, environment setup, and conventions. |
| CODE_OF_CONDUCT.md | Adds Contributor Covenant 3.0 based code of conduct and reporting info. |
| CHANGELOG.md | Adds Keep-a-Changelog formatted changelog with Unreleased (3.0) and 2.0.1 sections. |
| .github/PULL_REQUEST_TEMPLATE.md | Adds PR checklist template. |
| .github/ISSUE_TEMPLATE/feature_request.yml | Adds feature request issue form. |
| .github/ISSUE_TEMPLATE/design_discussion.yml | Adds design discussion issue form. |
| .github/ISSUE_TEMPLATE/config.yml | Configures issue templates (disables blank issues, adds roadmap link). |
| .github/ISSUE_TEMPLATE/bug_report.yml | Adds bug report issue form. |
💡 Add Copilot custom instructions for smarter, more guided reviews. Learn how to get started.
Reflects current repo state accurately in the community-health files while preserving forward-looking signals for planned trees. + CONTRIBUTING.md, PR template, and issue templates now describe the Base/ + Setoid/ layout that exists today, with planned Classical/ (M3), Cubical/ (M5), and Legacy/Base/ (M2) tagged explicitly as future work (Copilot comments 3, 4, 5, 9). + CHANGELOG.md corrected to reference INSTALL.md at the repo root rather than a nonexistent docs/INSTALL.md (Copilot comments 6, 10). + .github/ISSUE_TEMPLATE/config.yml corrected from doc/ to docs/ (Copilot comment 8). + .github/ISSUE_TEMPLATE/feature_request.yml uses an absolute URL for the roadmap link (Copilot comment 2) and renumbers the Setoid option to 3.0 (Copilot 3). + docs/GITHUB_PROJECT.md M3 description clarifies that the Cubical-target phrasing refers to the future 4.0 track, not the current 3.0 reconstruction (Copilot comment 7). + Adds a short "A note on version numbering" section to docs/GITHUB_PROJECT.md explaining the v2.0.1 → 3.0 → 4.0 sequence (Copilot comment 1). Part of #252 (M1-3).
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
Adds the standard community-health files (
CONTRIBUTING.md,CODE_OF_CONDUCT.md,CHANGELOG.md, issue templates, PR template) and renumbers the reconstruction line from 2.0 to 3.0 throughout the repository to respect the archival v2.0.1 release from December 2021.Closes #252.
Contents
Community-health files
CONTRIBUTING.md— documents the Nix-based development workflow, fork-and-pull-request conventions, and the library-specific considerations that shape how we review contributions. Emphasizes the library-as-training-corpus character (small focused theorems, named helper lemmas, rich prose comments), the Setoid/Classical/Cubical tree split, and stable public APIs with deprecation cycles.CODE_OF_CONDUCT.md— adopts Contributor Covenant 3.0, the current version (superseding the 2.1 originally mentioned in [M1-3] Add CONTRIBUTING.md, CHANGELOG.md, CODE_OF_CONDUCT.md #252). Fills in the "Addressing and Repairing Harm" section with a concrete reporting address.CHANGELOG.md— seeded in Keep a Changelog format. Contains the in-progress 3.0 entry, a separate [2.0.1] section linking the Zenodo deposit so that archival release stays visible in the change log, and a [1.x and earlier] stub pointing at the git log for the pre-v2.0.1 era..github/ISSUE_TEMPLATE/— three templates (bug_report, feature_request, design_discussion) plus aconfig.ymldisabling blank issues. The feature_request template prompts for mathematical context (paper/textbook citation) and target tree (Setoid/Classical/Cubical), supporting provenance in the training corpus. The design_discussion template scaffolds the "should X be a record or Σ-type" questions that come up often in a library under active reconstruction..github/PULL_REQUEST_TEMPLATE.md— lightweight PR checklist. Deliberately kept short; long templates get ignored.Renumbering
The archival release v2.0.1 was published in December 2021 for the TYPES 2021 submission (Zenodo DOI 10.5281/zenodo.5765793) and is referenced in published papers and downstream projects (thmpr.org credits page among them). That version number is part of the scholarly record.
Continuing to call the current reconstruction "agda-algebras 2.0" would be semantically wrong: the work breaks essentially everything from v2.0.1 (Agda 2.6.2 → 2.8.0, stdlib 1.7 → 2.3,
--without-K→--cubical-compatible, Base/ frozen and moved to Legacy/, directory layout changes, dual-license change, canonical HSP proof relocation). That's the textbook definition of a major version bump.This PR therefore renumbers throughout:
Files updated:
docs/GITHUB_PROJECT.md(titles, project description, milestone descriptions, exit criteria, M5 Cubical-target references, M3-1 design-decisions note);README.md;docs/lagda/Overture/Basic.lagda;docs/INSTALL.md. The v2.0.1 BibTeX entry is intentionally preserved verbatim as a citation for the 2021 deposit.docs/GITHUB_PROJECT.mdnow includes a short "A note on version numbering" section near the top explaining the v2.0.1 → 3.0 → 4.0 sequence, so anyone reading the roadmap can orient themselves without archaeology.Notes for reviewers
The renumbering was done as a single sweep across the repository with
rgto enumerate hits, then edited in batches. The result is mechanically uniform.GitHub issue descriptions (for [M1-1] Upgrade to Agda 2.8.0 and stdlib v2.3; replace
--without-Kwith--cubical-compatible#250, [M1-2] Add GitHub Actions CI to type-check the library #251, [M1-3] Add CONTRIBUTING.md, CHANGELOG.md, CODE_OF_CONDUCT.md #252, [M5-2] Monitor agda/agda-stdlib#2967 and finalize cubical-port flag strategy #279, [M1-9] Simplify Nix agda wrapper: drop defensive flags and rely on auto-discovery #285, and this PR's own description) were also edited in the GitHub UI to reflect the renumber, so the scholarly record and the planning record agree.CODE_OF_CONDUCT.mduses[email protected]as the reporting address. This is already in the public domain via the GitHub profile and prior publications; the marginal spam impact is essentially zero.GitHub Discussions is deliberately not linked from
.github/ISSUE_TEMPLATE/config.yml. The consensus after discussion was that empty Discussions tabs are worse than no Discussions tab for a project at this scale; Discussions will be enabled later if a concrete trigger emerges.The existing
CONTRIBUTING.mdreference inREADME.mdwas already updated to match during [M1-1] Upgrade to Agda 2.8.0+stdlib 2.3;--without-K->--cubical-compatible#278 (license + docs rename), so no additional README patching is needed in this PR.Follow-up, not blocking this PR
docs/STYLE.mdis tracked in M1-4 and referenced from CONTRIBUTING.md. TheCONTRIBUTING.mddraft explicitly says the style guide is "tracked in M1-4 and will land shortly" so the forward reference is not a broken link, just a promissory one.Contributor Covenant translations — if the project ever attracts non-English-speaking contributors, Contributor Covenant has official translations available. Not a concern at current scale.