proofs(agda): PERMANOVA's p-value floor and which terms are withheld

CONTRIBUTING.md → .github/CONTRIBUTING.md

@@ -98,7 +98,7 @@ A pull request does not reopen these. An issue can discuss them.
 
 - `config/defaults/tool_versions.yml` pins Julia, R, bun and the external tools,
   and `install.jl` and CI both install from it. The Julia version is repeated in
-  the CI matrix. Change a pin by editing that file, and expect the change to be
+  the CI workflow. Change a pin by editing that file, and expect the change to be
   discussed.
 - R packages are pinned in `renv.lock`.
 - CI job names carry no version numbers, so that a pin change leaves required

.github/dependabot.yml

@@ -0,0 +1,53 @@
+# Dependabot version updates. Until this file landed, only security updates
+# ran (those need no configuration), and those failed for a separate reason:
+# the "Dependabot Updates" runs of 2026-09-26..27 tried to fix alerts against
+# fixtures under test/doi using the npm_and_yarn updater, which refuses a
+# Bun-managed project ("bun.lock but no package-lock.json"). Those fixtures
+# have since left the repository and both alerts are fixed.
+#
+# What cannot be covered here: Julia (Project.toml / Manifest.toml) and R
+# (renv.lock) are not Dependabot package-ecosystems. Their pins live in
+# config/defaults/tool_versions.yml and are asserted by
+# test/unit/test_install_pins.jl and the CI workflow instead.
+#
+# The workflows pin every action to a full commit SHA (this account's
+# allowlist policy, asserted by test/unit/test_install_pins.jl). Dependabot
+# advances those pins to the current SHA of the tracked version, so the
+# pinning policy itself survives updates.
+#
+# The #124 rule: minor and patch updates are batched, because they are
+# interchangeable in kind; a MAJOR (React 18->19, vite 6->8, TypeScript
+# 5->7 -- which #124 landed as one grouped PR, with the build already red
+# until #140 repaired it) is a migration, not an update. Every group below
+# therefore names its update-types as minor and patch ONLY: an update that
+# matches no group opens its own PR, carrying its own review and its own CI
+# run. test/unit/test_install_pins.jl asserts this shape, so a new group
+# cannot silently go back to batching majors.
+version: 2
+updates:
+  # The frontend is Bun-managed: package.json plus bun.lock, no npm/yarn/pnpm
+  # lockfile, so it must be declared as the "bun" ecosystem.
+  - package-ecosystem: "bun"
+    directory: "/frontend"
+    schedule:
+      interval: "weekly"
+    commit-message:
+      prefix: "chore(deps)"
+    groups:
+      # Minor and patch in one weekly PR; majors arrive one PR each.
+      frontend-minor-and-patch:
+        patterns: ["*"]
+        update-types: ["minor", "patch"]
+
+  - package-ecosystem: "github-actions"
+    directory: "/"
+    schedule:
+      interval: "weekly"
+    commit-message:
+      prefix: "chore(deps)"
+    groups:
+      # Same rule as the frontend: a new major of an action (checkout
+      # v4.4.0 -> v7.0.1 came through #123) gets a PR of its own.
+      actions-minor-and-patch:
+        patterns: ["*"]
+        update-types: ["minor", "patch"]

.github/workflows/ci.yml

@@ -1,10 +1,20 @@
 name: CI
 
+# This fork's account allows only GitHub's own actions (actions/*) and its own,
+# each pinned to a full commit SHA. Upstream's julia-actions, oven-sh/setup-bun
+# and codecov/codecov-action are none of these, and with them this workflow
+# ended in startup_failure on every run. So Julia and Bun are installed here
+# from the archives config/defaults/tool_versions.yml pins, each refused unless
+# it hashes to the pinned SHA256, and the Julia depot is cached with
+# actions/cache. Coverage is kept as a workflow artifact, since the Codecov
+# project is upstream's. test/unit/test_install_pins.jl asserts that every
+# `uses:` in .github/workflows is allowed by that policy.
+
 on:
   push:
     branches: [main]
+  # Any base branch, so a PR stacked on another one is tested too.
   pull_request:
-    branches: [main]
 
 permissions:
   contents: read
@@ -17,8 +27,33 @@ concurrency:
 
 jobs:
   test:
