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
70 changes: 60 additions & 10 deletions .github/workflows/ci.yml
Original file line number Diff line number Diff line change
Expand Up @@ -240,17 +240,53 @@ jobs:
- uses: actions/checkout@3d3c42e5aac5ba805825da76410c181273ba90b1 # v7.0.1

- name: Set up Julia
uses: julia-actions/setup-julia@fa02766e078afaaf09b14210362cee14137e6a32 # v3.0.2
with:
# 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.
version: "1.12.5"
# julia-actions/setup-julia is refused by this repository's Actions
# allow-list: every action must be from a repository owned by
# hyperpolymath, created by GitHub, verified in the GitHub Marketplace,
# or match the configured pattern, AND be pinned to a full-length
# commit SHA. A refused action does not fail the job -- it prevents the
# job from starting (startup_failure), which silenced every workflow
# from 2026-09-25 22:19 UTC onward. Julia is therefore installed
# straight from the official binaries and verified against the
# official checksum file before anything from it executes.
#
# JULIA_VERSION is pinned rather than tracking latest stable, because a
# pinned Manifest.toml resolved by an unpinned Julia is not a
# reproducible build. It 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.
run: |
set -euo pipefail
JULIA_VERSION="1.12.5"
archive="julia-${JULIA_VERSION}-linux-x86_64.tar.gz"
base="https://julialang-s3.julialang.org/bin"
curl --fail --location --retry 3 --retry-all-errors --max-time 600 \
"${base}/linux/x64/${JULIA_VERSION%.*}/${archive}" \
-o "${RUNNER_TEMP}/${archive}"
curl --fail --location --retry 3 --retry-all-errors --max-time 120 \
"${base}/checksums/julia-${JULIA_VERSION}.sha256" \
-o "${RUNNER_TEMP}/julia-${JULIA_VERSION}.sha256"
grep "${archive}" "${RUNNER_TEMP}/julia-${JULIA_VERSION}.sha256" \
| (cd "${RUNNER_TEMP}" && sha256sum --check)
mkdir -p "${RUNNER_TEMP}/julia"
tar -xzf "${RUNNER_TEMP}/${archive}" -C "${RUNNER_TEMP}/julia" --strip-components=1
echo "${RUNNER_TEMP}/julia/bin" >> "${GITHUB_PATH}"

- name: Cache Julia packages
uses: julia-actions/cache@a7bed9df697e5d7309d68afe7542a87621a8b6c8 # v3.3.0
# julia-actions/cache is refused by the Actions allow-list (see
# "Set up Julia" above); actions/cache at a full-length SHA is
# permitted and caches the same depot directories.
uses: actions/cache@55cc8345863c7cc4c66a329aec7e433d2d1c52a9 # v6.1.0
with:
path: |
~/.julia/artifacts
~/.julia/packages
~/.julia/compiled
~/.julia/registries
key: julia-depot-${{ runner.os }}-${{ hashFiles('Manifest.toml', 'Project.toml') }}
restore-keys: |
julia-depot-${{ runner.os }}-

# Static source lint, deliberately dependency-free (`--project=no`) so it can
# run before instantiation and fail in seconds rather than after the ~26
Expand Down Expand Up @@ -632,7 +668,21 @@ jobs:
exit "$status"

- name: Process coverage
uses: julia-actions/julia-processcoverage@03114f09f119417c3242a9fb6e0b722676aedf38 # v1
# Faithful replacement for julia-actions/julia-processcoverage, which
# the Actions allow-list refuses: same library (CoverageTools), same
# default directories (src and ext, with ext skipped when absent), same
# output (lcov.info at the workspace root). The temporary environment
# keeps the checkout's Project/Manifest untouched.
run: |
set -euo pipefail
julia --startup-file=no -e '
using Pkg
Pkg.activate(temp = true)
Pkg.add(PackageSpec(name = "CoverageTools"))
using CoverageTools
dirs = filter(isdir, ["src", "ext"])
LCOV.writefile("lcov.info", mapreduce(process_folder, vcat, dirs))
'

