Say what things are, not what they are not

records/agent.json

@@ -1,10 +1,10 @@
 {
   "recorded": {
-    "compiler": "iyi 0.12.0 (built on Crystal 1.22.0-dev [44b843563] (2026-09-11))",
-    "commit": "44b8435633d47d2d3ba2106abe86e0ea1188257f",
+    "compiler": "iyi 0.13.0 (built on Crystal 1.22.0-dev [1f79e251a] (2026-09-16))",
+    "commit": "1f79e251ae76b1ce03c398dc99675529f1b31825",
     "machine": "Linux 7.2.4-1-cachyos x86_64, AMD Ryzen AI 9 465 w/ Radeon 880M",
     "command": "npm run record:agent",
-    "when": "2026-09-12T16:06:28.321Z"
+    "when": "2026-09-20T11:18:01.910Z"
   },
   "project": [
     {
@@ -44,7 +44,7 @@
       "command": "iyi mod context --json app.iyi",
       "exitCode": 0,
       "payload": "stdout",
-      "stdout": "{\"file\":\"agent/app.iyi\",\"imports\":[{\"import\":\"app/greeter\",\"api\":{\"module\":\"app/greeter\",\"interface_hash\":\"90e5d376253c2ff8727008aaba9fece1\",\"functions\":[{\"name\":\"polite\",\"parameters\":[\"name : String\"],\"returns\":\"String\",\"doc\":\"The exported surface carries its doc comment, so the grounding pack an agent\\nreads says what the function is for and not only what it takes.\",\"rendered\":\"def polite(name : String) : String\"},{\"name\":\"shout\",\"parameters\":[\"name : String\"],\"returns\":\"String\",\"rendered\":\"def shout(name : String) : String\"}],\"types\":[{\"name\":\"Greet\",\"kind\":\"trait\",\"visibility\":\"pub\",\"methods\":[{\"name\":\"greet\",\"parameters\":[],\"returns\":\"String\",\"required\":true,\"rendered\":\"abstract def greet : String\"}]}],\"impls\":[]}}]}\n",
+      "stdout": "{\"file\":\"agent/app.iyi\",\"imports\":[{\"import\":\"app/greeter\",\"api\":{\"module\":\"app/greeter\",\"interface_hash\":\"14c937d996cd42f50dcce4594c179cca\",\"functions\":[{\"name\":\"polite\",\"parameters\":[\"name : String\"],\"returns\":\"String\",\"doc\":\"The exported surface carries its doc comment, so the grounding pack an agent\\nreads says what the function is for and not only what it takes.\",\"rendered\":\"def polite(name : String) : String\"},{\"name\":\"shout\",\"parameters\":[\"name : String\"],\"returns\":\"String\",\"rendered\":\"def shout(name : String) : String\"}],\"types\":[{\"name\":\"Greet\",\"kind\":\"trait\",\"visibility\":\"pub\",\"methods\":[{\"name\":\"greet\",\"parameters\":[],\"returns\":\"String\",\"required\":true,\"rendered\":\"abstract def greet : String\"}]}],\"impls\":[]}}]}\n",
       "stderr": ""
     },
     {
@@ -104,7 +104,7 @@
       "command": "iyi test --json .",
       "exitCode": 0,
       "payload": "stdout",
-      "stdout": "{\"tests\":[{\"file\":\"./app_test.iyi\",\"status\":\"pass\",\"seconds\":0.229}],\"passed\":1,\"failed\":0,\"skipped\":0}\n",
+      "stdout": "{\"tests\":[{\"file\":\"./app_test.iyi\",\"status\":\"pass\",\"seconds\":0.27}],\"passed\":1,\"failed\":0,\"skipped\":0}\n",
       "stderr": ""
     },
     {
@@ -135,7 +135,7 @@
     "bytes": 731,
     "sourceBytes": 707,
     "interfaceHashes": {
-      "app/greeter": "90e5d376253c2ff8727008aaba9fece1"
+      "app/greeter": "14c937d996cd42f50dcce4594c179cca"
     }
   },
   "suggested": [
@@ -167,7 +167,7 @@
       },
       "serverInfo": {
         "name": "iyi",
-        "version": "0.12.0"
+        "version": "0.13.0"
       }
     },
     "tools": [

records/diagnostics.json

@@ -1,10 +1,10 @@
 {
   "recorded": {
-    "compiler": "iyi 0.12.0 (built on Crystal 1.22.0-dev [44b843563] (2026-09-11))",
-    "commit": "44b8435633d47d2d3ba2106abe86e0ea1188257f",
+    "compiler": "iyi 0.13.0 (built on Crystal 1.22.0-dev [1f79e251a] (2026-09-16))",
+    "commit": "1f79e251ae76b1ce03c398dc99675529f1b31825",
     "machine": "Linux 7.2.4-1-cachyos x86_64, AMD Ryzen AI 9 465 w/ Radeon 880M",
     "command": "npm run record:diagnostics",
-    "when": "2026-09-12T16:06:26.670Z"
+    "when": "2026-09-20T11:18:00.000Z"
   },
   "cases": [
     {

scripts/download.mjs

@@ -100,12 +100,16 @@ const verify = span(installer, INSTALLER, "verify", /^# The checksum line for th
 // The release job that writes the file the installer looks for. Anchored on
 // the `cat` as well, because an earlier job writes SHA256SUMS too: it is the
 // one that proves the refusal, below, and matching it here would have quoted
-// fifty lines of the wrong job.
+// fifty lines of the wrong job. The globs it sums are not spelled out: one
+// SHA256SUMS covers every archive a release publishes, so 472e2ba1a added
+// `*.zip` beside `*.tar.gz` and this anchor has no business caring. What it
+// cares about is that the release job still writes that one file and prints
+// it.
 const publish = span(
   workflow,
   WORKFLOW,
   "publish",
-  /sha256sum \*\.tar\.gz > SHA256SUMS && cat SHA256SUMS/,
+  /sha256sum [^>]*> SHA256SUMS && cat SHA256SUMS/,
   /gh release create/,
 );
 
@@ -176,7 +180,7 @@ if (!refused) die(`${INSTALLER}'s uname case no longer ends in a die, so a machi
 // is that these are one file.
 const wantedFile = /-o "\$tmp\/([A-Za-z0-9._]+)"/.exec(verify.text);
 if (!wantedFile) die(`${INSTALLER}'s verification no longer downloads a file this script can name`);
-const writtenFile = /sha256sum \*\.tar\.gz > ([A-Za-z0-9._]+)/.exec(publish.text);
+const writtenFile = /sha256sum [^>]*> ([A-Za-z0-9._]+)/.exec(publish.text);
 if (!writtenFile) die(`${WORKFLOW}'s release job no longer writes a checksum file this script can name`);
 if (wantedFile[1] !== writtenFile[1]) {
   die(

scripts/install-targets.mjs

@@ -28,10 +28,19 @@
 //     shown, so the site restates the repository rather than one file of it;
 //   * README.md's own platform words under the one-liner ("Linux x86-64 and
 //     macOS arm64"), which is where the prose name beside each target comes
-//     from. It is matched back to a target by scoring the target's own `uname`
-//     components against the phrase's words, so the only spellings this file
-//     knows are the two aliases below. An unmatched or ambiguous phrase fails
-//     and names itself; it is never guessed.
+//     from. They are found by the fenced block that holds the `install.sh`
+//     one-liner rather than by the clause that used to follow them, because
+//     what follows is prose about other platforms and moves: 48bc8d0b5 put a
+//     PowerShell block between the sentence and the clause this once matched.
+//     What does not move is that the sentence sits directly under the command
+//     it qualifies. Each phrase is matched back to a target by scoring the
+//     target's own `uname` components against the phrase's words, so the only
+//     spellings this file knows are the two aliases below. An unmatched or
+//     ambiguous phrase fails and names itself; it is never guessed;
+//   * install.sh is the only installer read here. Windows has its own
+//     (install.ps1) and its own archive, a zip rather than a tarball, so it is
+//     not one of this record's targets and src/lib/release.ts builds no URL
+//     for it.
 //
 // WHAT IT DOES NOT DO. It does not check that a release actually published the
 // tarballs, or that a URL resolves. It checks that the site offers exactly what
@@ -155,15 +164,17 @@ if (undocumented.length > 0) {
   );
 }
 
-/* The platform words, out of the sentence under README's one-liner. Anchored on
- * the clause that follows them, because the sentence is prose and a looser
- * match would drag half a paragraph in. */
-const prose = /\.? ([A-Z][^.;]*?); the tarball by hand/.exec(readme);
+/* The platform words, out of the sentence under README's one-liner. Anchored
+ * on the one-liner's own fenced block: the sentence a reader is shown is the
+ * one directly under the command, and the first sentence after the fence is
+ * it. Anchoring on what comes after instead put this at the mercy of a
+ * paragraph about a platform this record does not carry. */
+const prose = /install\.sh \| sh[^`]*``` ([A-Z][^.;]*)[.;]/.exec(readme);
 if (!prose) {
   throw new Error(
-    `install-targets: ${CLAIM} no longer names the platforms under its ` +
-      `one-liner ("... ; the tarball by hand"), so there is no sentence in ` +
-      `the repository to take the prose name of each target from.`,
+    `install-targets: ${CLAIM} no longer states the platforms in a sentence ` +
+      `under the fenced ${SOURCE} one-liner, so there is no sentence in the ` +
+      `repository to take the prose name of each target from.`,
   );
 }
 const phrases = prose[1].split(/\s*(?:,|and)\s*/).filter(Boolean);

scripts/project.mjs

@@ -47,7 +47,7 @@ const DOCUMENTS = [
   { id: "contributing", file: "CONTRIBUTING.md", blurb: "What a change to this repository is expected to come with." },
   { id: "security", file: "SECURITY.md", blurb: "Where a vulnerability goes, and which of the two trackers is the right one." },
   { id: "conduct", file: "CODE_OF_CONDUCT.md", blurb: "The Contributor Covenant, and the address that enforces it here." },
-  { id: "notice", file: "NOTICE.md", blurb: "Crystal's copyright, the licence, and every library the compiler links." },
+  { id: "notice", file: "NOTICE.md", blurb: "Crystal's copyright, the license, and every library the compiler links." },
 ];
 
 const commit = execFileSync("git", ["-C", repo, "rev-parse", "HEAD"], {

scripts/samples.mjs

@@ -2,12 +2,25 @@
 // Transcludes the repository's own text into JSON the site imports. Nothing a
 // lesson shows as code is typed into the lesson. Two kinds of text arrive here:
 //
-//   1. The sample programs under `samples/iyi` in the iyi repository, and the
-//      tour under `samples/tour` in this one. A lesson names a file, a named
-//      top-level declaration in it, or a content-anchored span of it, and the
-//      build reads that text out of the file at that moment. A sample that
-//      changes in the repository changes on the site. A sample that is renamed
-//      or deleted fails the build, naming the lesson that asked for it.
+//   1. The sample programs under `samples/iyi` in the iyi repository, read at
+//      the tag CHANGELOG.md names, and the tour under `samples/tour` in this
+//      one, read off disk. A lesson names a file, a named top-level
+//      declaration in it, or a content-anchored span of it, and the build
+//      reads that text out of the tree that ships it. A sample a release
+//      renamed or dropped fails the build, naming the lesson that asked for
+//      it.
+//
+//      WHY THE TAG RATHER THAN THE CHECKOUT. Every listing is painted with
+//      the tokens in `records/highlight.json`, which
+//      `scripts/record-highlight.mjs` records from a release and
+//      `scripts/records.mjs` checks against that release. Indexing the text
+//      from master instead left the site holding two readings of one program
+//      the moment a commit after the tag touched a sample, and `Sample.astro`
+//      compares them: the build stopped, correctly, about the wrong pair of
+//      files. The line `scripts/records.mjs` draws is drawn here too -
+//      `samples/iyi/` is the iyi tree's and is read at the release, and this
+//      repository's own files are in front of you and move when you move
+//      them.
 //   2. The console recordings in README.md. A lesson names a block by an anchor
 //      string, and that anchor has to appear in exactly one fenced block in the
 //      whole README. The block travels with the line numbers it was quoted
@@ -27,6 +40,7 @@ import {
 } from "node:fs";
 import { dirname, join, relative, resolve } from "node:path";
 import { fileURLToPath } from "node:url";
+import { blobAt, releaseRef, treeAt } from "./release-ref.mjs";
 
 const here = dirname(fileURLToPath(import.meta.url));
 const repo = process.env.IYI_REPO ? resolve(process.env.IYI_REPO) : resolve(here, "..", "..", "iyi");
@@ -40,7 +54,8 @@ const die = (message) => {
 // Samples ------------------------------------------------------------------
 
 const site = resolve(here, "..");
-const samplesRoot = resolve(repo, "samples", "iyi");
+const release = releaseRef(repo);
+const samplesRoot = `${release.tag}:samples/iyi`;
 const tourRoot = resolve(site, "samples", "tour");
 
 function walk(dir) {
@@ -107,22 +122,31 @@ function regionsOf(lines) {
   return { regions, ambiguous: [...ambiguous].sort() };
 }
 
-const samples = {};
-for (const [root, tree] of [[samplesRoot, repo], [tourRoot, site]]) {
-  for (const file of walk(root)) {
-    const path = relative(resolve(tree, "samples"), file).split("\\").join("/");
-    const text = readFileSync(file, "utf8");
-    const lines = text.replace(/\n$/, "").split("\n");
-    const { regions, ambiguous } = regionsOf(lines);
+/* Two trees, read two ways, for the reason at the top of this file. `git
+ * ls-tree` sorts, which is what `walk` does to a directory, so the index is in
+ * one order whichever side a program came from. */
+const indexed = [
+  ...treeAt(repo, release.tag, "samples/iyi")
+    .filter((path) => path.endsWith(".iyi"))
+    .map((path) => [path, blobAt(repo, release.tag, path).toString("utf8")]),
+  ...walk(tourRoot).map((file) => [
+    relative(site, file).split("\\").join("/"),
+    readFileSync(file, "utf8"),
+  ]),
+];
 
-    samples[path] = {
-      path: `samples/${path}`,
-      text,
-      lines: lines.length,
-      regions,
-      ambiguous,
-    };
-  }
+const samples = {};
+for (const [path, text] of indexed) {
+  const lines = text.replace(/\n$/, "").split("\n");
+  const { regions, ambiguous } = regionsOf(lines);
+
+  samples[path.replace(/^samples\//, "")] = {
+    path,
+    text,
+    lines: lines.length,
+    regions,
+    ambiguous,
+  };
 }
 
 if (Object.keys(samples).length === 0) {
@@ -443,8 +467,19 @@ if (missing.length > 0) {
   );
 }
 
+/* Where a citation is checked follows what the citation is. A sample is shown
+ * from the release, so it has to be in the release. This repository's own
+ * files, and the rest of the iyi checkout a lesson stands on - SPEC.md, a
+ * bench script, a compiler pass - are cited as they stand and are checked
+ * where they stand, which is the tree scripts/facts.mjs and
+ * scripts/proofs.mjs read as well. */
+const cited = (path) => {
+  if (path.startsWith("samples/iyi/")) return blobAt(repo, release.tag, path) !== null;
+  return existsSync(resolve(path.startsWith("records/") ? site : repo, path));
+};
+
 const absentSources = [...claimedSources]
-  .filter(([path]) => !existsSync(resolve(path.startsWith("records/") ? resolve(here, "..") : repo, path)))
+  .filter(([path]) => !cited(path))
   .map(([path, where]) => `${path} (cited by ${[...where].join(", ")})`);
 if (absentSources.length > 0) {
   die(

src/content/learn/declarations-not-bodies.mdx

@@ -33,11 +33,10 @@ This is the step the language exists for. Everything else in iyi, the `pub`
 signatures, the traits, the orphan rule, is here to make it hold.
 
 Two files are enough to show it, so start with the one being imported. Every iyi
-file opens by saying which module it is, and that line is not a namespace
-declaration you can put anywhere. It is the compilation unit's name, it is
-absolute, and it tells you where the file sits: a module called `app/greeter`
-lives at `app/greeter.iyi`, resolved from the project root and never relative to
-whoever imports it. No manifest, no include path, no search order.
+file opens by naming its compilation unit, and that name is absolute. It tells
+you where the file sits: a module called `app/greeter` lives at
+`app/greeter.iyi`, resolved from the project root and never relative to whoever
+imports it. No manifest, no include path, no search order.
 
 <Sample path="samples/iyi/app/greeter.iyi" />
 
@@ -89,7 +88,7 @@ Two files is a demonstration. A web framework is a test.
 lives in `samples/iyi/kemal`. That whole directory goes away between the two
 builds, and the program still builds, links, runs, and prints the same output.
 
-## It is a gate, not a slogan
+## The roundtrip gate
 
 `bench/samples_roundtrip.sh` is where the claim stops being prose. For every
 sample that imports a module it builds with `--emit-iyimod`, runs the binary, and
@@ -99,9 +98,9 @@ each sample again with `--use-iyimod`, runs that second binary, and diffs the tw
 outputs. Any sample that fails to build either way, or prints something
 different, exits the script non zero. README.md says CI runs it on every push.
 
-Look at what the diff compares. Not that both builds succeeded, which would only
-prove the front end swallowed the artifacts. That both programs ran, and printed
-the same thing. The script's own header is blunt about why the deletion is the
+Look at what the diff compares: that both programs ran, and printed the same
+thing. Merely checking that both builds succeeded would only prove the front
+end swallowed the artifacts. The script's own header is blunt about why the
 whole test: the only way to be sure a consumer never reads a dependency's source
 is to take the source away and see whether the build still produces a program
 that behaves.
@@ -110,13 +109,12 @@ What that boundary saves in seconds belongs to a machine rather than to a
 language, so this page will not quote you a number. README.md publishes them with
 the machine attached and the command that measures them.
 
-## The clause the deletion did not use
+## Acyclic imports
 
-Read the premise at the top of this page again. It is three sentences, and the
-deletion proves the third. The second one, that `import` forms a DAG, is
-enforced long before any of that, and it has to be: a module initialises after
-every module it imports, so two modules that wait for each other have no order
-to be initialised in and there is no build to have.
+The rule that `import` forms a DAG is enforced long before any of that, and it
+has to be: a module initializes after every module it imports, so two modules
+that wait for each other have no order to be initialized in and there is no
+build to have.
 
 Write one anyway and the compiler declines, draws the cycle it found, and names
 the move that fixes it.

src/content/learn/errors-are-values.mdx

@@ -9,7 +9,7 @@ bought: >-
   Nothing was built for this. Exhaustiveness was already in the language and
   unions already carried a type id, so adding an error member to an exported
   signature turns every incomplete `case` on it into a compile error, and an
-  error a caller has not handled cannot reach production quietly.
+  error a caller has not handled cannot reach production.
 sources:
   - file: samples/iyi/errors.iyi
     note: the two producers, the propagating call, the exhaustive case, and what `.or` and `.or_panic` are
@@ -83,7 +83,7 @@ incomplete `case` on it stops compiling.
 Sometimes you want the value or a default. `.or` takes the default, `.or_panic`
 takes the value or dies.
 
-Neither can be an ordinary method, and the reason is worth understanding. A real
+Neither can be an ordinary method: a real
 method call on `Int32 | IOError` would demand that method from both members, and
 a method every error type has to supply is exactly what this design avoids. So
 the compiler knows these two by name, which is also why `or` and `or_panic` are
@@ -94,7 +94,7 @@ instead of being computed: the default's type unioned with the non-error members
 `.or_panic` yields the non-error members alone, because what it calls never
 returns.
 
-## What this does not do yet
+## Limits
 
 Panics. They are meant to be catchable only at task boundaries, and what a task
 boundary is has not been specified. Until it is, `.or_panic` raises a Crystal