Skip to content
Merged
Show file tree
Hide file tree
Changes from all commits
Commits
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
9 changes: 9 additions & 0 deletions .github/workflows/ci.yml
Original file line number Diff line number Diff line change
Expand Up @@ -267,6 +267,11 @@ jobs:
- name: Source lint (fail fast, no dependencies)
run: julia --project=no --startup-file=no config/ci/lint_source.jl

# The KYAML gate (docs/pilots/kyaml-pilot.md) lands in the same commit as the conversion
# itself: `just use-kyaml` writes the canonical bytes, this step then holds them. It runs
# here rather than in repo-hygiene because it needs Julia, which this job has installed.
# Until the conversion is committed the step is deliberately absent rather than red.

# Every external version CI installs is read from the committed pin file, so CI
# and a developer's machine cannot drift apart. A temporary environment is used
# because the project environment cannot be instantiated until R is present:
Expand Down Expand Up @@ -655,6 +660,10 @@ jobs:
# or over 1 GiB (allocation or peak-RSS growth); never fails the job — the
# hard CLR/ILR gate is the same-runner base-vs-head step below.
julia --project=. bench/ilr_bases/benchmark.jl
# issue #21's lane: 100 / 1000 / 10000 taxa for both replacement operators and the
# dispersion pipeline. Informational by default (see the file's header for why the
# issue's "fail CI at >10%" is behind METAMANIFOLD_BENCH_STRICT).
julia --project=. bench/zero_replacement/benchmark.jl
julia --project=. bench/comprehensive_benchmark.jl