- name: Upload coverage artifact (local, Codecov removed per Milestone 2)
if: always()
Expand Down
34 changes: 31 additions & 3 deletions .github/workflows/doi.yml
Original file line number Diff line number Diff line change
Expand Up @@ -21,10 +21,38 @@ jobs:
JULIA_PKG_PRECOMPILE_AUTO: '0'
steps:
- uses: actions/checkout@3d3c42e5aac5ba805825da76410c181273ba90b1 # v7.0.1
- uses: julia-actions/setup-julia@fa02766e078afaaf09b14210362cee14137e6a32 # v3.0.2
# julia-actions/* is refused by the repository's Actions allow-list
# (startup_failure), so Julia is installed from the official binaries
# with checksum verification instead -- same version and procedure as
# ci.yml's "Set up Julia" step, which test/unit/test_install_pins.jl pins.
- name: Set up Julia
run: |
set -euo pipefail
JULIA_VERSION="1.12.5"
archive="julia-${JULIA_VERSION}-linux-x86_64.tar.gz"
base="https://julialang-s3.julialang.org/bin"
curl --fail --location --retry 3 --retry-all-errors --max-time 600 \
"${base}/linux/x64/${JULIA_VERSION%.*}/${archive}" \
-o "${RUNNER_TEMP}/${archive}"
curl --fail --location --retry 3 --retry-all-errors --max-time 120 \
"${base}/checksums/julia-${JULIA_VERSION}.sha256" \
-o "${RUNNER_TEMP}/julia-${JULIA_VERSION}.sha256"
grep "${archive}" "${RUNNER_TEMP}/julia-${JULIA_VERSION}.sha256" \
| (cd "${RUNNER_TEMP}" && sha256sum --check)
mkdir -p "${RUNNER_TEMP}/julia"
tar -xzf "${RUNNER_TEMP}/${archive}" -C "${RUNNER_TEMP}/julia" --strip-components=1
echo "${RUNNER_TEMP}/julia/bin" >> "${GITHUB_PATH}"
- name: Cache Julia packages
uses: actions/cache@55cc8345863c7cc4c66a329aec7e433d2d1c52a9 # v6.1.0
with:
version: '1.12.5'
- uses: julia-actions/cache@a7bed9df697e5d7309d68afe7542a87621a8b6c8 # v3.3.0
path: |
~/.julia/artifacts
~/.julia/packages
~/.julia/compiled
~/.julia/registries
key: julia-depot-${{ runner.os }}-${{ hashFiles('test/doi/Manifest.toml', 'test/doi/Project.toml') }}
restore-keys: |
julia-depot-${{ runner.os }}-
- uses: oven-sh/setup-bun@0c5077e51419868618aeaa5fe8019c62421857d6 # v2
with:
bun-version-file: .bun-version
Expand Down
14 changes: 9 additions & 5 deletions .github/workflows/proofs.yml
Original file line number Diff line number Diff line change
Expand Up @@ -37,14 +37,18 @@ jobs:
runs-on: ubuntu-24.04
timeout-minutes: 45
steps:
- uses: actions/checkout@v4
# Tag refs (@v4/@v5) are refused by the repository's Actions allow-list,
# which requires a full-length commit SHA; run 36293672919 never started
# for exactly this reason. The SHAs below are the commits the tags pointed
# at when the policy was enforced, so behaviour is unchanged.
- uses: actions/checkout@11d5960a326750d5838078e36cf38b85af677262 # v4

- uses: actions/setup-python@v5
- uses: actions/setup-python@a26af69be951a213d495a4c3e4e4022e16d87065 # v5
with:
python-version: "3.11"

- name: Cache the vendored toolchain
uses: actions/cache@v4
uses: actions/cache@0057852bfaa89a56745cba8c7296529d2fc39830 # v4
with:
path: |
proofs/.vendor
Expand Down Expand Up @@ -75,7 +79,7 @@ jobs:

- name: Upload the type-check transcript
if: always()
uses: actions/upload-artifact@v4
uses: actions/upload-artifact@ea165f8d65b6e75b540449e92b4886f43607fa02 # v4
with:
name: agda-typecheck-transcript
path: proofs-typecheck.log
Expand All @@ -89,7 +93,7 @@ jobs:
runs-on: ubuntu-24.04
timeout-minutes: 10
steps:
- uses: actions/checkout@v4
- uses: actions/checkout@11d5960a326750d5838078e36cf38b85af677262 # v4

