Something went wrong. Try again.
The Monad language. Dependent types, functional programming compiled with LLVM. Hobby project. monad-lang.org
dependent-types language compiler programming-language functional-programming
Something went wrong. Try again.
123456789101112131415161718192021222324252627282930313233343536373839404142434445464748495051525354555657585960616263646566676869707172737475767778798081828384858687888990#!/usr/bin/env bash# Does this change touch anything that can move the compiler? Prints `true`# or `false` on stdout and ALWAYS exits 0, so a caller can put the answer# straight into `$GITHUB_OUTPUT` without a failing status turning the step# red. Usage:## scripts/ci-compiler-relevant.sh <base-revision> [head-revision]## It exists because the two expensive CI jobs (`test`, 54 min, and# `bootstrap`, 22 min) cannot be affected by a change that only touches# prose -- and a docs-only change is exactly the traffic that fills the# runner queue, where every queued minute is paid by an unrelated branch.## A workflow-level `paths-ignore` would be shorter and is WRONG here, for# two reasons that were checked rather than assumed:## * `docs-check` is a pre-commit hook (devenv.nix -> scripts/check-docs.sh,# which type-checks every code block under docs/). So a docs-only change# is NOT a change CI can ignore wholesale: it still needs the# `pre-commit-checks` job. A workflow-level filter would skip that too,# which is a missed signal rather than a saving. Only the two compiler# jobs are gated, and this script only decides whether they can see the# change.## That is the ONLY docs gate in this repository, which is why the point# is not academic: `gh workflow list --all` reports just three workflows# here -- CI, "Nightly release" (active, but its single job is gated on# `github.repository == 'monad-lang/monad'`, never this remote, so it runs# nothing) and "Deploy mdBook site to Pages" (disabled_manually, and it# builds and deploys a site rather than checking any code block). Round# 1's changes to those two files are unobservable in this repository.# * `paths-ignore` on `pull_request` skips the whole workflow, and a# skipped workflow leaves its required status checks PENDING -- GitHub's# documented behaviour -- so on a repository with required checks the# filter blocks the merge instead of saving an hour. Whether this# repository has them could not be verified from here (the PAT is not# allowed to read branch protection), so the design has to be correct# either way: a job-level skip reports a verdict.## A third reason is local to this corpus: `bench/` and `proofs/` are in# `check-monad-tests.sh`'s `corpus_dirs`, so their `.mo` files ARE swept.# Ignoring those trees wholesale would skip real signal; only their markdown# is ignorable, which is what the `*.md` rule below does.## THE DECISION FAILS OPEN. An empty diff, an all-zeros or unreachable base# (`github.event.before` on a new branch), an unknown event, or any git# error all answer `true`. That is the only acceptable direction: a# misclassification may then cost an hour of runner time, never a missed# failure. The rules below are the paths a change can touch without the# compiler reading them -- markdown in any directory, the generated mdbook# under docs/, and files no build in this repository opens.set -euo pipefail
base="${1:-}"head="${2:-HEAD}"
files=""if [ -n "$base" ] && ! printf '%s' "$base" | grep -qE '^0+$' \ && git rev-parse --verify --quiet "${base}^{commit}" > /dev/null 2>&1; then files="$(git diff --name-only "$base" "$head" 2> /dev/null)" || files=""fi
if [ -z "$files" ]; then echo true exit 0fi
while IFS= read -r path; do [ -n "$path" ] || continue case "$path" in # Markdown is prose wherever this repository keeps it: the root # README/AGENTS/CODE_OF_CONDUCT, docs/src's book sources, the # per-directory READMEs, and .claude-plugin's. *.md) ;; # The mdbook's config and its COMMITTED build output (docs/book/*.html). # Generated, and nothing compiles it -- mdbook.yml is disabled_manually. docs/*) ;; # Opened by no nix expression, script or hook in the tree: nix's # `meta.license` names a nixpkgs value, not this file, and the ignore # rules are consumed by git itself. LICENSE | .gitignore) ;; # Agent/plugin configuration. Not read by any CI step -- the pre-commit # hooks come from .pre-commit-config.yaml, generated by devenv. .claude-plugin/*) ;; *) echo true; exit 0 ;; esacdone <<< "$files"
echo false