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.
123456789101112131415161718192021222324252627282930313233343536373839404142434445464748495051525354555657585960616263646566676869707172737475767778798081828384858687888990919293949596979899100101102103104105106107108109110111112113114115116117118119120121122123124125126127128129130131132133134135136137138139140141142143144145146147148149150151152153154155156157158159160161162163164165166167168169170171172173174175176177178179180181182183184185#!/usr/bin/env bash# Type-check every Monad code block in the mdBook under docs/.## `mdbook build` only renders markdown -- it never compiles the code inside# the chapters, which is how the book drifted far enough from the compiler# that most of its samples stopped parsing. This script closes that gap.## A fenced block tagged ```monad is extracted to its own .mo file and run# through `check`. A block tagged ```monad,ignore is skipped: that tag is# for samples that are deliberately not valid today -- syntax the docs# describe as unimplemented, or fragments shown for illustration -- and# every one of them should have prose next to it saying so.## WHICH FILES, AND WHICH DEFAULT## docs/src/*.md OPT-OUT. ```monad is checked, ```monad,ignore skips.# The chapters are mostly runnable samples, so checking# is the right default.## AGENTS.md OPT-IN. ```monad is SKIPPED, ```monad,check asks for it.# AGENTS.md is prose written for contributors and agents,# and most of its fences are FRAGMENTS that cannot be a# file at all: bare expressions, a literal `...`, blocks# whose own next line says they are invalid, blocks that# redefine a prelude name. Compiling them all is not# possible, and mass-tagging them `monad,ignore` would# break the rule above -- an ignore tag means "there is# prose here saying why this is not valid", and for a# fragment there is nothing to say.## So AGENTS.md is opt-in, and the fences worth checking are the ones that# make a CLAIM a reader would copy: a `use` line, a declaration form, a# complete example. That is the class that has actually been wrong here --# AGENTS.md carried a `use` spelling neither compiler accepts, for months,# while every gate was green (this script never opened the file).## ```monad,check is honoured in docs/src too, so a chapter can opt a# fragment in for the same reason.## Blocks are checked in isolation, so each ```monad block must stand on its# own: its own `use`/`open` lines, its own type annotations. That is a# feature, not a limitation -- a reader copying one block into a file gets# exactly what the checker saw.## Two modes. The default uses the Rust bootstrap host, which is fast and is# what the pre-commit hook runs:## scripts/check-docs.sh## The book documents the SELF-HOSTED compiler, though, so the stricter check is# to point MONAD_BIN at a bootstrapped `monad` binary:## MONAD_BIN=/path/to/monad scripts/check-docs.sh## Both binaries take the same `check <paths>...` shape and the same exit codes,# so no other change is needed. The self-hosted run is expected to be GREEN:# every construct this header used to tolerate a failure for -- `#[derive]`, a# `\u{...}` escape, a dotted instance name, a call relying on a brace# parameter's default -- now checks self-hosted. Measured 2026-09-23 with a# binary built from the tree: 114 block(s) checked, 0 error(s). Anything it# reports is therefore a real problem, and docs/src/bootstrap-host.md is where# the differences that remain between the two compilers are recorded.## The reverse also exists, which is why a few blocks are tagged# ```monad,ignore even though they are correct: a multiplicity prefix on a# destructured parameter parses self-hosted and is a parse error on the host.## Module resolution is relative to the working directory, so this must run# from the repository root (it cd's there itself).
set -euo pipefail
cd "$(dirname "$0")/.."
# Overridable so local runs can use an already-installed `monad-rs` instead# of paying for a cargo rebuild: MONAD_BIN=monad-rs scripts/check-docs.shMONAD_BIN=${MONAD_BIN:-"cargo run --release --quiet --"}
work=$(mktemp -d)trap 'rm -rf "$work"' EXIT
total=0skipped=0declare -a blocks=()declare -a origins=()
for md in docs/src/*.md AGENTS.md; do [ -f "$md" ] || continue # Resolved BEFORE the loop, not inside it: a `$(basename "$md" ...)` in the # body of a `while ... done < "$md"` reads as writing the file it redirects # from (shellcheck SC2094), which it isn't. stem=$(basename "$md" .md) # Which default this file gets -- see the header. `docs/src` is the book and # is checked by default; everything else must ask. case "$md" in docs/src/*) default=check ;; *) default=skip ;; esac # State machine over the file: `fence` holds the info string of the block # we're inside ("" when outside one), `start` its opening line number. fence="" start=0 buf="" lineno=0 while IFS= read -r line || [ -n "$line" ]; do lineno=$((lineno + 1)) if [ -z "$fence" ]; then case "$line" in '```'*) fence=${line#'```'} start=$lineno buf="" ;; esac continue fi if [ "$line" = '```' ]; then case "$fence" in monad) if [ "$default" = check ]; then total=$((total + 1)) f="$work/${stem}_$start.mo" printf '%s' "$buf" > "$f" blocks+=("$f") origins+=("$md:$start") else skipped=$((skipped + 1)) fi ;; monad,check) total=$((total + 1)) f="$work/${stem}_$start.mo" printf '%s' "$buf" > "$f" blocks+=("$f") origins+=("$md:$start") ;; monad,ignore) skipped=$((skipped + 1)) ;; esac fence="" continue fi buf+="$line"$'\n' done < "$md"done
if [ "$total" -eq 0 ] && [ "$skipped" -eq 0 ]; then echo "check-docs: no \`\`\`monad blocks found at all -- is the tag right?" >&2 exit 1fi
echo "check-docs: checking $total block(s), skipping $skipped"
# One `check` invocation over every block: it reports per-file diagnostics# already, and paying the module-loading cost once instead of N times takes# this from minutes to seconds.if out=$($MONAD_BIN check "${blocks[@]}" 2>&1); then echo "$out" | tail -1 echo "check-docs: OK" exit 0fi
echo "$out"echoecho "check-docs: FAILED -- the block(s) above came from:" >&2# Only the blocks the diagnostics actually named. Listing all of them buries# the failure under every origin in the book, and the diagnostic does name the# block's file, so a substring test on the basename finds the right ones.# If nothing matches -- a `check` that failed without naming a file, say -- fall# back to the full list rather than printing nothing.found_all=0for i in "${!blocks[@]}"; do if grep -qF "$(basename "${blocks[$i]}")" <<<"$out"; then echo " $(basename "${blocks[$i]}") <- ${origins[$i]}" >&2 found_all=1 fidoneif [ "$found_all" -eq 0 ]; then for i in "${!blocks[@]}"; do echo " $(basename "${blocks[$i]}") <- ${origins[$i]}" >&2 donefiexit 1