- name: Every module is listed, and every listed module exists
run: |
Expand Down
34 changes: 31 additions & 3 deletions .github/workflows/ui.yml
Original file line number Diff line number Diff line change
Expand Up @@ -21,10 +21,38 @@ jobs:
JULIA_PKG_PRECOMPILE_AUTO: '0'
steps:
- uses: actions/checkout@3d3c42e5aac5ba805825da76410c181273ba90b1 # v7.0.1
- uses: julia-actions/setup-julia@fa02766e078afaaf09b14210362cee14137e6a32 # v3.0.2
# julia-actions/* is refused by the repository's Actions allow-list
# (startup_failure), so Julia is installed from the official binaries
# with checksum verification instead -- same version and procedure as
# ci.yml's "Set up Julia" step, which test/unit/test_install_pins.jl pins.
- name: Set up Julia
run: |
set -euo pipefail
JULIA_VERSION="1.12.5"
archive="julia-${JULIA_VERSION}-linux-x86_64.tar.gz"
base="https://julialang-s3.julialang.org/bin"
curl --fail --location --retry 3 --retry-all-errors --max-time 600 \
"${base}/linux/x64/${JULIA_VERSION%.*}/${archive}" \
-o "${RUNNER_TEMP}/${archive}"
curl --fail --location --retry 3 --retry-all-errors --max-time 120 \
"${base}/checksums/julia-${JULIA_VERSION}.sha256" \
-o "${RUNNER_TEMP}/julia-${JULIA_VERSION}.sha256"
grep "${archive}" "${RUNNER_TEMP}/julia-${JULIA_VERSION}.sha256" \
| (cd "${RUNNER_TEMP}" && sha256sum --check)
mkdir -p "${RUNNER_TEMP}/julia"
tar -xzf "${RUNNER_TEMP}/${archive}" -C "${RUNNER_TEMP}/julia" --strip-components=1
echo "${RUNNER_TEMP}/julia/bin" >> "${GITHUB_PATH}"
- name: Cache Julia packages
uses: actions/cache@55cc8345863c7cc4c66a329aec7e433d2d1c52a9 # v6.1.0
with:
version: '1.12.5'
- uses: julia-actions/cache@a7bed9df697e5d7309d68afe7542a87621a8b6c8 # v3.3.0
path: |
~/.julia/artifacts
~/.julia/packages
~/.julia/compiled
~/.julia/registries
key: julia-depot-${{ runner.os }}-${{ hashFiles('ui/Manifest.toml', 'ui/Project.toml') }}
restore-keys: |
julia-depot-${{ runner.os }}-
- name: Instantiate isolated UI environment
run: julia --project=ui -e 'using Pkg; Pkg.instantiate()'
- name: Test contracts and backend URL validation
Expand Down
11 changes: 9 additions & 2 deletions src/analysis/Execution.jl
Original file line number Diff line number Diff line change
Expand Up @@ -281,14 +281,21 @@ struct ExecutionManifest
if !haskey(prov, "config_hash")
prov["config_hash"] = config_hash
end
# Both probe fallbacks warn: a placeholder written silently makes the
# manifest look probed when it was not, which is exactly the
# concealment rule every fallback in this product is judged by
# (audit category: dependency_environment). The placeholder keeps the
# schema; the warning keeps the reason.
try
prov["metamanifold"] = probe_metamanifold()
catch
catch err
@warn "Metamanifold probe failed — manifest will record version=unknown" probe="metamanifold" err=sprint(showerror, err)
prov["metamanifold"] = OrderedDict("version" => "unknown")
end
try
prov["host"] = probe_host()
catch
catch err
@warn "Host probe failed — manifest will record hostname=unknown" probe="host" err=sprint(showerror, err)
prov["host"] = OrderedDict("hostname" => "unknown")
end

