[M1-1] Upgrade to Agda 2.8.0+stdlib 2.3; --without-K -> --cubical-compatible#278
Merged
Merged
Conversation
As of Agda 2.6.3, --without-K is superseded by --cubical-compatible. The new flag is a strict improvement: it additionally checks compatibility with cubical Agda's stricter rules for pattern matching on indexed inductive types, which the library will rely on when the Cubical/ tree becomes canonical (M5, per the 2.0 roadmap). This commit is purely mechanical: every occurrence of the old flag is replaced with the new flag. Imports and code are untouched. The library will not type-check after this commit alone; that work is tracked in subsequent commits on this branch addressing the stdlib 1.7 → 2.3 API migration. Part of #250.
Closed
11 tasks
williamdemeo
changed the title
--without-K -> --cubical-compatible
Collaborator
|
You should definitely be aware that |
The previous nix/flake.nix was architecturally wrong: it tried to construct agda-algebras as `haskellPackages.agda-algebras` via `makeHaskellPackage`, which is not appropriate for an Agda library. Replace it with a clean top-level flake that + takes a single `nixpkgs` input on `nixos-unstable`; the flake.lock pins the revision, which in turn pins Agda 2.8.0 and stdlib 2.3; + exposes `devShells.default` wiring them together via `agda.withPackages`, and writes a project-local AGDA_DIR at $ROOT/.agda that shadows the user's ~/.config/agda/ entirely (a globally-registered stdlib 2.2 will NOT leak into this shell); + defines an `agda()` shell wrapper that re-passes --library-file and --no-default-libraries, so Agda's last-flag-wins rule uses the project-local libraries file rather than the nix wrapper's baked-in one; + supports x86_64-linux, aarch64-linux (Jetson), and both darwin arches; + exports an overlay (agda-algebras-agda) and package for downstream flakes. Also update agda-algebras.agda-lib to `depend: standard-library-2.3` to document the required minimum (the v2.3 tag of stdlib registers itself under that exact versioned name; Agda's library resolver requires an exact match when a version is given, any version when omitted). Drop nix/default.nix, nix/flake.lock, and nix/README_NIXOS.md — all of which documented or supported the old, broken model. Part of #250 (M1-1).
Reorganize into titled sections; add brief header explaining gitignore syntax subtleties (no inline comments, leading `/` anchors to repo root). Add conventional entries that were missing: + Emacs lock/auto-save: `.#*`, `\#*\#` + Vim swap: `*.swp`, `*.swo` + Nix build outputs: `/result`, `/result-*` + nix-direnv cache: `.direnv/` Quarantine legacy paper-submission paths (TYPES2021, ITP2021, ARCHIVE, Notes/Complexity, referee, makefile-, mk) under a "Legacy / historical" header to be pruned in a dedicated follow-up once we confirm nothing in the current build writes to them. No functional change.
Member
Author
Thank you so much for pointing this out! You just saved me a ton of refactor churn! After looking more closely at the issue and considering the goals of |
The previous Makefile targeted .lagda files (a stale assumption after the flattening to .agda) and contained a brittle `s/.agda//` sed substitution — unanchored, with an unescaped `.` — that eats the `import ` prefix whenever a path segment contains the substring "agda". Rewrite: + Source discovery via `find` instead of `git ls-tree HEAD`, so uncommitted files in the working tree are included during development. + Anchored, escaped regex `s|\.agda$||` strips only the trailing extension. + Preemptively exclude src/Legacy/ from the scan (M2 will move src/Base/ there). + Drop the dead .tex/.md/Jekyll plumbing; it never worked with the flat-.agda layout and a proper docs pipeline belongs in a separate PR against the .lagda.md migration (#M1-5). Also: standardize `make check` as the canonical type-check target (what CI will call); keep `make test` as an alias. Part of #250 (M1-1).
Update versions (Agda 2.8.0, stdlib 2.3), replace the hand-crafted cabal-install instructions with `nix develop`, and defer non-Nix installation guidance to doc/INSTALL.md. Mark the 2.0 line as α software with a pointer to the milestone plan. Link to `doc/INSTALL.md` (added in the same PR) and `doc/STYLE.md` (tracked in M1-4, forthcoming). Add a citation placeholder for the Zenodo entry that will follow the 2.0 release. Part of #250 (M1-1).
Add a deprecation banner at the top pointing readers to the new doc/INSTALL.md. Keep the file's content for historical continuity (it documents the pre-Nix, pre-2.8.0 workflow Martín Escardó originally authored for MGS 2019); schedule for removal in a future release once external link rot is unlikely. Part of #250 (M1-1).
Document four installation paths: (1) Nix via `nix develop` (recommended), (2) the Python installer new in Agda 2.8.0, (3) prebuilt binaries from the Agda GitHub release, (4) cabal from Hackage. Include troubleshooting notes for common issues (stdlib resolution, UnsupportedIndexedMatch warnings, build time) and verification steps. Replaces the role of the legacy doc/INSTALL_AGDA.md, which is now deprecated (see separate commit marking it so). Part of #250 (M1-1).
Flip the OPTIONS pragma from --without-K to --cubical-compatible and update the accompanying prose. Explain the flag change, why --cubical-compatible is strictly what we want given the Cubical port goal, and how the -WnoUnsupportedIndexedMatch suppression relates to it. This file lives under doc/lagda/, which is scheduled for consolidation with src/ under .lagda.md (tracked in M1-6). This commit maintains the deprecation-cycle contract — a third party reading doc/lagda/ today gets accurate guidance — even though the file itself is slated for replacement. Part of #250 (M1-1).
Contributor
There was a problem hiding this comment.
Pull request overview
This PR advances the agda-algebras 2.0 upgrade work by moving the codebase to Agda 2.8.0 + stdlib 2.3 conventions (notably --cubical-compatible), and by adding a top-level Nix flake + updated docs/Makefile to support a reproducible dev environment.
Changes:
- Replace deprecated
--without-Kwith--cubical-compatibleacross library modules and literate docs. - Pin the library dependency to
standard-library-2.3and suppressUnsupportedIndexedMatchwarnings viaagda-algebras.agda-lib. - Introduce root
flake.nix/flake.lock, updateMakefile, and refresh install/docs (including deprecatingdoc/INSTALL_AGDA.md).
Reviewed changes
Copilot reviewed 266 out of 268 changed files in this pull request and generated 5 comments.
Show a summary per file
| File | Description |
|---|---|
| src/agda-algebras.agda | Update OPTIONS pragma to --cubical-compatible. |
| src/Setoid/Varieties/SoundAndComplete.agda | Pragma update. |
| src/Setoid/Varieties/Properties.agda | Pragma update. |
| src/Setoid/Varieties/Preservation.agda | Pragma update. |
| src/Setoid/Varieties/HSP.agda | Pragma update. |
| src/Setoid/Varieties/FreeAlgebras.agda | Pragma update. |
| src/Setoid/Varieties/EquationalLogic.agda | Pragma update. |
| src/Setoid/Varieties/Closure.agda | Pragma update. |
| src/Setoid/Varieties.agda | Pragma update. |
| src/Setoid/Terms/Properties.agda | Pragma update. |
| src/Setoid/Terms/Operations.agda | Pragma update. |
| src/Setoid/Terms/Basic.agda | Pragma update. |
| src/Setoid/Terms.agda | Pragma update. |
| src/Setoid/Subalgebras/Subuniverses.agda | Pragma update. |
| src/Setoid/Subalgebras/Subalgebras.agda | Pragma update. |
| src/Setoid/Subalgebras/Properties.agda | Pragma update. |
| src/Setoid/Subalgebras.agda | Pragma update. |
| src/Setoid/Relations/Quotients.agda | Pragma update. |
| src/Setoid/Relations/Discrete.agda | Pragma update. |
| src/Setoid/Relations.agda | Pragma update. |
| src/Setoid/Homomorphisms/Properties.agda | Pragma update. |
| src/Setoid/Homomorphisms/Products.agda | Pragma update. |
| src/Setoid/Homomorphisms/Noether.agda | Pragma update. |
| src/Setoid/Homomorphisms/Kernels.agda | Pragma update. |
| src/Setoid/Homomorphisms/Isomorphisms.agda | Pragma update. |
| src/Setoid/Homomorphisms/HomomorphicImages.agda | Pragma update. |
| src/Setoid/Homomorphisms/Factor.agda | Pragma update. |
| src/Setoid/Homomorphisms/Basic.agda | Pragma update. |
| src/Setoid/Homomorphisms.agda | Pragma update. |
| src/Setoid/Functions/Surjective.agda | Pragma update. |
| src/Setoid/Functions/Inverses.agda | Pragma update. |
| src/Setoid/Functions/Injective.agda | Pragma update. |
| src/Setoid/Functions/Bijective.agda | Pragma update. |
| src/Setoid/Functions/Basic.agda | Pragma update. |
| src/Setoid/Functions.agda | Pragma update. |
| src/Setoid/Algebras/Products.agda | Pragma update. |
| src/Setoid/Algebras/Congruences.agda | Pragma update. |
| src/Setoid/Algebras/Basic.agda | Pragma update. |
| src/Setoid/Algebras.agda | Pragma update. |
| src/Setoid.agda | Pragma update. |
| src/Overture/Signatures.agda | Pragma update. |
| src/Overture/Preface.agda | Pragma update. |
| src/Overture/Operations.agda | Pragma update. |
| src/Overture/Basic.agda | Pragma update. |
| src/Overture.agda | Pragma update. |
| src/Exercises/Complexity/FiniteCSP.agda | Pragma update. |
| src/Exercises/Complexity.agda | Pragma update. |
| src/Exercises.agda | Pragma update. |
| src/Examples/Structures/Signatures.agda | Pragma update. |
| src/Examples/Structures/Basic.agda | Pragma update. |
| src/Examples/Structures.agda | Pragma update. |
| src/Examples/Categories/Functors.agda | Pragma update. |
| src/Examples/Categories.agda | Pragma update. |
| src/Examples.agda | Pragma update. |
| src/Demos/HSP.agda | Pragma update. |
| src/Demos/GeneralOperationsAndRelations.agda | Pragma update. |
| src/Demos/ContraX.agda | Pragma update. |
| src/Demos.agda | Pragma update. |
| src/Base/Varieties/Properties.agda | Pragma update. |
| src/Base/Varieties/Preservation.agda | Pragma update. |
| src/Base/Varieties/Invariants.agda | Pragma update. |
| src/Base/Varieties/FreeAlgebras.agda | Pragma update. |
| src/Base/Varieties/EquationalLogic.agda | Pragma update. |
| src/Base/Varieties/Closure.agda | Pragma update. |
| src/Base/Varieties.agda | Pragma update. |
| src/Base/Terms/Properties.agda | Pragma update. |
| src/Base/Terms/Operations.agda | Pragma update. |
| src/Base/Terms/Basic.agda | Pragma update. |
| src/Base/Terms.agda | Pragma update. |
| src/Base/Subalgebras/Subuniverses.agda | Pragma update. |
| src/Base/Subalgebras/Subalgebras.agda | Pragma update. |
| src/Base/Subalgebras/Properties.agda | Pragma update. |
| src/Base/Subalgebras.agda | Pragma update. |
| src/Base/Structures/Terms.agda | Pragma update. |
| src/Base/Structures/Substructures.agda | Pragma update. |
| src/Base/Structures/Sigma/Products.agda | Pragma update. |
| src/Base/Structures/Sigma/Isos.agda | Pragma update. |
| src/Base/Structures/Sigma/Homs.agda | Pragma update. |
| src/Base/Structures/Sigma/Congruences.agda | Pragma update. |
| src/Base/Structures/Sigma/Basic.agda | Pragma update. |
| src/Base/Structures/Sigma.agda | Pragma update. |
| src/Base/Structures/Products.agda | Pragma update. |
| src/Base/Structures/Isos.agda | Pragma update. |
| src/Base/Structures/Homs.agda | Pragma update. |
| src/Base/Structures/Graphs0.agda | Pragma update. |
| src/Base/Structures/Graphs.agda | Pragma update. |
| src/Base/Structures/EquationalLogic.agda | Pragma update. |
| src/Base/Structures/Congruences.agda | Pragma update. |
| src/Base/Structures/Basic.agda | Pragma update. |
| src/Base/Structures.agda | Pragma update. |
| src/Base/Relations/Quotients.agda | Pragma update. |
| src/Base/Relations/Properties.agda | Pragma update. |
| src/Base/Relations/Discrete.agda | Pragma update. |
| src/Base/Relations/Continuous.agda | Pragma update. |
| src/Base/Relations.agda | Pragma update. |
| src/Base/Homomorphisms/Properties.agda | Pragma update. |
| src/Base/Homomorphisms/Products.agda | Pragma update. |
| src/Base/Homomorphisms/Noether.agda | Pragma update. |
| src/Base/Homomorphisms/Kernels.agda | Pragma update. |
| src/Base/Homomorphisms/Isomorphisms.agda | Pragma update. |
| src/Base/Homomorphisms/HomomorphicImages.agda | Pragma update. |
| src/Base/Homomorphisms/Factor.agda | Pragma update. |
| src/Base/Homomorphisms/Basic.agda | Pragma update. |
| src/Base/Homomorphisms.agda | Pragma update. |
| src/Base/Functions/Transformers.agda | Pragma update. |
| src/Base/Functions/Surjective.agda | Pragma update. |
| src/Base/Functions/Inverses.agda | Pragma update. |
| src/Base/Functions/Injective.agda | Pragma update. |
| src/Base/Functions.agda | Pragma update. |
| src/Base/Equality/Welldefined.agda | Pragma update. |
| src/Base/Equality/Truncation.agda | Pragma update. |
| src/Base/Equality/Extensionality.agda | Pragma update. |
| src/Base/Equality.agda | Pragma update. |
| src/Base/Complexity/CSP.agda | Pragma update. |
| src/Base/Complexity/Basic.agda | Pragma update. |
| src/Base/Complexity.agda | Pragma update. |
| src/Base/Categories/Functors.agda | Pragma update. |
| src/Base/Categories.agda | Pragma update. |
| src/Base/Algebras/Products.agda | Pragma update. |
| src/Base/Algebras/Congruences.agda | Pragma update. |
| src/Base/Algebras/Basic.agda | Pragma update. |
| src/Base/Algebras.agda | Pragma update. |
| src/Base/Adjunction/Residuation.agda | Pragma update. |
| src/Base/Adjunction/Galois.agda | Pragma update. |
| src/Base/Adjunction/Closure.agda | Pragma update. |
| src/Base/Adjunction.agda | Pragma update. |
| src/Base.agda | Pragma update. |
| doc/papers/wjd.sty | Update embedded Agda OPTIONS snippet. |
| doc/papers/TYPES2021/wjd.sty | Update embedded Agda OPTIONS snippet. |
| doc/lagda/agda-algebras.lagda | Pragma update in literate docs. |
| doc/lagda/Overture/Basic.lagda | Update pragma and expand explanation of --cubical-compatible. |
| doc/lagda/Base.lagda | Pragma update in literate docs. |
| doc/lagda/Base/Adjunction.lagda | Pragma update in literate docs. |
| doc/lagda/Base/Adjunction/Closure.lagda | Pragma update in literate docs. |
| doc/lagda/Base/Adjunction/Galois.lagda | Pragma update in literate docs. |
| doc/lagda/Base/Adjunction/Residuation.lagda | Pragma update in literate docs. |
| doc/lagda/Base/Algebras.lagda | Pragma update in literate docs. |
| doc/lagda/Base/Algebras/Basic.lagda | Pragma update in literate docs. |
| doc/lagda/Base/Algebras/Congruences.lagda | Pragma update in literate docs. |
| doc/lagda/Base/Algebras/Products.lagda | Pragma update in literate docs. |
| doc/lagda/Base/Categories.lagda | Pragma update in literate docs. |
| doc/lagda/Base/Categories/Functors.lagda | Pragma update in literate docs. |
| doc/lagda/Base/Complexity.lagda | Pragma update in literate docs. |
| doc/lagda/Base/Complexity/Basic.lagda | Pragma update in literate docs. |
| doc/lagda/Base/Complexity/CSP.lagda | Pragma update in literate docs. |
| doc/lagda/Base/Equality.lagda | Pragma update in literate docs. |
| doc/lagda/Base/Equality/Extensionality.lagda | Pragma update in literate docs. |
| doc/lagda/Base/Equality/Truncation.lagda | Pragma update in literate docs. |
| doc/lagda/Base/Equality/Welldefined.lagda | Pragma update in literate docs. |
| doc/lagda/Base/Functions.lagda | Pragma update in literate docs. |
| doc/lagda/Base/Functions/Injective.lagda | Pragma update in literate docs. |
| doc/lagda/Base/Functions/Inverses.lagda | Pragma update in literate docs. |
| doc/lagda/Base/Functions/Surjective.lagda | Pragma update in literate docs. |
| doc/lagda/Base/Functions/Transformers.lagda | Pragma update in literate docs. |
| doc/lagda/Base/Homomorphisms.lagda | Pragma update in literate docs. |
| doc/lagda/Base/Homomorphisms/Basic.lagda | Pragma update in literate docs. |
| doc/lagda/Base/Homomorphisms/Factor.lagda | Pragma update in literate docs. |
| doc/lagda/Base/Homomorphisms/HomomorphicImages.lagda | Pragma update in literate docs. |
| doc/lagda/Base/Homomorphisms/Isomorphisms.lagda | Pragma update in literate docs. |
| doc/lagda/Base/Homomorphisms/Kernels.lagda | Pragma update in literate docs. |
| doc/lagda/Base/Homomorphisms/Noether.lagda | Pragma update in literate docs. |
| doc/lagda/Base/Homomorphisms/Products.lagda | Pragma update in literate docs. |
| doc/lagda/Base/Homomorphisms/Properties.lagda | Pragma update in literate docs. |
| doc/lagda/Base/Relations.lagda | Pragma update in literate docs. |
| doc/lagda/Base/Relations/Continuous.lagda | Pragma update in literate docs. |
| doc/lagda/Base/Relations/Discrete.lagda | Pragma update in literate docs. |
| doc/lagda/Base/Relations/Properties.lagda | Pragma update in literate docs. |
| doc/lagda/Base/Relations/Quotients.lagda | Pragma update in literate docs. |
| doc/lagda/Base/Structures.lagda | Pragma update in literate docs. |
| doc/lagda/Base/Structures/Basic.lagda | Pragma update in literate docs. |
| doc/lagda/Base/Structures/Congruences.lagda | Pragma update in literate docs. |
| doc/lagda/Base/Structures/EquationalLogic.lagda | Pragma update in literate docs. |
| doc/lagda/Base/Structures/Graphs.lagda | Pragma update in literate docs. |
| doc/lagda/Base/Structures/Graphs0.lagda | Pragma update in literate docs. |
| doc/lagda/Base/Structures/Homs.lagda | Pragma update in literate docs. |
| doc/lagda/Base/Structures/Isos.lagda | Pragma update in literate docs. |
| doc/lagda/Base/Structures/Products.lagda | Pragma update in literate docs. |
| doc/lagda/Base/Structures/Sigma.lagda | Pragma update in literate docs. |
| doc/lagda/Base/Structures/Sigma/Basic.lagda | Pragma update in literate docs. |
| doc/lagda/Base/Structures/Sigma/Congruences.lagda | Pragma update in literate docs. |
| doc/lagda/Base/Structures/Sigma/Homs.lagda | Pragma update in literate docs. |
| doc/lagda/Base/Structures/Sigma/Isos.lagda | Pragma update in literate docs. |
| doc/lagda/Base/Structures/Sigma/Products.lagda | Pragma update in literate docs. |
| doc/lagda/Base/Structures/Substructures.lagda | Pragma update in literate docs. |
| doc/lagda/Base/Structures/Terms.lagda | Pragma update in literate docs. |
| doc/lagda/Base/Subalgebras.lagda | Pragma update in literate docs. |
| doc/lagda/Base/Subalgebras/Properties.lagda | Pragma update in literate docs. |
| doc/lagda/Base/Subalgebras/Subalgebras.lagda | Pragma update in literate docs. |
| doc/lagda/Base/Subalgebras/Subuniverses.lagda | Pragma update in literate docs. |
| doc/lagda/Base/Terms.lagda | Pragma update in literate docs. |
| doc/lagda/Base/Terms/Basic.lagda | Pragma update in literate docs. |
| doc/lagda/Base/Terms/Operations.lagda | Pragma update in literate docs. |
| doc/lagda/Base/Terms/Properties.lagda | Pragma update in literate docs. |
| doc/lagda/Base/Varieties.lagda | Pragma update in literate docs. |
| doc/lagda/Base/Varieties/Closure.lagda | Pragma update in literate docs. |
| doc/lagda/Base/Varieties/EquationalLogic.lagda | Pragma update in literate docs. |
| doc/lagda/Base/Varieties/FreeAlgebras.lagda | Pragma update in literate docs. |
| doc/lagda/Base/Varieties/Invariants.lagda | Pragma update in literate docs. |
| doc/lagda/Base/Varieties/Preservation.lagda | Pragma update in literate docs. |
| doc/lagda/Base/Varieties/Properties.lagda | Pragma update in literate docs. |
| doc/lagda/Setoid.lagda | Pragma update in literate docs. |
| doc/lagda/Setoid/Algebras.lagda | Pragma update in literate docs. |
| doc/lagda/Setoid/Algebras/Basic.lagda | Pragma update in literate docs. |
| doc/lagda/Setoid/Algebras/Congruences.lagda | Pragma update in literate docs. |
| doc/lagda/Setoid/Algebras/Products.lagda | Pragma update in literate docs. |
| doc/lagda/Setoid/Functions.lagda | Pragma update in literate docs. |
| doc/lagda/Setoid/Functions/Basic.lagda | Pragma update in literate docs. |
| doc/lagda/Setoid/Functions/Bijective.lagda | Pragma update in literate docs. |
| doc/lagda/Setoid/Functions/Injective.lagda | Pragma update in literate docs. |
| doc/lagda/Setoid/Functions/Inverses.lagda | Pragma update in literate docs. |
| doc/lagda/Setoid/Functions/Surjective.lagda | Pragma update in literate docs. |
| doc/lagda/Setoid/Homomorphisms.lagda | Pragma update in literate docs. |
| doc/lagda/Setoid/Homomorphisms/Basic.lagda | Pragma update in literate docs. |
| doc/lagda/Setoid/Homomorphisms/Factor.lagda | Pragma update in literate docs. |
| doc/lagda/Setoid/Homomorphisms/HomomorphicImages.lagda | Pragma update in literate docs. |
| doc/lagda/Setoid/Homomorphisms/Isomorphisms.lagda | Pragma update in literate docs. |
| doc/lagda/Setoid/Homomorphisms/Kernels.lagda | Pragma update in literate docs. |
| doc/lagda/Setoid/Homomorphisms/Noether.lagda | Pragma update in literate docs. |
| doc/lagda/Setoid/Homomorphisms/Products.lagda | Pragma update in literate docs. |
| doc/lagda/Setoid/Homomorphisms/Properties.lagda | Pragma update in literate docs. |
| doc/lagda/Setoid/Relations.lagda | Pragma update in literate docs. |
| doc/lagda/Setoid/Relations/Discrete.lagda | Pragma update in literate docs. |
| doc/lagda/Setoid/Relations/Quotients.lagda | Pragma update in literate docs. |
| doc/lagda/Setoid/Subalgebras.lagda | Pragma update in literate docs. |
| doc/lagda/Setoid/Subalgebras/Properties.lagda | Pragma update in literate docs. |
| doc/lagda/Setoid/Subalgebras/Subalgebras.lagda | Pragma update in literate docs. |
| doc/lagda/Setoid/Subalgebras/Subuniverses.lagda | Pragma update in literate docs. |
| doc/lagda/Setoid/Terms.lagda | Pragma update in literate docs. |
| doc/lagda/Setoid/Terms/Basic.lagda | Pragma update in literate docs. |
| doc/lagda/Setoid/Terms/Operations.lagda | Pragma update in literate docs. |
| doc/lagda/Setoid/Terms/Properties.lagda | Pragma update in literate docs. |
| doc/lagda/Setoid/Varieties.lagda | Pragma update in literate docs. |
| doc/lagda/Setoid/Varieties/Closure.lagda | Pragma update in literate docs. |
| doc/lagda/Setoid/Varieties/EquationalLogic.lagda | Pragma update in literate docs. |
| doc/lagda/Setoid/Varieties/FreeAlgebras.lagda | Pragma update in literate docs. |
| doc/lagda/Setoid/Varieties/HSP.lagda | Pragma update in literate docs. |
| doc/lagda/Setoid/Varieties/Preservation.lagda | Pragma update in literate docs. |
| doc/lagda/Setoid/Varieties/Properties.lagda | Pragma update in literate docs. |
| doc/lagda/Setoid/Varieties/SoundAndComplete.lagda | Pragma update in literate docs. |
| doc/lagda/Overture.lagda | Pragma update in literate docs. |
| doc/lagda/Overture/Operations.lagda | Pragma update in literate docs. |
| doc/lagda/Overture/Preface.lagda | Pragma update in literate docs. |
| doc/lagda/Overture/Signatures.lagda | Pragma update in literate docs. |
| doc/lagda/Exercises.lagda | Pragma update in literate docs. |
| doc/lagda/Exercises/Complexity.lagda | Pragma update in literate docs. |
| doc/lagda/Exercises/Complexity/FiniteCSP.lagda | Pragma update in literate docs. |
| doc/lagda/Examples.lagda | Pragma update in literate docs. |
| doc/lagda/Examples/Categories.lagda | Pragma update in literate docs. |
| doc/lagda/Examples/Categories/Functors.lagda | Pragma update in literate docs. |
| doc/lagda/Examples/Structures.lagda | Pragma update in literate docs. |
| doc/lagda/Examples/Structures/Basic.lagda | Pragma update in literate docs. |
| doc/lagda/Examples/Structures/Signatures.lagda | Pragma update in literate docs. |
| doc/lagda/Demos.lagda | Pragma update in literate docs. |
| doc/lagda/Demos/ContraX.lagda | Pragma update in literate docs. |
| doc/lagda/Demos/GeneralOperationsAndRelations.lagda | Pragma update in literate docs. |
| doc/lagda/Demos/HSP.lagda | Pragma update in literate docs. |
| nix/flake.nix | Remove older nested flake (replaced by root flake). |
| nix/default.nix | Remove legacy nix-shell definition (superseded by flake). |
| nix/README_NIXOS.md | Remove NixOS overlay usage doc (superseded by new flake docs). |
| flake.nix | Add root flake to pin Agda/stdlib and provide dev shell. |
| flake.lock | Update nixpkgs pin for the new flake. |
| agda-algebras.agda-lib | Pin stdlib dependency to 2.3 and add warning-suppression flags. |
| admin/generate-html | Update OPTIONS line in generated Everything module (script now diverges from current src layout). |
| doc/INSTALL_AGDA.md | Mark legacy install guide as deprecated. |
| INSTALL.md | Add canonical installation guide for Agda 2.8.0 + stdlib 2.3. |
| README.md | Refresh README for 2.0 line, Nix workflow, and requirements. |
| Makefile | Rewrite build targets for Everything.agda, check, html, and clean. |
| .gitignore | Expand/organize ignore patterns and add Nix + generated artifacts. |
Comments suppressed due to low confidence (1)
admin/generate-html:27
- admin/generate-html still assumes
src/contains.lagdamodules (itfinds*.lagdaand greps forsrc/...*.lagda), but the current source tree is.agda(andmake htmlusesEverything.agdagenerated from.agda). As written, this script will generate anEverything.agdawith no imports and won’t produce the expected outputs. Update it to scan*.agda(or explicitly deprecate/remove the script in favor of the Makefile).
## absolute module names with no src/ prefix and no .lagda suffix
CHOPMODS=$(find $SRCDIR -name "*.lagda" | sed -e 's|^src/[/]*||' -e 's|.lagda||')
## replace / with . in $CHOPMODS list of module names
DOTMODS=$(echo $CHOPMODS | sed -e 's|/|.|g')
echo " "
echo "STEP 1. Generating agda program Everything.agda which imports all modules..."
echo " "
echo "{-# OPTIONS --cubical-compatible --exact-split --safe #-}" > $SRCDIR/$TARGET.agda
echo " " >> $SRCDIR/$TARGET.agda
git ls-tree --full-tree -r --name-only HEAD | grep '^src/[^\.]*.lagda' | sed -e 's|^src/[/]*|import |' -e 's|/|.|g' -e 's/.lagda//' -e '/import Everything/d' | LC_COLLATE='C' sort >> $SRCDIR/$TARGET.agda
💡 Add Copilot custom instructions for smarter, more guided reviews. Learn how to get started.
**Structural changes**. - Add **M9 — Applications of continuous relations** as a new milestone with three issues (M9-1 Scott-continuous relations, M9-2 Infinitary CSP, M9-3 Coalgebraic bisimulation exploration). - Clarify M7's scope as **finite-template** CSP to cleanly separate from M9-2, with a cross-reference to M9-2 in M7-1. - Add `milestone-9-apps` label. - Update the top-level project description to mention nine milestones. - Update both Mermaid graphs (top and bottom) to include M9. - Extend the summary table with an M9 section. - Update totals: 27 → 30 issues, 8 → 9 milestones. **Style cleanup (applied throughout)**. - Two spaces after every sentence-ending period. - Every task bullet ends in a period. - `**Bold**:` and `**Bold**.` with punctuation outside bold. - Paragraphs on single lines (no artificial line breaks within a paragraph).
williamdemeo
changed the title
--without-K -> --cubical-compatible--without-K -> --cubical-compatible
`docs/` is the contemporary convention used by GitHub Pages, Sphinx, MkDocs, Docusaurus, and most modern software projects; `doc/` is associated with older GNU/Debian conventions. Rename preemptively so future M1-* documentation issues (STYLE.md, adr/, etc.) can land at the paths they already reference in doc/GITHUB_PROJECT.md. Update cross-references in README.md and [any Makefile / _config.yml entries you find with the grep above]. Part of #250 (M1-1).
The library is now primarily a software artifact rather than a literate mathematical exposition, so the previous CC-BY-SA-4.0 license (designed for content, with a viral copyleft clause that creates friction for anyone importing agda-algebras into a non-CC-BY-SA project) is no longer appropriate for the source tree. Adopt the dual-license pattern from agda-native-air: + LICENSE (Apache-2.0) covers source code under src/. + LICENSE-docs (CC BY 4.0) covers documentation, papers, and tutorials under docs/. Apache-2.0 is the industry-standard permissive software license, fully compatible with downstream use including commercial redistribution. CC BY 4.0 (not CC-BY-SA-4.0) removes the ShareAlike friction from the documentation side. Also flagged by Copilot's review of PR #278. Part of #250 (M1-1).
+ Replace the previous MIT badge (which misrepresented the actual CC-BY-SA-4.0 LICENSE file; flagged by Copilot) with two badges accurately reflecting the new dual-license layout. + Add badges for CI (workflow to land in #251, M1-2), Agda 2.8.0, and stdlib 2.3. + Add a Licensing section between Contributing and Credits that explains the dual-license split to contributors and downstream users. Part of #250 (M1-1).
williamdemeo
force-pushed
the
250-m1-1-upgrade-agda-and-stdlib-versions
branch
from
3a9ca3f to
a4c967e
Compare
williamdemeo
added a commit
that referenced
this pull request
Apr 20, 2026
The library is now primarily a software artifact rather than a literate mathematical exposition, so the previous CC-BY-SA-4.0 license (designed for content, with a viral copyleft clause that creates friction for anyone importing agda-algebras into a non-CC-BY-SA project) is no longer appropriate for the source tree. Adopt the dual-license pattern from agda-native-air: + LICENSE (Apache-2.0) covers source code under src/. + LICENSE-docs (CC BY 4.0) covers documentation, papers, and tutorials under docs/. Apache-2.0 is the industry-standard permissive software license, fully compatible with downstream use including commercial redistribution. CC BY 4.0 (not CC-BY-SA-4.0) removes the ShareAlike friction from the documentation side. Also flagged by Copilot's review of PR #278. Part of #250 (M1-1).
This was referenced Apr 20, 2026
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
Upgrades the agda-algebras library from its current target of Agda 2.6.2 / stdlib 1.7 to Agda 2.8.0 / stdlib 2.3, and replaces the deprecated
--without-Kpragma with--cubical-compatiblethroughout. Also lands Nix flake support at the repo top level sonix developprovides a reproducible build environment.
Closes #250 (issue M1-1 from the agda-algebras 2.0 project).
Status: WORK IN PROGRESS (draft)
--without-K→--cubical-compatible)agda-algebras.agda-libto the correct stdlib nameflake.nixto repo root and rewrite to pin Agda 2.8.0 / stdlib 2.3 viaagda.withPackagesFunction.Bundles.Func,Function.Bundles.Injection,Relation.Binary.*reorganization)README.mdfor 2.0 linedoc/INSTALL.mdas the canonical install guidedoc/INSTALL_AGDA.mddeprecateddoc/lagda/Overture/Basic.lagdaexplanation of--cubical-compatibleBlocking
This PR blocks essentially every other issue in the agda-algebras 2.0 project (M2-, M3-, etc.), per the dependency graph in
doc/GITHUB_PROJECT.md.Notes for reviewers
A note on
--cubical-compatiblevs--without-Kstdlib 2.3 uses
--cubical-compatible, which this PR matches. As @JacquesCarette points out, stdlib v3.0 is considering a revert to--without-K(agda/agda-stdlib#2967). The implications for agda-algebras — speed, and thesrc/Cubical/import firewall to agda-cubical — are tracked in [M1-4] (Issue #279) and will be evaluated once the upstream decision lands. No action for this PR.