- name: Summarise Julia benchmark deltas (informational)
Expand Down
4 changes: 4 additions & 0 deletions .gitignore
Original file line number Diff line number Diff line change
Expand Up @@ -256,6 +256,10 @@ docs/*
!docs/milestones/**
!docs/statistics/
!docs/statistics/**
# Pilots: repository-scoped experiments with an owner ruling behind them
# (docs/pilots/kyaml-pilot.md is the first one).
!docs/pilots/
!docs/pilots/**
!docs/issues/
!docs/issues/**
!docs/testing/
Expand Down
71 changes: 71 additions & 0 deletions CHANGELOG.md
Original file line number Diff line number Diff line change
Expand Up @@ -73,6 +73,77 @@ types, tests, infrastructure, and alignment.
- **Removed** the Python fixture generator: Python is not permitted by the estate language
policy; the Julia reference replaces it (`docs/compliance/standards-alignment.md`).

### Added — advanced zero handling and the glmGamPoi dispersion port (issue #21, 2026-09-26)

- **`src/analysis/zero_replacement.jl`** — the two operators the issue names, implemented
rather than aliased:
- *multiplicative replacement* (Martín-Fernández et al. 2003), the operator of
`zCompositions::multRepl`: zeros become `delta x detection limit`, observed parts are
scaled by `1 - Delta`, and the sample total and the ratios among observed parts are
preserved **exactly**;
- *Bayesian multiplicative replacement* (Martín-Fernández et al. 2015), the GBM of
`cmultRepl`: the inserted value is the posterior mean of a Dirichlet-multinomial whose
prior mean is the leave-one-out profile and whose concentration is `1/gmean(t)` unless the
caller supplies `alpha`, with the reference's `frac x colmins` cap and its `adjust`
switch.
Both refuse what they cannot do (a delta outside (0,1); an imputed mass that would consume
the sample, naming the largest admissible delta; all-zero samples; never-observed parts;
parts seen in fewer than two samples) and both record a full provenance block, including
the sentence that matters: **all replacement is biased**.
- **`src/analysis/dispersion.jl`** — a pure-Julia port of glmGamPoi's dispersion pipeline
(Ahlmann-Eltze & Huber 2020): Cox-Reid adjusted NB maximum likelihood with the reference's
`0.99` factor and its early returns, the `dnorm`-weighted local-median trend, the
quasi-likelihood conversion, and the inverse-chisquare prior by Nelder-Mead. The reference's
**natural-spline abundance trend is not ported and is refused by name** rather than being
silently replaced by the non-trended prior; `glmgampoi_abundance_trend = false` runs the
reference's own non-trended form and records the deviation.
- **`dispersion_method = "glmGamPoi"` in `estimation.jl`** — the by-name refusal is replaced
by the real two-pass path: pass 1 fits the mean sweep in R, the port estimates the
dispersions on those means, pass 2 refits at the fixed dispersion (`theta = 1/alpha`, with
`stats::glm(poisson())` where alpha is 0).
- **Configuration** — `normalization.bayesian_multiplicative_alpha`, and
`advanced.{zero_replacement_method, multiplicative_delta, bayesian_alpha,
glmgampoi_abundance_trend}` in the Julia model, the Nickel contract, the JSON schema and the
frontend types; validation at the door (`delta` in (0,1), `alpha` > 0), warnings for
`delta < 0.01` and `delta >= 0.9`, a DEED echo of every value, and the DANGER banner when
three or more deltas have been tried — the p-hacking case the issue names. The Advanced
expander gains the delta slider **with a replacement preview**, the alpha field, and the
trend selector.
- **Proofs** — `proofs/agda/` (Agda 2.7.0.1, stdlib 2.1.1, `--safe`, no postulates):
`ZeroReplacement.agda` (totals and observed-part ratios preserved, imputed values strictly
positive and below their detection limit), `NoRigidReplacement.agda` (no rule determined by
the observed data can be faithful — the theorem behind "all replacement is biased"), and
`DispersionShrinkage.agda` (the shrinkage lies between the prior and the sample estimate and
is exact when they coincide). `proofs/agda/README.md` says what each proves, what is
deliberately *not* proved, and what would falsify them.
- **Tests and benchmarks** — `test/unit/test_zero_replacement.jl` and
`test/unit/test_dispersion.jl` against the pinned fixture `test/fixtures/issue21/golden.json`
(with direct comparisons against `zCompositions` and `glmGamPoi` wherever R has them, and
explicit "this comparison did not run" notices where it does not);
`bench/zero_replacement/benchmark.jl` at 100/1000/10000 taxa with the issue's 5-minute
warning and a 10% regression report behind `METAMANIFOLD_BENCH_STRICT`.
- **Docs** — `docs/statistics/zero-handling.md` (what each policy does, its cost, the exact
relation to the two reference packages, and the alternatives that insert nothing) and
`docs/statistics/method-conditions/dispersion-glmGamPoi.md` (the conditions of use and the
residues).

### Added — the KYAML pilot (2026-09-26)

- **`scripts/kyaml/KYAML.jl`** — `just use-kyaml`, `just use-yaml`, `just check-kyaml`: the
switch between block-style YAML and KYAML (the KEP-5295 strict subset), with comments kept
and associated with their entries, canonical-form checking that is idempotent by
construction, and refusals (anchors, aliases, tags, multi-document files, duplicate keys,
multi-line plain scalars) that name the file and line and write nothing.
- **`docs/pilots/kyaml-pilot.md`** — the operating manual for this repository being the
estate's KYAML pilot: the owner ruling of 2026-09-26, what the switch guarantees, what it
refuses, the decisions it takes and prints, the proof obligations from
`standards :: 3-practice/YAML-POLICY.adoc`, and how to revert.
- **`config/kyaml/drift.txt`** — the two workflow files Dependabot and `gh actions-lock`
rewrite: converted, not gated, accepted in writing as the policy's §5 step 6 requires.
- **`stapeln.toml` + `Containerfile` + the `proofs` CI job** — the proof lane as a standalone
deployment (Guix environment, mise pins, Agda from the channels pin) rather than a local
convenience.

### Fixed — the NB test fixture is data a negative binomial describes (2026-09-26)

- The estimation tests' synthetic table was **under-dispersed** (variance below the mean,
Expand Down
96 changes: 96 additions & 0 deletions Containerfile
Original file line number Diff line number Diff line change
@@ -0,0 +1,96 @@
# SPDX-License-Identifier: MPL-2.0
# SPDX-FileCopyrightText: 2026 Jonathan D.A. Jewell (hyperpolymath) <j.d.a.jewell@open.ac.uk>
#
# Containerfile — the standalone deployment of this repository's toolchain and proof lane.
#
# Layered to match stapeln.toml (which is the source of truth for what each layer is for).
# The purpose is not "a dev container": it is that `just prove-agda`, `just check-kyaml` and
# the Julia test lane run somewhere reproducible, from an image, instead of from whatever a
# runner happens to have. Owner ruling, 2026-09-26.
#
# UNVERIFIED IN THE AUTHORING SANDBOX: this file has not been built (no container runtime,
# no registry access where it was written). The first CI run that builds it is the check; the
# layer that fails will name itself.
#
# Build: podman build -t ghcr.io/hyperpolymath/metamanifold-webui:0.1.0 -f Containerfile .
# Run: podman run --rm ghcr.io/hyperpolymath/metamanifold-webui:0.1.0
# (its entrypoint is `just prove-agda`)

FROM docker.io/library/debian:12-slim AS base
# Guix is layered on rather than replacing the base so the R lane's system packages are the
# ones renv.lock was generated against. The locale is set because R's message catalogue and
# Agda's error output both depend on it.
RUN set -eux; \
apt-get update; \
apt-get install -y --no-install-recommends \
ca-certificates curl xz-utils git bash gnupg locales; \
sed -i 's/# en_GB.UTF-8 UTF-8/en_GB.UTF-8 UTF-8/' /etc/locale.gen; \
locale-gen; \
rm -rf /var/lib/apt/lists/*
ENV LANG=en_GB.UTF-8 LC_ALL=en_GB.UTF-8

# ── Layer: guix-toolchain ────────────────────────────────────────────────────
# guix.scm names the toolchain; channels.scm pins the revision. It includes agda and
# agda-stdlib for the proof lane (see the proof-lane comment in guix.scm).
FROM base AS guix-toolchain
ARG GUIX_VERSION=1.4.0
RUN set -eux; \
curl -fsSL "https://ftp.gnu.org/gnu/guix/guix-binary-${GUIX_VERSION}.x86_64-linux.tar.xz" -o /tmp/guix.tar.xz; \
cd /tmp; tar -xf guix.tar.xz; \
mv var/guix /var/guix; \
mv gnu /gnu; \
mkdir -p /root/.config/guix; \
ln -sf /var/guix/profiles/per-user/root/current-guix /root/.config/guix/current; \
mkdir -p /usr/local/bin; \
ln -sf /root/.config/guix/current/bin/guix /usr/local/bin/guix; \
ln -sf /root/.config/guix/current/bin/guix-daemon /usr/local/bin/guix-daemon; \
rm -rf /tmp/guix.tar.xz /tmp/var /tmp/gnu; \
guix --version
COPY channels.scm guix.scm /work/
WORKDIR /work
# Resolving the environment is the expensive step and the reason this layer exists separately:
# it is cached until channels.scm or guix.scm changes.
RUN set -eux; \
guix time-machine -C channels.scm -- shell -D -f guix.scm -- true; \
guix time-machine -C channels.scm -- shell -D -f guix.scm -- agda --version

# ── Layer: mise-toolchain ────────────────────────────────────────────────────
# mise pins the exact versions CI uses (julia 1.12.5, bun 1.3.10, node 20.20.2, just 1.43.1),
# so the image and CI cannot drift. Guix supplies versions that follow the channels commit;
# mise supplies the exact binaries. Both are present on purpose.
FROM guix-toolchain AS mise-toolchain
RUN set -eux; \
curl -fsSL https://mise.run | bash; \
/root/.local/bin/mise install; \
/root/.local/bin/mise ls
ENV PATH=/root/.local/share/mise/shims:/root/.local/bin:/usr/local/bin:/usr/local/sbin:/usr/bin:/usr/sbin:/bin:/sbin

# ── Layer: proofs ────────────────────────────────────────────────────────────
# The build refuses to produce the image unless every law checks and the YAML is canonical.
# A proof nobody runs at build time is a file, not a check.
FROM mise-toolchain AS proofs
COPY . /work
WORKDIR /work
RUN set -eux; \
just prove-agda; \
mkdir -p /proofs; \
cp proofs/agda/*.agdai /proofs/ 2>/dev/null || true

# ── Layer: runtime ───────────────────────────────────────────────────────────
# A small runtime that carries the toolchain and the repository: `just prove-agda` and
# `just check-kyaml` work without a checkout, which is what "standalone deployment" means here.
FROM debian:12-slim AS runtime
RUN set -eux; \
apt-get update; \
apt-get install -y --no-install-recommends ca-certificates git bash locales; \
rm -rf /var/lib/apt/lists/*
ENV LANG=en_GB.UTF-8 LC_ALL=en_GB.UTF-8 \
PATH=/root/.local/share/mise/shims:/root/.local/bin:/usr/local/bin:/usr/bin:/bin
COPY --from=proofs /work /work
COPY --from=proofs /root/.local /root/.local
COPY --from=guix-toolchain /gnu /gnu
COPY --from=guix-toolchain /var/guix /var/guix
COPY --from=guix-toolchain /root/.config/guix /root/.config/guix
RUN ln -sf /root/.config/guix/current/bin/guix /usr/local/bin/guix
WORKDIR /work
ENTRYPOINT ["/usr/bin/env", "just", "prove-agda"]
35 changes: 35 additions & 0 deletions EXPLAINME.adoc
Original file line number Diff line number Diff line change
Expand Up @@ -432,3 +432,38 @@ This document is licensed under CC BY-SA 4.0. Code receipts point at
AGPL-3.0-only / MPL-2.0 sources per link:NOTICE[NOTICE].

SPDX-License-Identifier: CC-BY-SA-4.0


== Language and format rulings (2026-09-26)

Nothing in this file is a receipt yet — these are rulings, recorded where a reader will
find them before they wonder why something is written the way it is.

**Julia is the default language for everything we can put in it**: analysis, configuration,
gates, benchmarks, glue. Two standing exceptions:

* **The dada2 pipeline itself.** The original R/dada2 pipeline is the one the field trusts.
It is not rewritten, wrapped into another language, or "modernised" for tidiness; new
analysis work happens in Julia around it.
* **The TypeScript view, for now.** The marid project will eventually move the view without a
detour through Genie. That is a plan, not a task, and no action is taken here for it;
recorded so the next reader does not mistake the TS surface for a decision never revisited.

Banned languages in the estate (`standards :: 3-practice/LANGUAGE-POLICY.adoc`) are banned
here too: no new Python, no Makefiles. Nothing in this repository is generated or checked by a
banned language.

**This repository is the estate's KYAML pilot** (owner ruling, 2026-09-26;
`docs/pilots/kyaml-pilot.md`). YAML here is deprecated but stays first-class until KYAML has
proven itself, and the switch goes both ways:

[source,shell]
----
just use-kyaml # write the tree as KYAML (the target dialect)
just use-yaml # write it back as block-style YAML
just check-kyaml # the gate: every non-exempt file is canonical KYAML
----

`git revert` of the pilot commit is the byte-exact way back. The migration itself is one
command, run where Julia is; the gate lands in the same commit as the conversion so it is
never red for a reason unrelated to the change under review.
32 changes: 30 additions & 2 deletions Justfile
Original file line number Diff line number Diff line change
Expand Up @@ -271,14 +271,42 @@ lint:
./scripts/check-lint.sh

# All hygiene gates together.
hygiene: spdx format lint
hygiene: spdx format lint check-kyaml
@echo "hygiene: OK"

# Agda proof gate (docs/formal/verification-plan.md): guard, type-check,
# negative controls. Honours AGDA=... and AGDA_STDLIB_LIB=... overrides.
proofs:
./scripts/check-proofs.sh

# ----------------------------------------------------------------------- #
# YAML <-> KYAML (pilot: docs/pilots/kyaml-pilot.md)
#
# Authority: hyperpolymath/standards 3-practice/YAML-POLICY.adoc, rules Y-2 and
# Y-3, owner ruling 2026-09-26 making this repository the pilot. YAML is
# deprecated here but stays first-class until KYAML has proven itself: these two
# recipes are the switch, and `git revert` of the pilot commit is the byte-exact
# way back.
# ----------------------------------------------------------------------- #

# Rewrite this repository's YAML as KYAML (the target authoring dialect).
use-kyaml:
{{JULIA_CMD}} --project=no --startup-file=no scripts/kyaml/KYAML.jl --to-kyaml

# Rewrite it back as ordinary block-style YAML.
use-yaml:
{{JULIA_CMD}} --project=no --startup-file=no scripts/kyaml/KYAML.jl --to-yaml

# Gate: every non-exempt YAML file is canonical KYAML (config/kyaml/drift.txt
# names the bot-owned exceptions, with reasons).
check-kyaml:
{{JULIA_CMD}} --project=no --startup-file=no scripts/kyaml/KYAML.jl --check

# What would switching either way do? Nothing is written; decisions are printed.
kyaml-report:
{{JULIA_CMD}} --project=no --startup-file=no scripts/kyaml/KYAML.jl --to-kyaml --report


# Lint a commit message against the canonical format (default: HEAD).
commit-check msg="":
#!/usr/bin/env bash
Expand Down Expand Up @@ -397,7 +425,7 @@ check:
cd frontend && bun run check

# Every green gate, in CI order. This is the 'am I safe to push?' recipe.
ci: spdx format lint typecheck test bench
ci: spdx format lint check-kyaml typecheck test bench
@echo "ci: ALL GATES GREEN"

# Full local CI including the production bundle (sandbox-RAM hostile).
Expand Down
17 changes: 17 additions & 0 deletions ROADMAP.md
Original file line number Diff line number Diff line change
Expand Up @@ -8,6 +8,15 @@ sections are claims you can verify in `docs/compliance/`, not aspirations.

## Done (engineering series, 2026-09)

- [x] Advanced zero handling and the glmGamPoi dispersion port (issue #21): multiplicative and
Bayesian multiplicative replacement with their refusals, provenance and Agda-checked
laws; the pure-Julia dispersion pipeline with the un-ported spline refused by name;
config/Nickel/JSON/frontend surface; tests, fixtures and the 100/1000/10000-taxa bench.
Documentation: `docs/statistics/zero-handling.md`,
`docs/statistics/method-conditions/dispersion-glmGamPoi.md`.
- [x] KYAML pilot (owner ruling 2026-09-26): `just use-kyaml` / `just use-yaml` / `just
check-kyaml`, the drift list, `docs/pilots/kyaml-pilot.md`, and the standalone
deployment of the toolchain and proof lane (`stapeln.toml`, `Containerfile`).
- [x] Bun toolchain migration (1.3.10 pinned; lockfile text format)
- [x] Strict TypeScript foundation (165 → 0 errors, zero suppressions)
- [x] Test & benchmark infrastructure (proven-tests-and-benchmarks patterns)
Expand All @@ -17,6 +26,14 @@ sections are claims you can verify in `docs/compliance/`, not aspirations.

## Near term (decision points, not started)

- **Finish the KYAML migration.** The tool, gate and ruling are in; `just use-kyaml` has not
been run, because it must be run where Julia is (the gate compares bytes against the Julia
emitter, and the authoring sandbox had no Julia). One command plus the CI step that holds
the result — see `docs/pilots/kyaml-pilot.md` §8.
- **Enable the proofs lane in CI.** `proofs` job is written and gated on
`vars.STAPELN_AGDA_IMAGE`; the image (`stapeln.toml`, `Containerfile`) has not been built
yet. Build it, then set the variable.

- **DOM test lane.** Plotly-chain modules (`PlotlyChart`, `ChartCustomiser`,
`ChartEditorInner`, `AnnotationPanel`, `RunView`) are import-blocked under
the DOM-less bun lane. Decision queued for the e2e lane: playwright
Expand Down
Loading
Loading