Expand Down
72 changes: 66 additions & 6 deletions test/unit/test_install_pins.jl
Original file line number Diff line number Diff line change
Expand Up @@ -29,10 +29,10 @@ const EXPECTED_PLATFORMS = ["linux-x86_64", "linux-aarch64", "macos-x86_64", "ma

is_sha256(s) = s isa AbstractString && occursin(r"^[0-9a-f]{64}$", s)

"""Return the first step of `job` whose `uses:` names `action`, or nothing."""
function ci_step_using(job, action)
"""Return the first step of `job` whose `name:` is `name`, or nothing."""
function ci_step_named(job, name)
for step in get(job, "steps", [])
startswith(get(step, "uses", ""), action) && return step
get(step, "name", nothing) == name && return step
end
return nothing
end
Expand Down Expand Up @@ -203,11 +203,22 @@ end
# Read from the `Set up Julia` step rather than from a matrix: the matrix was
# removed because GitHub appends a matrix combination to the posted check name
# (see "a required check name is a stable identifier" below). The step is located
# by its `uses:` rather than by index, so reordering the steps cannot make this
# by its name rather than by index, so reordering the steps cannot make this
# assertion quietly vanish.
setup = ci_step_using(job, "julia-actions/setup-julia")
#
# It used to be located by its `uses: julia-actions/setup-julia`, but that
# action is refused by the repository's Actions allow-list (see "every GitHub
# Action satisfies the repository Actions policy" below), so Julia is now
# installed by a pinned `run:` step whose JULIA_VERSION carries the copy this
# testset exists to keep honest.
setup = ci_step_named(job, "Set up Julia")
@test setup !== nothing
@test setup["with"]["version"] == pins["runtimes"]["julia"]["version"]
setup_run = setup === nothing ? "" : get(setup, "run", "")
julia_pin = match(r"JULIA_VERSION=\"([^\"]+)\"", setup_run)
@test julia_pin !== nothing
if julia_pin !== nothing
@test julia_pin[1] == pins["runtimes"]["julia"]["version"]
end

# A floating runner would carry the R apt pin, which names a 24.04 build, off to
# whatever the next LTS ships.
Expand Down Expand Up @@ -303,6 +314,55 @@ end
end
end

@testset "every GitHub Action satisfies the repository Actions policy" begin
# MEASURED 2026-09-25 22:19 UTC through 2026-09-27: every workflow run
# failed with `startup_failure` and zero jobs because the repository
# began enforcing an Actions allow-list. The run annotation reads:
# actions must be "from a repository owned by hyperpolymath, created by
# GitHub, verified in the GitHub Marketplace, or match the pattern"
# configured for the repository, and "all actions must also be pinned
# to a full-length commit SHA". A violation is not a red job -- it is a
# job that never starts, so nothing INSIDE the workflow can report it.
# This testset is where that policy becomes visible to `Pkg.test`.
#
# Local actions (`./...`) are part of the checked-out tree: always
# allowed, and there is no remote ref to pin.
github_owned_owners = ("actions", "github", "hyperpolymath")
# Marketplace-verified third parties used by this repository. Extend
# deliberately -- each entry is a claim that the action is verified,
# made here because the check itself cannot reach the Marketplace.
marketplace_verified = ("oven-sh/setup-bun",)

violations = String[]
workflows = sort(readdir(joinpath(REPO_ROOT, ".github", "workflows")))
@test !isempty(workflows)
for file in workflows
(endswith(file, ".yml") || endswith(file, ".yaml")) || continue
workflow = YAML.load_file(joinpath(REPO_ROOT, ".github", "workflows", file))
for (_, job) in get(workflow, "jobs", Dict())
for step in get(job, "steps", [])
uses = get(step, "uses", nothing)
uses === nothing && continue
startswith(uses, "./") && continue
parts = split(uses, '@'; limit = 2)
if length(parts) != 2
push!(violations, "$file: $uses has no @ref")
continue
end
src, ref = parts
if !occursin(r"^[0-9a-f]{40}$", ref)
push!(violations, "$file: $uses is not pinned to a full-length commit SHA")
end
owner = first(split(src, '/'))
if !(owner in github_owned_owners || src in marketplace_verified)
push!(violations, "$file: $uses is neither github-owned, hyperpolymath-owned, nor on the verified list")
end
end
end
end
@test isempty(violations)
end

@testset "a required check name is a stable identifier" begin
ci = YAML.load_file(CI_PATH)

Expand Down
Loading