Arena/01a0db23 metamanifold webui - #87
Merged
Merged
Conversation
Pilot ruling of 2026-09-26 (owner): this repository is the pilot for migrating the estate's YAML to KYAML, the strict YAML subset of KEP-5295. Authority is hyperpolymath/standards 3-practice/YAML-POLICY.adoc rules Y-2 and Y-3. - scripts/kyaml/KYAML.jl: the switch. --to-kyaml, --to-yaml, --check and --report; comments keep their association; canonical-form checking makes the gate idempotent by construction; a refusal names the file and line and writes nothing, so a tree is never half-converted. - config/kyaml/drift.txt: the two workflow files Dependabot and gh actions-lock rewrite. Converted, not gated, accepted in writing (policy §5 step 6). - Justfile: use-kyaml, use-yaml, check-kyaml (wired into hygiene and ci), kyaml-report, and prove-agda, which fails loudly when no Agda is on PATH. - docs/pilots/kyaml-pilot.md: the operating manual — the ruling, what the switch guarantees, what it refuses by name, the decisions it takes and prints, the proof-obligation table, how to revert, and what is deliberately out of scope. - test/unit/test_kyaml.jl: comment association, idempotence, YAML round trip, block scalars, the forced decisions, six refusals, a dropped-comment mutant that must turn the gate red, and every tracked YAML file parsed and re-emitted. - EXPLAINME.adoc: the language ruling (Julia for everything we can; the dada2 pipeline stays as it is; the TypeScript view is a plan, not a task) and the KYAML pilot pointer. - proofs/agda/README.md: how to run the proofs, what each proves, what is deliberately not proved, and what would falsify them. *.agdai ignored. Not in this commit: the conversion itself (next), the shell extraction out of ci.yml into scripts/ci/*.sh, the CI step for check-kyaml, and the Agda CI job. Co-authored-by: arena-agent <297053741+arena-agent@users.noreply.github.com>
…ort (issue #21) Zero handling, implemented rather than aliased, and proved where it can be proved. Operators (src/analysis/zero_replacement.jl): - multiplicative replacement (Martin-Fernandez et al. 2003), the operator of zCompositions::multRepl: zeros get delta x per-part detection limit, observed parts scale by 1 - Delta, and the sample total and the ratios among observed parts are preserved exactly. - Bayesian multiplicative replacement (Martin-Fernandez et al. 2015), the GBM of cmultRepl: posterior mean of a Dirichlet-multinomial with the leave-one-out prior mean and concentration 1/gmean(t) unless alpha is supplied, with the reference's frac x colmins cap and its adjust switch. - Both refuse by name what they cannot do, record per-sample diagnostics, and carry the provenance sentence the issue asks for: all replacement is biased. Dispersion (src/analysis/dispersion.jl): - pure-Julia port of glmGamPoi (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: true is refused, null is refused at or above 100 features, false runs the reference's own non-trended prior and records the deviation. No silent substitution. - estimation.jl: the by-name refusal becomes the real two-pass path (mean sweep in R, dispersions in Julia, refit at fixed dispersion; theta = 1/alpha, with stats::glm(poisson()) where alpha is 0). Configuration and surface: 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; delta in (0,1) and alpha > 0 validated at the door; warnings below 0.01 and at or above 0.9; a DEED echo of every value; the DANGER banner when three or more deltas have been tried. 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): totals and ratios preserved, imputed values positive and below their detection limit; no data-determined rule can be faithful (the fibre behind "every replacement is biased"); the shrinkage lies between the prior and the sample estimate. proofs/agda/README.md states what is not proved and what would falsify each file. Tests and benchmarks: - test/unit/test_zero_replacement.jl and test_dispersion.jl against test/fixtures/issue21/golden.json, with direct comparisons against zCompositions and glmGamPoi wherever R has them and an explicit "this comparison did not run" where it does not; - bench/zero_replacement/benchmark.jl at 100/1000/10000 taxa with the issue's 5-minute warning and the 10% regression report behind METAMANIFOLD_BENCH_STRICT (the repository's later decision made the other Julia benches informational; the reasoning and the switch are recorded in the file header). KYAML pilot follow-ups in the same change: the KYAML tool now preserves comments that sit above the document root instead of dropping them (every file here starts with an SPDX header, so a silent drop would have deleted licence headers); guix.scm gains the agda + agda-stdlib lane; stapeln.toml and Containerfile define the standalone toolchain deployment (owner ruling: standalone, not local-only); the review bench lane is added to the existing Julia benchmark step. The three new Agda modules are flat, standalone-checked files: folding them into the existing MetaManifold/ suite (module namespace, the suite OPTIONS header, All.agda, a guard run) is the follow-up, and doing it blind would have risked a passing lane. Docs: docs/statistics/zero-handling.md, docs/statistics/method-conditions/dispersion-glmGamPoi.md, CHANGELOG, ROADMAP. Not in this commit: the KYAML conversion itself (one command, where Julia is), the shell extraction from ci.yml into scripts/ci/*.sh, and the first CI run of any of it - the sandbox has no Julia or R, so every number here is unexecuted locally and the first CI run is the debugger. Co-authored-by: arena-agent <297053741+arena-agent@users.noreply.github.com>
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
Base check
hyperpolymath/MetaManifold-WebUI:main(not the upstreamparent; application changes go to
JoshuaJewell/MetaManifold-WebUI)Changes
Engineering checklist
Required
bun run checkpasses (frontend/: typecheck 0 errors, tests,benchmarks)
scripts/check-spdx.sh/check-format.sh/check-lint.shpass(advisory in CI — does not block merge)
CONTRIBUTING.md; advisory in CI)NOTICEexplainsthe authorship rule)
.env, or sequencing data includedAs applicable
CHANGELOG.mdupdated for user/developer-visible changesdocs/types/architecture.mdupdated if type boundaries moveddocs/testing/coverage.mdupdated if test coverage moveddocs/reproducibility.mdupdated if environment requirements changedTesting