From c7d7c7ee8c3ade9f5e016f543e49cafd6a155bd9 Mon Sep 17 00:00:00 2001 From: Claude Date: Tue, 20 Oct 2026 13:48:59 +0000 Subject: [PATCH 1/2] release: v0.4.0 (EchoAggregation) Bump Project.toml to 0.4.0 and record version and release date in CITATION.cff. v0.3.0 was never tagged on its own (Project.toml already said 0.3.0 but the tags stop at v0.2.0), so its content ships here together with EchoAggregation; the README now says so and no longer calls EchoAggregation unreleased. No code change. 302 of 302 assertions pass. The tag is the owner's to push. Co-Authored-By: Claude Sonnet 5.5 Claude-Session: https://claude.ai/code/session_01MF5GeeBBDF6sUzr6pZTjWV --- CITATION.cff | 2 ++ Project.toml | 2 +- README.adoc | 12 ++++++------ src/EchoTypes.jl | 4 ++-- 4 files changed, 11 insertions(+), 9 deletions(-) diff --git a/CITATION.cff b/CITATION.cff index cf0ab67..11e9b35 100644 --- a/CITATION.cff +++ b/CITATION.cff @@ -23,3 +23,5 @@ keywords: - "scientific-software" - "typed-provenance" - "veridical-computing" +version: 0.4.0 +date-released: 2026-10-20 diff --git a/Project.toml b/Project.toml index f9ceb0d..1fd81cc 100644 --- a/Project.toml +++ b/Project.toml @@ -6,7 +6,7 @@ name = "EchoTypes" uuid = "a8ca608b-856a-4215-8c3d-f9ffd1705524" authors = ["Jonathan D.A. Jewell <6759885+hyperpolymath@users.noreply.github.com>"] -version = "0.3.0" +version = "0.4.0" [compat] julia = "1.10" diff --git a/README.adoc b/README.adoc index cd518c4..5ef5635 100644 --- a/README.adoc +++ b/README.adoc @@ -64,7 +64,7 @@ The Agda. This release mirrors `+hyperpolymath/echo-types+` at (2026-05-28 head, after the Tier-3 audience-facing spine landed — EchoProvenance, EchoSecurity, EchoProbabilisticSupport, EchoDifferential, EchoLLEncoding, plus the EchoCanonicalIdentitySuite -re-export bundle). The unreleased `+EchoAggregation+` entry below is +re-export bundle). The `+EchoAggregation+` entry below (new in v0.4.0) is mirrored from a later commit, `+703dd77af402e959b46f49e8ce2e084521bedbae+`; every other row keeps the pin above: @@ -139,7 +139,7 @@ audience move 4 — blur loses perturbation tag) `+source_no_section_holds+`, `+gap_paired+` |`+EchoLLEncoding.agda+` (cementing-negative — the LL `+!A := 1+` shadow admits an encoded section paired with source-side no-section) -|*unreleased* `+Monoid+`, `+GroupAggregator+`, `+oplus_fold+`, +|*v0.4.0* `+Monoid+`, `+GroupAggregator+`, `+oplus_fold+`, `+aggregate_values+`, `+aggregation_as_fold_holds+`, `+sum_monoid+` / `+count_monoid+` / `+max_monoid+` / `+min_monoid+`, `+no_canonical_disaggregation_of+`, `+pair_sum+` and its @@ -237,16 +237,16 @@ green and is the only correctness claim this package makes about itself. === Status -`+v0.3.0+`, local development. The v0.1.0 surface (`+Echo+`, +`+v0.4.0+`. The v0.1.0 surface (`+Echo+`, `+EchoResidue+`, `+EchoFiberCount+`, `+EchoThermodynamics+`) and the v0.2.0 Tier-1+Tier-2 canonical-identity spine are preserved unchanged; v0.3.0 adds executable shadows of the Tier-3 audience-facing spine that landed upstream on 2026-05-27/28 (`+EchoProvenance+`, `+EchoSecurity+`, `+EchoProbabilisticSupport+`, `+EchoDifferential+`) plus the cementing-negative `+EchoLLEncoding+` (LL shallow-encoding gap with -paired source-side no-section). Unreleased on top of v0.3.0: -`+EchoAggregation+` (mirrored from echo-types `+703dd77+`, not from -`+eed4250+`). Test suite: +paired source-side no-section). v0.3.0 was never tagged on its own; its +content ships in v0.4.0, which adds `+EchoAggregation+` (mirrored from +echo-types `+703dd77+`, not from `+eed4250+`). Test suite: *302 passing assertions across 21 testsets*, organised as finite shadows of named Agda lemmas plus the semantic-fibre vocabulary exercise over the kernel. Registered as `+EchoTypes+` in the hyperpolymath professional registry; *not* diff --git a/src/EchoTypes.jl b/src/EchoTypes.jl index 4b6cacc..600a1a9 100644 --- a/src/EchoTypes.jl +++ b/src/EchoTypes.jl @@ -24,7 +24,7 @@ # worked instance`) + cementing-negative EchoLLEncoding (the # trivial-⊤-shadow LL gap with paired source-side no-section). # -# Unreleased on top of v0.3.0: EchoAggregation (general monoid/group +# v0.4.0 adds EchoAggregation (general monoid/group # aggregation, echo-types#175), mirrored from echo-types origin/main # @ 703dd77af402e959b46f49e8ce2e084521bedbae. The rest of this header's # provenance pin is unchanged. @@ -94,7 +94,7 @@ export EchoWitness, echo_intro, in_fiber, fiber, LLShallowEncoding, trivial_encoding, trivial_encoding_has_section, ll_encoding_gap, source_no_section_holds, gap_paired, - # EchoAggregation (unreleased; general monoid/group form, echo-types#175) + # EchoAggregation (v0.4.0; general monoid/group form, echo-types#175) Monoid, GroupAggregator, monoid_laws_hold, oplus_fold, oplus_fold_append_holds, aggregate_values, aggregation_as_fold_holds, From c3b20f77ebae90e3e62af73e121a84137bc869c8 Mon Sep 17 00:00:00 2001 From: Claude Date: Tue, 20 Oct 2026 13:57:38 +0000 Subject: [PATCH 2/2] docs(wiki): describe v0.4.0 (Codex P2) wiki/Home.md and wiki/Exercises.md still called v0.3.0 the current pin and reported 15 modules, 19 testsets and 258 assertions. They now name v0.4.0, add the EchoAggregation row, and report 16 modules, 21 testsets and 302 assertions, with the two source-of-truth pins (eed4250 and 703dd77). Co-Authored-By: Claude Sonnet 5.5 Claude-Session: https://claude.ai/code/session_01MF5GeeBBDF6sUzr6pZTjWV --- wiki/Exercises.md | 3 ++- wiki/Home.md | 13 ++++++++----- 2 files changed, 10 insertions(+), 6 deletions(-) diff --git a/wiki/Exercises.md b/wiki/Exercises.md index 2df2528..78797b2 100644 --- a/wiki/Exercises.md +++ b/wiki/Exercises.md @@ -33,7 +33,8 @@ julia> using EchoTypes ``` The package is **not** in Julia's General registry. It carries its -own SoT pin tying v0.3.0 to echo-types `eed4250` (2026-05-28). +own SoT pin tying v0.4.0 to echo-types `eed4250` (2026-05-28), except +`EchoAggregation`, which is pinned to `703dd77`. --- diff --git a/wiki/Home.md b/wiki/Home.md index 86adc59..9c93ee8 100644 --- a/wiki/Home.md +++ b/wiki/Home.md @@ -51,10 +51,12 @@ Agda repo remains the formal source of truth. ## Current pin -`v0.3.0` mirrors echo-types `origin/main` at -`eed42503a1a4c54ec0a347ebef3440b4d4db30c9` (2026-05-28). The -package's preamble carries the SoT pin; re-pin a fresh clone if -you want to track HEAD. +`v0.4.0` mirrors echo-types `origin/main` at +`eed42503a1a4c54ec0a347ebef3440b4d4db30c9` (2026-05-28) for every +module except `EchoAggregation`, which is mirrored from +`703dd77af402e959b46f49e8ce2e084521bedbae`. The package's preamble +carries the SoT pin; re-pin a fresh clone if you want to track HEAD. +(`v0.3.0` was never tagged on its own; its content ships in v0.4.0.) ## Coverage map (one-line summary) @@ -63,7 +65,8 @@ you want to track HEAD. | Foundation (v0.1.0) | Echo / EchoResidue / EchoFiberCount / EchoThermodynamics | 7 | | Canonical identity (v0.2.0) | TotalCompletion / OFS / Image / NoSectionGeneric / LossTaxonomy / Entropy / ObsEquivalence | 7 | | Audience-facing + LL gap (v0.3.0) | Provenance / Security / ProbabilisticSupport / Differential / LLEncoding | 5 | -| **Total** | **15 Agda modules + semantic-fibre vocabulary exercise** | **19 testsets, 258 passing assertions** | +| Aggregation (v0.4.0) | Aggregation (monoid fold, homomorphism law, no-canonical-disaggregation, `pairSum` instance) | 2 | +| **Total** | **16 Agda modules + semantic-fibre vocabulary exercise** | **21 testsets, 302 passing assertions** | ## Intentionally NOT mirrored