-    name: Julia ${{ matrix.julia-version }} / ${{ matrix.os }}
-    runs-on: ${{ matrix.os }}
+    # The name is a fixed string, it carries no version, and the job has NO matrix.
+    # Both are required, and the first without the second is a trap that has already
+    # been sprung here once.
+    #
+    # A branch ruleset matches a required status check by the DISPLAY NAME GitHub posts
+    # for the job. A renamed check does not fail -- it is simply absent, and an absent
+    # required check can never be satisfied, so every pull request deadlocks until an
+    # admin bypasses the rule, triggered by nothing more alarming than editing a version
+    # number.
+    #
+    # MEASURED on hyperpolymath/MetaManifold-WebUI#39 (2026-09-21): this job, named exactly `Julia tests` but still
+    # carrying a 1x1 `strategy.matrix`, posted `Julia tests (1.12.5, ubuntu-24.04)`.
+    # GitHub appends the matrix combination whenever the name does not already reference
+    # the matrix, so a 1x1 matrix is still a matrix and the pins were still embedded in
+    # the check name. The matrix was therefore removed rather than merely renamed around:
+    # it selected exactly one combination and bought nothing.
+    #
+    # The two values it held are literals below, each keeping its own reasoning.
+    # `test/unit/test_install_pins.jl` asserts, for EVERY job in this file, that the name
+    # interpolates nothing AND that the job has no matrix -- so this cannot regress
+    # silently. If a matrix is ever genuinely wanted here, the required context must move
+    # to a matrix-free aggregator job first.
+    name: Julia tests
+    # Explicit, not ubuntu-latest: the R pin below names an apt package revision built
+    # for 24.04, and a runner that silently rolled to the next LTS would take that pin
+    # with it. `runs-on` cannot read `env`, so this is a literal.
+    runs-on: ubuntu-24.04
     # The repository's root .Rprofile sources renv/activate.R, so R started from
     # the checkout auto-activates renv and rewrites the library paths. renv is a
     # local-development convenience; CI installs into the system library and
@@ -28,30 +63,45 @@ jobs:
     # the environment, so those commands pass --no-init-file instead.
     env:
       RENV_CONFIG_AUTOLOADER_ENABLED: "FALSE"
-    strategy:
-      fail-fast: false
-      matrix:
-        # Pinned rather than tracking latest stable, because a pinned Manifest.toml
-        # resolved by an unpinned Julia is not a reproducible build. This must equal
-        # julia_version in Manifest.toml; it cannot be read from the pin file, since
-        # nothing can be read before Julia exists. test/unit/test_install_pins.jl
-        # fails if the three ever disagree.
-        julia-version: ["1.12.5"]
-        # Explicit, not ubuntu-latest: the R pin below names an apt package revision
-        # built for 24.04, and a runner that silently rolled to the next LTS would
-        # take that pin with it.
-        os: [ubuntu-24.04]
+      # Pinned rather than tracking latest stable, because a pinned Manifest.toml
+      # resolved by an unpinned Julia is not a reproducible build. These must equal
+      # runtimes.julia.archives.linux-x86_64 in the pin file, whose version must
+      # equal julia_version in Manifest.toml; they cannot be read from the pin
+      # file, since nothing can be read before Julia exists.
+      # test/unit/test_install_pins.jl fails if any of them disagree.
+      JULIA_URL: https://julialang-s3.julialang.org/bin/linux/x64/1.12/julia-1.12.5-linux-x86_64.tar.gz
+      JULIA_SHA256: 41b84d727e4e96fbf3ed9e92fa195d773d247b9097f73fad688f8b699758bae7
 
     steps:
-      - uses: actions/checkout@11d5960a326750d5838078e36cf38b85af677262  # v4.4.0
-
-      - name: Set up Julia
-        uses: julia-actions/setup-julia@4c0cb0fce8556fdb04a90347310e5db8b1f98fb9  # v2.7.0
+      - uses: actions/checkout@3d3c42e5aac5ba805825da76410c181273ba90b1  # v7.0.1
         with:
-          version: ${{ matrix.julia-version }}
+          persist-credentials: false   # nothing here pushes
 
-      - name: Cache Julia packages
-        uses: julia-actions/cache@d10a6fd8f31b12404a54613ebad242900567f2b9  # v2.1.0
+      - name: Install Julia
+        run: |
+          source scripts/ci/fetch_pinned.sh
+          fetch_pinned "$JULIA_URL" julia.tar.gz
+          echo "$JULIA_SHA256  julia.tar.gz" | sha256sum -c -
+          sudo mkdir -p /opt/julia
+          sudo tar xzf julia.tar.gz -C /opt/julia --strip-components=1
+          rm julia.tar.gz
+          echo /opt/julia/bin >> "$GITHUB_PATH"
+
+      # The registry, packages, artifacts and precompiled caches, keyed on the
+      # Manifest (which also names the Julia version). Saved once instantiation
+      # has succeeded, so a failed run cannot store a half-built depot.
+      - name: Restore the Julia depot
+        id: julia-depot
+        uses: actions/cache/restore@55cc8345863c7cc4c66a329aec7e433d2d1c52a9  # v6.1.0
+        with:
+          path: |
+            ~/.julia/registries
+            ~/.julia/packages
+            ~/.julia/artifacts
+            ~/.julia/compiled
+          key: julia-depot-${{ runner.os }}-${{ hashFiles('Manifest.toml') }}
+          restore-keys: |
+            julia-depot-${{ runner.os }}-
 
       # 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
