Move the pin to v0.2.4

README.md

@@ -25,7 +25,7 @@ Concretely, that rules out a few things that would otherwise be tempting:
   pages the compiler generates rather than a list maintained here.
 - No examples written here. The playground's are the compiler's corpus at the
   pinned tag, and the summary under each one is the comment at the top of the
-  file. Which twelve of them the picker offers is a choice made here, and it is
+  file. Which thirteen of them the picker offers is a choice made here, and it is
   the only one: choosing what to show is not writing it, and every file is
   still served. The landing page's program is the exception, and it is short
   and its refusal was still produced by running it.
@@ -92,13 +92,13 @@ Everything in it comes from somewhere else: each summary is the comment at the
 top of the file, and the rest is what the pinned artifact answered when asked.
 
 What it was asked matters, because "can this be run" has two halves here.
-Twenty-one of the twenty-eight have no `main` at all. Six of the remaining
+Twenty-two of the twenty-nine have no `main` at all. Six of the remaining
 seven have one and want the filesystem, which a page does not have, so `needs`
 records the capabilities they asked for. That leaves exactly one example this
-page can start, and Run is off for the other twenty-seven with the reason
+page can start, and Run is off for the other twenty-eight with the reason
 beside it, rather than letting somebody press it and be refused.
 
-The picker shows twelve of the twenty-eight, and that list is in
+The picker shows thirteen of the twenty-nine, and that list is in
 `tools/artifact.mjs` because both tools need it. The corpus is not a menu:
 about half of it is one language feature at a time, written so the compiler's
 own tests have something to read, and a visitor scrolling past `sink`, `names`
@@ -113,7 +113,7 @@ corpus no longer has, so a promoted or deleted example shortens the menu
 loudly.
 
 `greeting.deed` is left out because it imports two other modules and this page
-hands the compiler one file. That is the only one: the other twenty-eight were
+hands the compiler one file. That is the only one: the other twenty-nine were
 checked through the pinned artifact and every one of them is clean.
 
 ## Layout
@@ -144,7 +144,7 @@ the release the pin names, and the example index still says what the compiler
 says.
 
 That last part is not a shape check. It loads the pinned artifact, asks it its
-version, and asks it about all twenty-eight examples, because a committed wasm
+version, and asks it about all twenty-nine examples, because a committed wasm
 is a file nothing here ever built: a truncated copy, or a different build
 wearing the right name, spells its filename correctly and passes everything
 else. It runs on every pull request too.

assets/errors.js

@@ -5,8 +5,8 @@
 // artifact carries all of them, so this page cannot document a code the
 // compiler does not have, or miss one it does.
 
-const TAG = "v0.2.3";
-const VERSION = "0.2.3";
+const TAG = "v0.2.4";
+const VERSION = "0.2.4";
 const WASM_URL = `../assets/deed-${TAG}-wasm32-unknown-unknown.wasm`;
 
 const STATUS = document.getElementById("status");

assets/play.js

@@ -13,8 +13,8 @@
 // release, because a release asset cannot be fetched from a browser at all:
 // both the download URL and the API one redirect to a host that sends no
 // `Access-Control-Allow-Origin`. See decisions/2026-07-31-no-build-step.md.
-const TAG = "v0.2.3";
-const VERSION = "0.2.3";
+const TAG = "v0.2.4";
+const VERSION = "0.2.4";
 const WASM_URL = `../assets/deed-${TAG}-wasm32-unknown-unknown.wasm`;
 
 const SOURCE = document.getElementById("source");

examples/index.json

