Skip to content

release: v0.4.0 (EchoAggregation) #33

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Merged
hyperpolymath merged 2 commits into from
Oct 20, 2026
Merged

release: v0.4.0 (EchoAggregation) #33

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
2 commits
Select commit Hold shift + click to select a range
c7d7c7e
release: v0.4.0 (EchoAggregation)
claude Oct 20, 2026
c3b20f7
docs(wiki): describe v0.4.0 (Codex P2)
claude Oct 20, 2026
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
2 changes: 2 additions & 0 deletions CITATION.cff
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -23,3 +23,5 @@ keywords:
- "scientific-software"
- "typed-provenance"
- "veridical-computing"
version: 0.4.0
date-released: 2026-10-20
2 changes: 1 addition & 1 deletion Project.toml
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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"
Expand Down
12 changes: 6 additions & 6 deletions README.adoc
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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:
Expand Down Expand Up @@ -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
Expand Down Expand Up @@ -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+`,

@chatgpt-codex-connector chatgpt-codex-connector Bot Oct 20, 2026

Copy link
Copy Markdown

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

P2 Badge Update the canonical wiki for v0.4.0

Declaring v0.4.0 current leaves the repository's canonical wiki inconsistent with the release: wiki/Home.md still calls v0.3.0 the current pin and reports 15 modules, 19 testsets, and 258 assertions, while wiki/Exercises.md likewise identifies v0.3.0 as current. When wiki/*.md is published using the documented sync process, users will therefore see obsolete release and coverage information and no EchoAggregation entry; update those canonical wiki pages as part of this version bump.

Useful? React with 👍 / 👎.

`+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*
Expand Down
4 changes: 2 additions & 2 deletions src/EchoTypes.jl
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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.
Expand Down Expand Up @@ -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,
Expand Down
3 changes: 2 additions & 1 deletion wiki/Exercises.md
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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`.

---

Expand Down
13 changes: 8 additions & 5 deletions wiki/Home.md
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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)

Expand All @@ -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

Expand Down
Loading