@@ -67,7 +117,10 @@ jobs:
             pins = YAML.load_file("config/defaults/tool_versions.yml")
             open(ENV["GITHUB_ENV"], "a") do io
                 println(io, "R_APT_VERSION=", pins["runtimes"]["r"]["apt_version"])
-                println(io, "BUN_VERSION=", pins["toolchain"]["bun"]["version"])
+                bun = pins["toolchain"]["bun"]
+                println(io, "BUN_VERSION=", bun["version"])
+                println(io, "BUN_URL=", bun["archives"]["linux-x86_64"]["url"])
+                println(io, "BUN_SHA256=", bun["archives"]["linux-x86_64"]["sha256"])
                 println(io, "CUTADAPT_SPEC=cutadapt==", pins["tools"]["cutadapt"]["version"])
                 println(io, "MULTIQC_SPEC=multiqc==", pins["tools"]["multiqc"]["version"])
                 fastqc = pins["tools"]["fastqc"]["archives"]["any"]
@@ -122,7 +175,7 @@ jobs:
       # the restore runs as root. The run id makes each key unique so every attempt
       # saves its progress; restore-keys picks the newest match.
       - name: Restore the renv cache
-        uses: actions/cache/restore@0057852bfaa89a56745cba8c7296529d2fc39830  # v4.3.0
+        uses: actions/cache/restore@55cc8345863c7cc4c66a329aec7e433d2d1c52a9  # v6.1.0
         with:
           path: /opt/renv-cache
           key: renv-${{ runner.os }}-R${{ env.R_APT_VERSION }}-${{ hashFiles('renv.lock') }}-${{ github.run_id }}
@@ -139,7 +192,7 @@ jobs:
           sudo chmod 777 "$RENV_PATHS_CACHE"
           sudo env R_CLI_DYNAMIC=false TERM=dumb Rscript --no-init-file -e 'install.packages(c("renv", "BiocManager"), repos="https://cloud.r-project.org", lib=.Library)'
           sudo env RENV_PATHS_CACHE="$RENV_PATHS_CACHE" R_CLI_DYNAMIC=false TERM=dumb Rscript --no-init-file -e 'renv::restore(project=".", library=.Library, prompt=FALSE)'
-          Rscript --no-init-file -e 'for (pkg in c("dada2","Biostrings","ShortRead","vegan","dplyr","MASS")) if (!require(pkg,character.only=TRUE,quietly=TRUE)) stop(pkg, " failed to install")'
+          Rscript --no-init-file -e 'for (pkg in c("dada2","Biostrings","ShortRead","vegan","dplyr","MASS","zCompositions")) if (!require(pkg,character.only=TRUE,quietly=TRUE)) stop(pkg, " failed to install")'
 
       # Saved on failure too, since the packages built before a failure are the ones
       # the next attempt should reuse. Root writes the cache, so it is made readable first.
@@ -149,7 +202,7 @@ jobs:
 
       - name: Save the renv cache
         if: always()
-        uses: actions/cache/save@0057852bfaa89a56745cba8c7296529d2fc39830  # v4.3.0
+        uses: actions/cache/save@55cc8345863c7cc4c66a329aec7e433d2d1c52a9  # v6.1.0
         with:
           path: /opt/renv-cache
           key: renv-${{ runner.os }}-R${{ env.R_APT_VERSION }}-${{ hashFiles('renv.lock') }}-${{ github.run_id }}
@@ -204,10 +257,28 @@ jobs:
       - name: Instantiate Julia project
         run: julia --project=. -e 'import Pkg; Pkg.instantiate()'
 
-      - name: Set up Bun
-        uses: oven-sh/setup-bun@0c5077e51419868618aeaa5fe8019c62421857d6  # v2.2.0
+      - name: Save the Julia depot
+        if: steps.julia-depot.outputs.cache-hit != 'true'
+        uses: actions/cache/save@55cc8345863c7cc4c66a329aec7e433d2d1c52a9  # v6.1.0
         with:
