Repository navigation

chore(deps): bump actions/upload-artifact from 4.6.2 to 7.0.2 #702

Workflow file for this run

	name: CI

	on:
	push:
	branches: [main]
	pull_request:
	branches: [main]

	permissions:
	contents: read

	# Pushes to main queue so each merge gets a test result; PR updates cancel the
	# run for the superseded head.
	concurrency:
	group: ${{ github.workflow }}-${{ github.ref }}
	cancel-in-progress: ${{ github.event_name != 'push' }}

	jobs:
	# Restore the required relevance contexts removed by the baseline sync (#178).
	# A failed comparison fails its gate; a docs-only diff can skip expensive jobs.
	gate:
	name: Code relevance
	runs-on: ubuntu-24.04
	timeout-minutes: 10
	outputs:
	relevant: ${{ steps.push.outputs.relevant \|\| steps.pr.outputs.relevant }}
	steps:
	# A push only starts this workflow on main (the branch filter above), so
	# the gate has nothing to decide: every push is relevant.
	- name: A push is already branch-filtered
	id: push
	if: github.event_name == 'push'
	run: echo 'relevant=true' >> "$GITHUB_OUTPUT"

	# Full history, because the three-dot diff names the merge base of the
	# PR's base tip and its merge commit, and a stacked PR's merge base sits
	# further back still.
	- name: Checkout the change
	if: github.event_name == 'pull_request'
	uses: actions/checkout@11d5960a326750d5838078e36cf38b85af677262 # v4.4.0
	with:
	persist-credentials: false # nothing here pushes
	fetch-depth: 0

	# --no-renames, so a file renamed out of a listed path is reported as a
	# deletion under its original name and still counts. -z with a
	# NUL-delimited read, so a pathname Git would quote or that contains a
	# newline arrives raw and matches the pattern. The base SHA travels
	# through env, not template interpolation into the script.
	- name: Does the change touch anything the suite exercises?
	id: pr
	if: github.event_name == 'pull_request'
	env:
	BASE_SHA: ${{ github.event.pull_request.base.sha }}
	run: \|
	relevant=false
	# Every pattern is quoted, so the glob survives array assignment and
	# fires at `case` time, against the diff -- an unquoted `src/*` would
	# expand against the checkout the runner happens to be standing in.
	patterns=('src/' 'test/' 'scripts/' 'frontend/' 'config/*'
	'bench/' 'data/' 'proofs/' 'R/' 'renv/*' 'Project.toml'
	'Manifest.toml' 'renv.lock' '.Rprofile' 'install.sh' 'install.jl'
	'start.sh' 'docs/occupancy/*' 'docs/occupancy-2026-10.adoc'
	'.github/workflows/*')
	# The diff goes to a file first because a process substitution hides
	# git diff's exit status: an unavailable comparison SHA (a force-push
	# on the base branch, for instance) or a repository error would read
	# as "no changes", and the gate would post relevant=false -- skipping
	# the Julia suite and the proof checker, whose `skipped` conclusion
	# satisfies a required check -- so a relevant PR would pass silently.
	# A failed diff must fail the gate itself: that is the one failure
	# the required-check design cannot afford to skip. As in the
	# occupancy gate, which this mirrors.
	changed="$RUNNER_TEMP/ci-changed-files"
	if ! git diff --no-renames --name-only -z "$BASE_SHA...HEAD" > "$changed"; then
	echo "ERROR: git diff $BASE_SHA...HEAD failed" >&2
	exit 1
	fi
	while IFS= read -r -d '' file; do
	for pattern in "${patterns[@]}"; do
	case "$file" in
	$pattern) relevant=true; break 2 ;;
	esac
	done
	done < "$changed"
	echo "relevant=$relevant" >> "$GITHUB_OUTPUT"

	occupancy_gate:
	name: Occupancy relevance
	runs-on: ubuntu-24.04
	timeout-minutes: 10
	outputs:
	relevant: ${{ steps.push.outputs.relevant \|\| steps.pr.outputs.relevant }}
	steps:
	# All pushes to main are relevant; PRs use the path classification below.
	- name: A push to main is relevant
	id: push
	if: github.event_name == 'push'
	run: echo 'relevant=true' >> "$GITHUB_OUTPUT"

	# Full history, because the three-dot diff names the merge base of the
	# PR's base tip and its merge commit -- a shallow checkout does not have
	# both, and a stacked PR's merge base sits further back still.
	- name: Checkout the change
	if: github.event_name == 'pull_request'
	uses: actions/checkout@11d5960a326750d5838078e36cf38b85af677262 # v4.4.0
	with:
	persist-credentials: false # nothing here pushes
	fetch-depth: 0

	- name: Does the change touch the occupancy reading?
	id: pr
	if: github.event_name == 'pull_request'
	env:
	# zizmor flags template expressions interpolated into run scripts
	# (template-injection), and the gate script is easier to run locally
	# with the value in an environment variable in any case. The base SHA
	# is GitHub-supplied, but the indirection costs nothing.
	BASE_SHA: ${{ github.event.pull_request.base.sha }}
	run: \|
	relevant=false
	patterns=('src/core/memory_probe.jl' 'src/core/provenance.jl' 'src/pipeline/tools.jl'
	'src/server/routes/pipeline.jl' 'test/occupancy_disagreement_test.jl'
	'test/unit/test_occupancy_grade.jl' 'scripts/check-occupancy-grades.jl'
	'scripts/lint-occupancy-readings.sh' 'docs/occupancy/*'
	'docs/occupancy-2026-10.adoc' 'scripts/check-occupancy.sh'
	'scripts/fetch-siblings.sh' 'scripts/install-ci-julia.sh'
	'Project.toml' 'Manifest.toml' 'renv.lock' 'config/defaults/tool_versions.yml'
	'.github/workflows/*')
	# The diff goes to a file first because a process substitution hides
	# git diff's exit status: an unavailable comparison SHA or a repository
	# error would read as "no changes", and the gate would post
	# relevant=false -- skipping the two occupancy jobs, whose `skipped`
	# conclusion satisfies a required check -- so a relevant PR would
	# pass silently. A failed diff must fail the gate itself: that is
	# the one failure the required-check design cannot afford to skip.
	changed="$RUNNER_TEMP/occupancy-changed-files"
	if ! git diff --no-renames --name-only -z "$BASE_SHA...HEAD" > "$changed"; then
	echo "ERROR: git diff $BASE_SHA...HEAD failed" >&2
	exit 1
	fi
	while IFS= read -r -d '' file; do
	for pattern in "${patterns[@]}"; do
	case "$file" in
	$pattern) relevant=true; break 2 ;;
	esac
	done
	done < "$changed"
	echo "relevant=$relevant" >> "$GITHUB_OUTPUT"

	test:
	# 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
	# R/Julia setup and integration tests are expensive, but may not hang for 6h.
	timeout-minutes: 90
	needs: gate
	if: needs.gate.outputs.relevant == 'true'
	# 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
	# reaches it through R_LIBS_SITE, so the autoloader is switched off here.
	# This variable covers the unprivileged R that Julia embeds through RCall.
	# It cannot cover the installs themselves, which run under sudo: sudo resets
	# the environment, so those commands pass --no-init-file instead.
	env:
	RENV_CONFIG_AUTOLOADER_ENABLED: "FALSE"

	steps:
	- uses: actions/checkout@11d5960a326750d5838078e36cf38b85af677262 # v4.4.0

	# The required "SonarCloud Code Analysis" check is the GitHub App's
	# automatic analysis -- nothing in this repository configures or runs it,
	# so its rules cannot be read here and its failure arrives only after the
	# push. This script reproduces the rule that failed the gate and the one
	# that came with it, needs no toolchain, and runs in about 0.1s: first,
	# before anything is installed, so the message beats the wait.
	- name: Check the Sonar reliability rules the gate enforces
	run: bash scripts/lint-sonar-reliability.sh

	- name: Set up Julia
	run: bash scripts/install-ci-julia.sh

	- name: Parse Julia sources before dependency setup
	run: julia scripts/check-julia-syntax.jl

	- name: Cache Julia packages
	uses: actions/cache@0057852bfaa89a56745cba8c7296529d2fc39830 # v4.3.0
	with:
	path: \|
	~/.julia/artifacts
	~/.julia/packages
	~/.julia/registries
	key: julia-${{ runner.os }}-${{ hashFiles('Manifest.toml', 'config/defaults/tool_versions.yml') }}

	# 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:
	# RCall's build step requires it.
	- name: Read pinned versions
	run: \|
	julia -e '
	using Pkg
	Pkg.activate(temp = true)
	Pkg.add("YAML")
	using YAML
	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"])
	println(io, "CUTADAPT_SPEC=cutadapt==", pins["tools"]["cutadapt"]["version"])
	println(io, "MULTIQC_SPEC=multiqc==", pins["tools"]["multiqc"]["version"])
	fastqc = pins["tools"]["fastqc"]["archives"]["any"]
	println(io, "FASTQC_URL=", fastqc["url"])
	println(io, "FASTQC_SHA256=", fastqc["sha256"])
	for tool in ("vsearch", "swarm")
	archive = pins["tools"][tool]["archives"]["linux-x86_64"]
	println(io, uppercase(tool), "_VERSION=", pins["tools"][tool]["version"])
	println(io, uppercase(tool), "_URL=", archive["url"])
	println(io, uppercase(tool), "_SHA256=", archive["sha256"])
	end
	end'

	# R + required packages (needed by RCall)
	# Install R directly via apt to avoid r-lib/actions/setup-r mangling
	# R_HOME and stripping default packages (utils, methods, stats, etc.)
	# The version is pinned to the apt revision named in the pin file, which tracks
	# R.Version in renv.lock; CRAN's Ubuntu repository retains older revisions, so
	# this resolves rather than merely requesting the newest.
	- name: Set up R
	run: \|
	wget --https-only -qO- https://cloud.r-project.org/bin/linux/ubuntu/marutter_pubkey.asc \
	\| sudo gpg --dearmor -o /usr/share/keyrings/r-project.gpg
	echo "deb [signed-by=/usr/share/keyrings/r-project.gpg] https://cloud.r-project.org/bin/linux/ubuntu $(lsb_release -cs)-cran40/" \
	\| sudo tee /etc/apt/sources.list.d/r-project.list
	sudo apt-get update -qq
	sudo apt-get install -y \
	r-base-core="$R_APT_VERSION" \
	r-base-dev="$R_APT_VERSION" \
	r-base-html="$R_APT_VERSION" \
	r-recommended="$R_APT_VERSION" \
	r-base="$R_APT_VERSION"
	Rscript -e 'cat(R.version.string, "\n")'

	- name: Install R system dependencies
	run: sudo apt-get install -y libcurl4-openssl-dev libssl-dev libxml2-dev libfontconfig1-dev

	# The R packages are restored from renv.lock, the same pin a developer restores
	# from, rather than resolved against whatever the repositories serve that day.
	# Asking for a bare package name pins nothing: a Bioconductor release is frozen,
	# so dada2 and its kin held still, but CRAN publishes only its newest revision,
	# so vegan silently moved off the pinned 2.7-3 and test_provenance caught the
	# drift. Restoring into .Library keeps the system library that the RCall steps
	# and R_LIBS_SITE below expect, and renv is invoked explicitly here rather than
	# left to activate itself. --no-init-file stops R sourcing the repository's
	# .Rprofile, and with it the renv autoloader, which would otherwise rebind
	# .Library to its own sandbox under root's cache; the flag is used rather than
	# the environment variable above because sudo resets the environment first.
	#
	# renv's package cache persists across runs, so a restore that fails partway
	# resumes from the packages it already built. The cache sits outside ~ because
	# 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
	with:
	path: /opt/renv-cache
	key: renv-${{ runner.os }}-R${{ env.R_APT_VERSION }}-${{ hashFiles('renv.lock') }}-${{ github.run_id }}
	restore-keys: \|
	renv-${{ runner.os }}-R${{ env.R_APT_VERSION }}-${{ hashFiles('renv.lock') }}-
	renv-${{ runner.os }}-R${{ env.R_APT_VERSION }}-

	# R_CLI_DYNAMIC and TERM make renv print progress one line at a time in the log.
	- name: Install R packages
	env:
	RENV_PATHS_CACHE: /opt/renv-cache
	run: \|
	sudo mkdir -p "$RENV_PATHS_CACHE"
	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","MASS","zCompositions","glmGamPoi")) if (!require(pkg,character.only=TRUE,quietly=TRUE)) stop(pkg, " failed to install")'

	- name: Check DADA2 CSV assembly
	run: Rscript --vanilla test/unit/test_dada2_tables.R

	# 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.
	- name: Make the renv cache readable
	if: always()
	run: sudo chmod -R a+rX /opt/renv-cache \|\| true

	- name: Save the renv cache
	if: always()
	uses: actions/cache/save@0057852bfaa89a56745cba8c7296529d2fc39830 # v4.3.0
	with:
	path: /opt/renv-cache
	key: renv-${{ runner.os }}-R${{ env.R_APT_VERSION }}-${{ hashFiles('renv.lock') }}-${{ github.run_id }}

	- name: Install cutadapt
	run: pip install "$CUTADAPT_SPEC"

	# The one tool CI does not pin. Ubuntu ships no versioned cd-hit revision worth
	# naming, and 24.04 is frozen, so its cd-hit does not move under us; the version
	# that arrives is recorded at preflight, where a discrepancy is visible.
	- name: Install cd-hit
	run: sudo apt-get install -y cd-hit

	# Downloaded against the pinned URL and refused unless it hashes to the pinned
	# SHA256, so CI runs the same bytes install.jl puts on a developer's machine.
	- name: Install vsearch
	run: \|
	source scripts/ci/fetch_pinned.sh
	fetch_pinned "$VSEARCH_URL" vsearch.tar.gz
	echo "$VSEARCH_SHA256 vsearch.tar.gz" \| sha256sum -c -
	tar xzf vsearch.tar.gz --warning=no-unknown-keyword
	sudo mv "vsearch-$VSEARCH_VERSION-linux-x86_64/bin/vsearch" /usr/local/bin/vsearch
	rm -rf vsearch.tar.gz "vsearch-$VSEARCH_VERSION-linux-x86_64"
	vsearch --version

	- name: Install swarm
	run: \|
	source scripts/ci/fetch_pinned.sh
	fetch_pinned "$SWARM_URL" swarm.tar.gz
	echo "$SWARM_SHA256 swarm.tar.gz" \| sha256sum -c -
	tar xzf swarm.tar.gz --warning=no-unknown-keyword
	sudo mv "swarm-$SWARM_VERSION-linux-x86_64/bin/swarm" /usr/local/bin/swarm
	rm -rf swarm.tar.gz "swarm-$SWARM_VERSION-linux-x86_64"
	swarm --version

	- name: Install multiqc
	run: pip install "$MULTIQC_SPEC"

	# FastQC ships as a Java launcher script; `fastqc --version` checks that Java
	# is on PATH as well.
	- name: Install fastqc
	run: \|
	source scripts/ci/fetch_pinned.sh
	fetch_pinned "$FASTQC_URL" fastqc.zip
	echo "$FASTQC_SHA256 fastqc.zip" \| sha256sum -c -
	sudo unzip -q -d /opt fastqc.zip
	rm -f fastqc.zip
	sudo chmod +x /opt/FastQC/fastqc
	sudo ln -sf /opt/FastQC/fastqc /usr/local/bin/fastqc
	fastqc --version

	- 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
	with:
	bun-version: ${{ env.BUN_VERSION }}

	- name: Build frontend
	working-directory: frontend
	run: \|
	bun install --frozen-lockfile --ignore-scripts
	bun run build

	- name: Audit frontend dependencies
	working-directory: frontend
	# Moderate advisories remain visible in `bun audit`; upgrading Router
	# across a major version needs a separate routing/SSR review.
	run: bun audit --audit-level high

	- name: Frontend unit tests
	working-directory: frontend
	run: bun run test

	- name: Download PR2 databases
	run: julia --project=. config/ci/download_databases.jl

	- name: Rebuild RCall against installed R
	run: julia --project=. -e 'import Pkg; Pkg.build("RCall")'

	- name: Verify R packages visible from RCall
	run: \|
	julia --project=. -e '
	using RCall
	R"cat(.libPaths(), sep=\"\n\")"
	for pkg in ["dada2", "vegan", "tibble", "MASS", "zCompositions", "glmGamPoi"]
	R"if (!require($pkg, character.only=TRUE, quietly=TRUE)) stop($pkg, \" not found\")"
	end
	'

	- name: Check independent high-precision references
	run: python3 test/references/check_high_precision_references.py --check test/unit/test_high_precision.jl

	- name: Run validated-statistics tests first
	env:
	R_LIBS_SITE: /usr/local/lib/R/site-library:/usr/lib/R/site-library:/usr/lib/R/library
	shell: bash
	run: \|
	set +e
	julia --project=. -t2 --compiled-modules=no test/runtests.jl validated_statistics numeric_policy exact_summaries high_precision derived_analyses 2>&1 \| tee /tmp/validated-statistics-tests.log
	# Preserve both exits immediately: a successful Julia run must not
	# hide a failed log write (e.g. a full runner filesystem).
	statuses=("${PIPESTATUS[@]}")
	status="${statuses[0]}"
	if [ "$status" -eq 0 ]; then status="${statuses[1]}"; fi
	if [ "$status" -ne 0 ]; then
	enc() { head -c 3000 \| sed -e 's/%/%25/g' -e 's/\r/%0D/g' \| awk '{printf "%s%%0A", $0}'; }
	# One annotation cannot hold a failing run, and a tail hides every
	# failure but the last one. Publish a digest of all failing
	# assertions first - the testset, the expression and the evaluated
	# values are what identify the bug - then the end of the log.
	# `set +e` above is deliberate: diagnostic helpers may find no
	# matches, and only the captured test status controls this step.
	grep -E "Test Failed at \|Error During Test at \|^ Expression: \|^ Evaluated: \|^ Test threw exception" \
	/tmp/validated-statistics-tests.log > /tmp/validated-statistics-failures.log
	rm -f /tmp/validated-statistics-digest-*
	split -b 2500 /tmp/validated-statistics-failures.log /tmp/validated-statistics-digest-
	index=0
	for chunk in /tmp/validated-statistics-digest-*; do
	[ -e "$chunk" ] \|\| continue
	index=$((index + 1))
	[ "$index" -le 8 ] \|\| break
	echo "::error title=Validated-statistics failure digest $index::$(enc < "$chunk")"
	done
	echo "::error title=Validated-statistics log tail::$(tail -c 3000 /tmp/validated-statistics-tests.log \| enc)"
	fi
	exit "$status"

	- name: Run tests
	env:
	OCCUPANCY_RESULTS: ${{ runner.temp }}/occupancy-results.yml
	CI_SKIP_TAXONOMY: "1"
	R_LIBS_SITE: /usr/local/lib/R/site-library:/usr/lib/R/site-library:/usr/lib/R/library
	# A failure also posts annotations, which the checks API serves without the full
	# log. Annotations are capped at 4096 bytes, so each failing assertion gets its own
	# (up to 8), followed by the summary rows that report a failure or an error.
	shell: bash
	run: \|
	command -v vsearch # The full suite must run the occupancy experiment, not skip it.
	set +e
	julia --project=. -t 2 --code-coverage=user --compiled-modules=no test/runtests.jl --integration --server 2>&1 \| tee /tmp/julia-tests.log
	# Preserve both exits immediately: a successful Julia run must not
	# hide a failed log write (e.g. a full runner filesystem).
	statuses=("${PIPESTATUS[@]}")
	status="${statuses[0]}"
	if [ "$status" -eq 0 ]; then status="${statuses[1]}"; fi
	if [ "$status" -ne 0 ]; then
	enc() { head -c 3500 \| sed -e 's/%/%25/g' -e 's/\r/%0D/g' \| awk '{printf "%s%%0A", $0}'; }
	awk '
	/Test Summary:/ { left = 0 }
	/(Test Failed at\|Error During Test at)/ \|\| (left == 0 && /Got exception outside of a @test/) { n++; left = 60 }
	left > 0 { print > ("/tmp/julia-failure-" n ".txt"); left-- }
	' /tmp/julia-tests.log
	shown=0
	for f in $(ls /tmp/julia-failure-*.txt 2>/dev/null \| sort -t- -k3 -n); do
	shown=$((shown + 1))
	[ "$shown" -gt 8 ] && break
	echo "::error title=Julia test failure ${shown}::$(enc < "$f")"
	done
	awk '
	/Test Summary:/ { print; p = index($0, "Pass"); pe = (p ? p + 3 : 0); t = index($0, "Total"); next }
	pe && t && index($0, "\|") && substr($0, pe + 1, t - pe - 1) ~ /[0-9]/ { print; next }
	/ERROR:\|Some tests did not pass/ { print }
	' /tmp/julia-tests.log \| tail -n 60 > /tmp/julia-tests-summary.txt
	echo "::error title=Julia tests failed (summary)::$(enc < /tmp/julia-tests-summary.txt)"
	if [ "$shown" -eq 0 ]; then
	echo "::error title=Julia tests failed (tail)::$(tail -c 3500 /tmp/julia-tests.log \| enc)"
	fi
	fi
	exit "$status"

	- name: Benchmark validated statistics
	run: julia --project=. -t2 bench/validated_statistics.jl --output "$RUNNER_TEMP/validated-statistics-benchmark.json"

	- name: Retain validated-statistics benchmark
	if: always()
	uses: actions/upload-artifact@cf430e030ddbb5b0abf93d22962f4752f3646cd9 # v7.0.2
	with:
	name: validated-statistics-benchmark
	path: ${{ runner.temp }}/validated-statistics-benchmark.json
	if-no-files-found: ignore
	retention-days: 30

	- name: Validate measured occupancy grades
	run: \|
	julia --project=. scripts/check-occupancy-grades.jl "$RUNNER_TEMP/occupancy-results.yml"
	bash scripts/lint-occupancy-readings.sh

	- name: Process coverage
	run: julia scripts/process-ci-coverage.jl

	- name: Upload coverage to Codecov
	uses: codecov/codecov-action@fb8b3582c8e4def4969c97caa2f19720cb33a72f # v6.0.2
	with:
	files: lcov.info
	token: ${{ secrets.CODECOV_TOKEN }}
	slug: JoshuaJewell/MetaManifold-WebUI
	fail_ci_if_error: false

	# Machine-checked proofs of the Benjamini-Hochberg adjustment and the TSS/RLE
	# scaling algebra (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
	needs: gate
	if: needs.gate.outputs.relevant == 'true'
	runs-on: ubuntu-24.04
	container: debian:trixie-20250929-slim@sha256:1caf1c703c8f7e15dcf2e7769b35000c764e6f50e4d7401c355fb0248f3ddfdb
	timeout-minutes: 30
	env:
	DEBIAN_FRONTEND: noninteractive
	steps:
	- uses: actions/checkout@11d5960a326750d5838078e36cf38b85af677262 # v4.4.0

	- 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
	if ! agda MetaManifold/All.agda >/tmp/agda.log 2>&1; then
	cat /tmp/agda.log
	msg="$(awk 'NR > 1 { printf "%%0A" } { gsub(/%/, "%25"); printf "%s", $0 }' /tmp/agda.log \| tail -c 3500)"
	echo "::error file=proofs/agda/MetaManifold/All.agda,title=Agda type-check failed::$msg"
	exit 1
	fi
	cat /tmp/agda.log

	occupancy:
	name: Occupancy typed peak
	needs: occupancy_gate
	if: needs.occupancy_gate.outputs.relevant == 'true'
	runs-on: ubuntu-24.04
	container: debian:trixie-20250929-slim@sha256:1caf1c703c8f7e15dcf2e7769b35000c764e6f50e4d7401c355fb0248f3ddfdb
	timeout-minutes: 30
	steps:
	- uses: actions/checkout@11d5960a326750d5838078e36cf38b85af677262
	- name: Install proof tools
	run: \|
	apt-get update -qq
	apt-get install -y --no-install-recommends ca-certificates curl git agda-bin=2.6.4.3-1+b2 agda-stdlib=2.1-4
	- name: Set up Julia
	run: bash scripts/install-ci-julia.sh
	- name: Check Session IR and occupancy proofs
	run: bash scripts/check-occupancy.sh

	# The full suite already runs the actual two-thread vsearch experiment. This
	# required context reports that result, including the fresh grade validation,
	# instead of paying for a second Julia/R installation and repeating the run.
	disagreement:
	name: Occupancy disagreement test
	needs: [occupancy_gate, test]
	if: always() && needs.occupancy_gate.result == 'success' && needs.occupancy_gate.outputs.relevant == 'true'
	runs-on: ubuntu-24.04
	timeout-minutes: 5
	steps:
	- name: Require the executed experiment and grade validation to pass
	env:
	TEST_RESULT: ${{ needs.test.result }}
	run: \|
	if [ "$TEST_RESULT" != success ]; then
	echo "ERROR: full suite, occupancy experiment or measured-grade validation did not pass ($TEST_RESULT)" >&2
	exit 1
	fi
	echo 'The full Julia suite passed, including the two-thread vsearch experiment and fresh empirical grade validation.' >> "$GITHUB_STEP_SUMMARY"

Navigation Menu

Repository navigation

chore(deps): bump actions/upload-artifact from 4.6.2 to 7.0.2 #702

Workflow file

chore(deps): bump actions/upload-artifact from 4.6.2 to 7.0.2 #702

Uh oh!

Workflow file for this run