@@ -1,5 +1,5 @@
 {
-  "tag": "v0.2.3",
+  "tag": "v0.2.4",
   "examples": [
     {
       "file": "calculator.deed",
@@ -146,7 +146,7 @@
     },
     {
       "file": "proven.deed",
-      "shown": 11,
+      "shown": 12,
       "summary": "The Proven tier, which is the part of this language that is supposed to be interesting.",
       "runs": false,
       "needs": [],
@@ -192,6 +192,14 @@
       "needs": [],
       "tests": 7
     },
+    {
+      "file": "tasks.deed",
+      "shown": 11,
+      "summary": "Tasks, out of the library.",
+      "runs": false,
+      "needs": [],
+      "tests": 2
+    },
     {
       "file": "tic_tac_toe.deed",
       "shown": 1,

examples/proven.deed

@@ -118,6 +118,29 @@ fn unbounded_span(low: Int, high: Int) -> Positive
     high - low
 }
 
+// Proven from a bound the program can name. `Int` is a signed 64-bit integer
+// and until `Int.max` existed there was no way to say so: the clause had to
+// carry the nineteen digits, or the function had to be written without a
+// bound and take the runtime check.
+//
+// The bound is what makes this Proven rather than Guarded. `n + 100` on an
+// unbounded `n` has no answer at the top of the range, and overflow stops the
+// program rather than wrapping, so the checker is right to want it said.
+fn headroom(n: Int) -> Positive
+  where
+    n >= 0,
+    n <= Int.max - 100,
+{
+    n + 100
+}
+
+// The other end, which is the one with no literal. Negation is an operator
+// rather than part of a literal, so the digits of the smallest `Int` are one
+// past the largest and there is nothing a literal alone could say.
+fn is_the_floor(n: Int) -> Bool {
+    n == Int.min
+}
+
 // Proven across a call. `always_one` promises what it returns, the promise is
 // read here, and the proof one function did is worth something to the next.
 // Without this every abstraction boundary would restart the reasoning from
@@ -354,6 +377,11 @@ test "the guarded ones are checked when they run" {
     assert one_more(1) == 2
     assert unbounded_span(2, 5) == 3
     assert squared(7) == 49
+    assert headroom(5) == 105
+    assert is_the_floor(Int.min)
+    assert !is_the_floor(0)
+    assert to_string(Int.min) == "-9223372036854775808"
+    assert Int.max == 9223372036854775807
 }
 
 // The half that was missing. Every one of these is a `Guarded` obligation

examples/scheduler.deed

@@ -32,22 +32,27 @@
 //
 // It is also not a library, and the reason is worth being exact about, because
 // "concurrency is a library here" is the claim this file is usually read as
-// making. What it shows is that a scheduler can be *written* in Deed. It cannot
-// be *shipped*, and a program that wants one has to copy this file and edit it.
+// making. What it shows is that a scheduler can be *written* in Deed. When this
+// file was written it could not be *shipped*, and a program that wanted one had
+// to copy this file and edit it.
 //
 // The wall is one line above: `Schedule.fork` takes a
 // `Fn() uses Schedule.fork, Schedule.yield, Log.note -> ()`, and that row names
 // `Log.note` because these particular tasks log. A library cannot know what its
 // tasks will perform, so the queue element type would have to be
-// `Fn() uses r -> ()` for a row variable `r` belonging to the effect. Effects do
-// not take row parameters: `effect Schedule<uses r>` does not parse, and
-// `DEED5008` separately confines a row variable to a function-typed parameter's
-// row and the declaration's own `uses`, which a handler's `state` is neither.
+// `Fn() uses r -> ()` for a row variable `r` belonging to the effect.
 //
-// So the queue's element type has to name a concrete row, the row has to name
-// every effect a task might perform, and both are things only the program
-// knows. That is why `std/task` does not exist next to `std/list`, and it is a
-// row-polymorphism gap rather than anything about concurrency.
+// That is what `effect Task<uses r>` is, and `std/task` is the scheduler
+// written that way. An effect declares row variables, they are in scope in its
+// operation signatures and in the state of any handler that implements it, and
+// each `Task.fork` fills the variable in from the value it was passed, so a
+// program that forks a task which logs is charged with logging.
+// `examples/tasks.deed` is this program written against the library.
+//
+// This file is kept as it was, because the difference between the two is the
+// whole of what a row variable on an effect buys, and it is easier to see side
+// by side than described. What is written below still works and still says
+// `Log.note` in a type that has nothing to do with logging.
 
 module examples/scheduler
 

examples/tasks.deed

@@ -0,0 +1,112 @@
+// Tasks, out of the library.
+//
+// The scheduler is `std/task`. Nothing in this file implements one: it forks
+// three tasks that log, runs them, and reads the log back. What is worth
+// noticing is that `std/task` says nothing about logging. `Task.fork` takes a
+// `Fn() uses r -> ()`, `r` is filled in from the value passed at each fork,
+// and that is why `main` below has to declare `Log.note` even though it never
+// calls it directly. The tasks perform it, `main` chose them, and the row
+// says so.
+//
+// `examples/scheduler.deed` is the same scheduler written out by hand, from
+// before an effect could take a row variable. Its queue names `Log.note` in
+// its own type, which is why it could not be a library and this can.
+
+module examples/tasks
+
+use std/task.{Task, RoundRobin, run, run_up_to}
+
+effect Log {
+    fn note(message: String) -> ()
+    fn messages() -> List<String>
+}
+
+handler Recorder implements Log {
+    state log: List<String>
+
+    fn note(message) -> () {
+        log = push(log, message)
+    }
+
+    fn messages() -> List<String> {
+        log
+    }
+}
+
+fn greet() -> ()
+  uses
+    Log.note,
+{
+    Log.note("hello")
+}
+
+fn count() -> ()
+  uses
+    Log.note,
+{
+    Log.note("one")
+    Log.note("two")
+}
+
+// A task that forks the rest of itself. This is how a task leaves room for
+// another one to run: there are no resumptions, so a task that wants to yield
+// splits, and the second half goes behind whatever else is waiting.
+fn later() -> ()
+  uses
+    Log.note,
+    Task.fork,
+{
+    Log.note("first half")
+    Task.fork(rest)
+}
+
+fn rest() -> ()
+  uses
+    Log.note,
+{
+    Log.note("second half")
+}
+
+// Everything the three tasks perform, and nothing about scheduling beyond
+// installing the handler.
+fn transcript() -> List<String>
+  uses
+    Log.note,
+    Log.messages,
+    Diverge,
+{
+    with RoundRobin { queue: [] } {
+        Task.fork(greet)
+        Task.fork(later)
+        Task.fork(count)
+        run()
+        Log.messages()
+    }
+}
+
+// The bounded runner, for when the number of tasks is the point.
+fn first_two() -> Int
+  uses
+    Log.note,
+{
+    with RoundRobin { queue: [] } {
+        Task.fork(greet)
+        Task.fork(count)
+        Task.fork(greet)
+        run_up_to(2)
+    }
+}
+
+test "tasks run in the order they were forked" {
+    let log = with Recorder { log: [] } {
+        transcript()
+    }
+    assert log == ["hello", "first half", "one", "two", "second half"]
+}
+
+test "a bounded run stops at the limit" {
+    let ran = with Recorder { log: [] } {
+        first_two()
+    }
+    assert ran == 2
+}

install/index.html

@@ -62,7 +62,7 @@ <h1>Install</h1>
         </p>
 
         <!--
-          Every `deed 0.2.3` below is the output of that binary on that
+          Every `deed 0.2.4` below is the output of that binary on that
           platform, printed by the release workflow, which refuses to publish
           when a binary disagrees with its tag. The program output further down
           was produced by running the released Windows build.
@@ -83,15 +83,15 @@ <h2>Take the file for your machine</h2>
           <tbody>
             <tr>
               <td>Linux, 64-bit Intel or AMD</td>
-              <td><code>deed-v0.2.3-x86_64-unknown-linux-gnu.tar.gz</code></td>
+              <td><code>deed-v0.2.4-x86_64-unknown-linux-gnu.tar.gz</code></td>
             </tr>
             <tr>
               <td>macOS, Apple silicon</td>
-              <td><code>deed-v0.2.3-aarch64-apple-darwin.tar.gz</code></td>
+              <td><code>deed-v0.2.4-aarch64-apple-darwin.tar.gz</code></td>
             </tr>
             <tr>
               <td>Windows, 64-bit</td>
-              <td><code>deed-v0.2.3-x86_64-pc-windows-msvc.zip</code></td>
+              <td><code>deed-v0.2.4-x86_64-pc-windows-msvc.zip</code></td>
             </tr>
           </tbody>
         </table>
@@ -110,23 +110,23 @@ <h2>Unpack it and ask it what it is</h2>
         </p>
 
         <h3>Linux</h3>
-        <pre class="code"><code>$ tar xzf deed-v0.2.3-x86_64-unknown-linux-gnu.tar.gz
-$ ./deed-v0.2.3-x86_64-unknown-linux-gnu/deed --version
-deed 0.2.3</code></pre>
+        <pre class="code"><code>$ tar xzf deed-v0.2.4-x86_64-unknown-linux-gnu.tar.gz
+$ ./deed-v0.2.4-x86_64-unknown-linux-gnu/deed --version
+deed 0.2.4</code></pre>
 
         <h3>macOS</h3>
-        <pre class="code"><code>$ tar xzf deed-v0.2.3-aarch64-apple-darwin.tar.gz
-$ xattr -d com.apple.quarantine deed-v0.2.3-aarch64-apple-darwin/deed
-$ ./deed-v0.2.3-aarch64-apple-darwin/deed --version
-deed 0.2.3</code></pre>
+        <pre class="code"><code>$ tar xzf deed-v0.2.4-aarch64-apple-darwin.tar.gz
+$ xattr -d com.apple.quarantine deed-v0.2.4-aarch64-apple-darwin/deed
+$ ./deed-v0.2.4-aarch64-apple-darwin/deed --version
+deed 0.2.4</code></pre>
         <p>
           The middle line is not optional and it is explained below.
         </p>
 
         <h3>Windows</h3>
-        <pre class="code"><code>&gt; Expand-Archive deed-v0.2.3-x86_64-pc-windows-msvc.zip .
-&gt; .\deed-v0.2.3-x86_64-pc-windows-msvc\deed.exe --version
-deed 0.2.3</code></pre>
+        <pre class="code"><code>&gt; Expand-Archive deed-v0.2.4-x86_64-pc-windows-msvc.zip .
+&gt; .\deed-v0.2.4-x86_64-pc-windows-msvc\deed.exe --version
+deed 0.2.4</code></pre>
 
         <h2>What your operating system will say about it</h2>
         <p>
@@ -162,7 +162,7 @@ <h2>Where to put it</h2>
           itself. To type <code>deed</code> instead of a path, move it onto
           yours:
         </p>
-        <pre class="code"><code>$ sudo mv deed-v0.2.3-x86_64-unknown-linux-gnu/deed /usr/local/bin/deed</code></pre>
+        <pre class="code"><code>$ sudo mv deed-v0.2.4-x86_64-unknown-linux-gnu/deed /usr/local/bin/deed</code></pre>
         <p>
           On Windows, put the folder on <code>Path</code> through Settings, or
           keep using the full path. Nothing on this page needs it on
@@ -218,7 +218,7 @@ <h2>When it does not work</h2>
             <code>./</code>, or move it as above.
           </dd>
 
-          <dt><code>--version</code> prints something other than 0.2.3</dt>
+          <dt><code>--version</code> prints something other than 0.2.4</dt>
           <dd>
             You are running a different <code>deed</code> than the one you
             unpacked. <code>which deed</code> says which.

one-clause/index.html

@@ -201,14 +201,14 @@ <h2 data-step="Now take the first one and add `Io.save` to it, and watch the com
         <nav class="next" aria-label="Open in the playground">
           <a
             class="card"
-            href="../play/#0.2.3/zTZFBi9wwDIXv_hXv1i5Mk3soC0t7mcsW2oUei-MoY4MjBUveNJT-9-JktuzRsvS9p6e-xzcmhOyrEhLDQ9ONvdVCSAqLhCnNMxXiQBjJNiKGbYIgyypMbNq5vnd9j5eYFHPlYEkYhfyk8JhTpg4vkd6R1e8K-u2D5R1b9IZkCJ5hUkMcGqwpt1Hd1Wi5YJZyIBPfOjyLxcQ3UFbq8EWWNWWaYIKfND6p0jLm_dIYDbXIVDN9UKRllWJQOh0GYfOJFcIEWan4ozwXWQ75KGrDfTdgIpqGJDhc3KtPRw8S60rBWlzekJMaRpqlEEplbkZbrHzLLWK1Ug_9DlfDRCFNpA22RbJIpW2hdV3zDvIh3k13b1qHxFrktY3hKl2zg7EaWKxhrtKpf6UjzlIZ1q7y_1jYkkWphkJqJZ1GnDsjwkSL9A34Szjvzs3cpAKpfjxuMeBrKhewX2jADyuJbw_49IjvpDXb57Nyuf88OqAqqQPwZvTi_rx_ntQT-OD-un8"
+            href="../play/#0.2.4/zTZFBi9wwDIXv_hXv1i5Mk3soC0t7mcsW2oUei-MoY4MjBUveNJT-9-JktuzRsvS9p6e-xzcmhOyrEhLDQ9ONvdVCSAqLhCnNMxXiQBjJNiKGbYIgyypMbNq5vnd9j5eYFHPlYEkYhfyk8JhTpg4vkd6R1e8K-u2D5R1b9IZkCJ5hUkMcGqwpt1Hd1Wi5YJZyIBPfOjyLxcQ3UFbq8EWWNWWaYIKfND6p0jLm_dIYDbXIVDN9UKRllWJQOh0GYfOJFcIEWan4ozwXWQ75KGrDfTdgIpqGJDhc3KtPRw8S60rBWlzekJMaRpqlEEplbkZbrHzLLWK1Ug_9DlfDRCFNpA22RbJIpW2hdV3zDvIh3k13b1qHxFrktY3hKl2zg7EaWKxhrtKpf6UjzlIZ1q7y_1jYkkWphkJqJZ1GnDsjwkSL9A34Szjvzs3cpAKpfjxuMeBrKhewX2jADyuJbw_49IjvpDXb57Nyuf88OqAqqQPwZvTi_rx_ntQT-OD-un8"
             >
             <strong>read_only.deed</strong>
             <span>The one a host without `Io.save` will run.</span>
           </a>
           <a
             class="card"
-            href="../play/#0.2.3/zhVFBjtswDLz7FXNrArj2PWgDLNpLTwXaBXpcKBIdC2uThkhvNijy90Jy7F20h-okaciZ4bBt8Z0JfnCzEiLDQeOZnc2JEBXWE0LsOkrEnnAiuxAx7CLwMk7CxKZN1bZV2-Kxj4puZm9RGIlcUDh0cSA4DrikaKSIhpPzz00RpldL7p289ZSZNg8HfJNG3Qs1-CLjFAcKMMEvOj2o0ngarnXxOEqYB_qgiOMkyaBUTGQulgu8sLnIWozLRMllVNElGUt_L2qH-xhAIAqHKCgz_PWVzdwLH0obrHeGKclLDKQQHq7ZdG6FEi0Z5q7VW84iUTdrwaJmqi1MnKiTREgzc-Rz2QefhxyOWprLVA0et5ERyA8uUYADExW360DwjlkMI5HVRXZDluUU51sG_0Z39-L4Ci-hmNKmqjblUdpM9FQ2W1Ud5xg8qe7y0vWArzHVYDfSAT8tRT7v8fGIH6TzYJ-Wn_qOHCsgR1IBWPOr10eOr65-l-fozPdrxSK0aOyxFORDKe0u_XWPz8ftXm-oPO-MXq2gG13WeE9XY6l5I_0_8Z38qcCryht8W6636lb9AQ"
+            href="../play/#0.2.4/zhVFBjtswDLz7FXNrArj2PWgDLNpLTwXaBXpcKBIdC2uThkhvNijy90Jy7F20h-okaciZ4bBt8Z0JfnCzEiLDQeOZnc2JEBXWE0LsOkrEnnAiuxAx7CLwMk7CxKZN1bZV2-Kxj4puZm9RGIlcUDh0cSA4DrikaKSIhpPzz00RpldL7p289ZSZNg8HfJNG3Qs1-CLjFAcKMMEvOj2o0ngarnXxOEqYB_qgiOMkyaBUTGQulgu8sLnIWozLRMllVNElGUt_L2qH-xhAIAqHKCgz_PWVzdwLH0obrHeGKclLDKQQHq7ZdG6FEi0Z5q7VW84iUTdrwaJmqi1MnKiTREgzc-Rz2QefhxyOWprLVA0et5ERyA8uUYADExW360DwjlkMI5HVRXZDluUU51sG_0Z39-L4Ci-hmNKmqjblUdpM9FQ2W1Ud5xg8qe7y0vWArzHVYDfSAT8tRT7v8fGIH6TzYJ-Wn_qOHCsgR1IBWPOr10eOr65-l-fozPdrxSK0aOyxFORDKe0u_XWPz8ftXm-oPO-MXq2gG13WeE9XY6l5I_0_8Z38qcCryht8W6636lb9AQ"
             >
             <strong>read_write.deed</strong>
             <span>The one it will not.</span>