-          bun-version: ${{ env.BUN_VERSION }}
+          path: |
+            ~/.julia/registries
+            ~/.julia/packages
+            ~/.julia/artifacts
+            ~/.julia/compiled
+          key: julia-depot-${{ runner.os }}-${{ hashFiles('Manifest.toml') }}
+
+      # Downloaded against the pinned URL and refused unless it hashes to the pinned
+      # SHA256, as install.jl does when no bun of this version is on PATH.
+      - name: Install Bun
+        run: |
+          source scripts/ci/fetch_pinned.sh
+          fetch_pinned "$BUN_URL" bun.zip
+          echo "$BUN_SHA256  bun.zip" | sha256sum -c -
+          unzip -q bun.zip
+          sudo mv bun-linux-x64/bun /usr/local/bin/bun
+          rm -rf bun.zip bun-linux-x64
+          test "$(bun --version)" = "$BUN_VERSION"
 
       - name: Build frontend
         working-directory: frontend
@@ -230,7 +301,7 @@ jobs:
           julia --project=. -e '
             using RCall
             R"cat(.libPaths(), sep=\"\n\")"
-            for pkg in ["dada2", "dplyr", "vegan", "tibble", "MASS"]
+            for pkg in ["dada2", "dplyr", "vegan", "tibble", "MASS", "zCompositions"]
               R"if (!require($pkg, character.only=TRUE, quietly=TRUE)) stop($pkg, \" not found\")"
             end
           '
@@ -272,13 +343,67 @@ jobs:
           fi
           exit "$status"
 
+      # What julia-processcoverage did: the .cov files under src/ to lcov.info, with
+      # CoverageTools pinned to an exact release.
       - name: Process coverage
-        uses: julia-actions/julia-processcoverage@03114f09f119417c3242a9fb6e0b722676aedf38  # v1.2.2
+        run: |
+          julia -e '
+            using Pkg
+            Pkg.activate(temp = true)
+            Pkg.add(name = "CoverageTools", version = "1.4.2")
+            using CoverageTools
+            LCOV.writefile("lcov.info", process_folder("src"))'
 
-      - name: Upload coverage to Codecov
-        uses: codecov/codecov-action@fb8b3582c8e4def4969c97caa2f19720cb33a72f  # v6.0.2
+      # The Codecov project (codecov.yml, the README badge) is upstream's, so the fork
+      # keeps its coverage as an artifact of the run instead.
+      - name: Keep coverage
+        uses: actions/upload-artifact@cf430e030ddbb5b0abf93d22962f4752f3646cd9  # v7.0.2
+        with:
+          name: lcov
+          path: lcov.info
+          retention-days: 14
+
+  # Machine-checked proofs of the Benjamini-Hochberg adjustment, the TSS/RLE
+  # scaling algebra and PERMANOVA's permutation bookkeeping (proofs/agda,
+  # proofs/agda/README.md).
+  # Agda publishes no 2.6.4.3 binary, and agda-stdlib 2.1 requires Agda 2.6.4.x,
+  # so the pair comes from Debian trixie, which packages exactly that pair with
+  # pre-built library interfaces. The image is pinned by digest and the two
+  # packages by revision, so a rebuild in the archive fails loudly here instead
+  # of silently changing the checker. These pins live here rather than in
+  # config/defaults/tool_versions.yml because no other job and no installer
+  # reads them.
+  agda:
+    name: Agda proofs
+    runs-on: ubuntu-24.04
+    container: debian:trixie-20250929-slim@sha256:1caf1c703c8f7e15dcf2e7769b35000c764e6f50e4d7401c355fb0248f3ddfdb
+    timeout-minutes: 30
+    env:
+      DEBIAN_FRONTEND: noninteractive
+    steps:
+      - uses: actions/checkout@3d3c42e5aac5ba805825da76410c181273ba90b1  # v7.0.1
         with:
-          files: lcov.info
-          token: ${{ secrets.CODECOV_TOKEN }}
-          slug: JoshuaJewell/MetaManifold-WebUI
-          fail_ci_if_error: false
+          persist-credentials: false   # nothing here pushes
+
+      - name: Install Agda and the standard library
+        run: |
+          apt-get update -qq
+          apt-get install -y --no-install-recommends agda-bin=2.6.4.3-1+b2 agda-stdlib=2.1-4
+          agda --version | grep -qx 'Agda version 2.6.4.3'
+          grep -qx 'name: standard-library-2.1' /usr/share/agda-stdlib/standard-library.agda-lib
+
+      # Runs before the type-check: --safe already refuses postulates, but the
+      # audit also refuses holes, check-disabling pragmas and flags, and any
+      # module that MetaManifold/All.agda does not import (an unimported module
+      # is never type-checked at all).
+      - name: Axiom audit
+        run: bash proofs/tests/axiom-audit.sh
+
+      - name: Type-check
+        env:
+          AGDA_DIR: /tmp/agda-dir
+        run: |
+          mkdir -p "$AGDA_DIR"
+          echo /usr/share/agda-stdlib/standard-library.agda-lib > "$AGDA_DIR/libraries"
+          cd proofs/agda
+          agda MetaManifold/All.agda