From d5f6f7e326683818c518e908d580a24bbec64c06 Mon Sep 17 00:00:00 2001
From: Alfonso Sastre
Date: Fri, 25 Sep 2026 22:17:55 +0200
Subject: [PATCH] site: replace the zip demo with a REST API the agent builds
on lex-web
The typed-issue demo was a pure function and the run was hidden in a
log file, so it played in two seconds with nothing to look at. The new
one is a real run on a fresh clone with an empty store: a one-line
"check lex.toml" nudge, no package named. The agent found lex-web,
read it, built /health and /quote/:topic on its router, closed the
issue, and the recording ends with the server answering real curls.
Tool calls stream live instead of going to a log.
Also states the wrinkle it exposed: importing lex-web's router widens
the runtime effect grant well past the declared [net].
Co-Authored-By: Claude Sonnet 5
---
site/demo/issue.cast | 203 +++++++++++++++++++++++++++++++++++++++++--
site/index.html | 49 ++++++-----
2 files changed, 222 insertions(+), 30 deletions(-)
diff --git a/site/demo/issue.cast b/site/demo/issue.cast
index c75d527..247919b 100644
--- a/site/demo/issue.cast
+++ b/site/demo/issue.cast
@@ -1,9 +1,194 @@
-{"version": 2, "width": 80, "height": 24, "timestamp": 1790342232, "env": {"SHELL": "/bin/zsh", "TERM": null}, "idle_time_limit": 2.0}
-[0.015462, "o", "TERM environment variable not set.\r\n"]
-[0.015727, "o", "$ ISSUE_ID=$(lex issue create --title \"add zip\" --shape typed_delta \\\r\n --api \"zip:(xs :: List[A], ys :: List[B]) -> List[(A, B)]\" \\\r\n --example \"zip([1,2],[\\\"a\\\",\\\"b\\\"]) => [(1,\\\"a\\\"),(2,\\\"b\\\")]\")\r\n"]
-[0.023593, "o", "$ ./bin/lex-code \"--issue=$ISSUE_ID\" --ollama > /tmp/lex-code-issue-demo.log 2>&1\r\n"]
-[2061.950497, "o", "$ grep \"^[ISSUE_VERDICT]\" /tmp/lex-code-issue-demo.log\r\n"]
-[2061.965744, "o", "[ISSUE_VERDICT]\tverified\taea6613fc9e96953bb1c89fb3c45ac7200f62a379acdee2a47e29bab4c938ced\r\n"]
-[2062.4771, "o", "$ awk '/^fn zip/,/^}/' src/list_lex.lex # what actually got written\r\n"]
-[2062.4788280000002, "o", "fn zip[A, B](xs :: List[A], ys :: List[B]) -> List[(A, B)]\r\n examples {\r\n zip([1, 2], [\"a\", \"b\"]) => [(1, \"a\"), (2, \"b\")]\r\n }\r\n{\r\n let acc := list.fold(xs, ([], ys), fn (a :: (List[(A, B)], List[B]), x :: A) -> (List[(A, B)], List[B]) {\r\n match a {\r\n (out, rest) => match list.head(rest) {\r\n Some(y) => (list.cons((x, y), out), list.tail(rest)),\r\n"]
-[2062.478845, "o", " None => (out, rest),\r\n },\r\n }\r\n })\r\n match acc {\r\n (out, _) => list.reverse(out),\r\n }\r\n}\r\n"]
+{"version": 2, "width": 100, "height": 30, "timestamp": 1790366387, "env": {"SHELL": "/bin/zsh", "TERM": null}, "idle_time_limit": 2.0}
+[0.026125, "o", "\u001b[3J\u001b[H\u001b[2J"]
+[0.026344, "o", "\u001b[1;34m$ \u001b[0m"]
+[0.038581, "o", "ISSUE_"]
+[0.220303, "o", "ID=$(l"]
+[0.314557, "o", "ex iss"]
+[0.409768, "o", "ue cre"]
+[0.501628, "o", "ate --"]
+[0.591887, "o", "title "]
+[0.685371, "o", "\"add q"]
+[0.780362, "o", "uote a"]
+[0.874194, "o", "pi\" --"]
+[0.968372, "o", "shape "]
+[1.060697, "o", "typed_"]
+[1.155522, "o", "delta "]
+[1.249473, "o", "\\"]
+[1.252766, "o", "\r\n"]
+[1.272099, "o", " --"]
+[1.45833, "o", "body \""]
+[1.550959, "o", "REST A"]
+[1.641449, "o", "PI on "]
+[1.734781, "o", ":8931 "]
+[1.825212, "o", "— GE"]
+[1.917042, "o", "T /hea"]
+[2.007808, "o", "lth, G"]
+[2.10141, "o", "ET /qu"]
+[2.194529, "o", "ote/:t"]
+[2.28648, "o", "opic ("]
+[2.381457, "o", "JSON),"]
+[2.47391, "o", " else "]
+[2.661685, "o", "404."]
+[2.664387, "o", "\r\n"]
+[2.684939, "o", " "]
+[2.869487, "o", " "]
+[2.963265, "o", "Check "]
+[3.058312, "o", "lex.to"]
+[3.153341, "o", "ml for"]
+[3.245966, "o", " somet"]
+[3.340455, "o", "hing t"]
+[3.434334, "o", "hat al"]
+[3.525193, "o", "ready "]
+[3.616237, "o", "does r"]
+[3.70637, "o", "outing"]
+[3.799465, "o", " befor"]
+[3.890837, "o", "e hand"]
+[3.985775, "o", "-rolli"]
+[4.171565, "o", "ng it."]
+[4.26657, "o", "\" \\"]
+[4.267624, "o", "\r\n"]
+[4.281207, "o", " --"]
+[4.470339, "o", "api \"q"]
+[4.565381, "o", "uote_f"]
+[4.655855, "o", "or:(to"]
+[4.750695, "o", "pic ::"]
+[4.843148, "o", " Str) "]
+[4.938272, "o", "-> Str"]
+[5.028775, "o", "\" \\"]
+[5.029955, "o", "\r\n"]
+[5.046291, "o", " --"]
+[5.234813, "o", "api \"m"]
+[5.327305, "o", "ain:()"]
+[5.421481, "o", " -> [n"]
+[5.51664, "o", "et] Ni"]
+[5.611748, "o", "l\" \\"]
+[5.61432, "o", "\r\n"]
+[5.634313, "o", " --"]
+[5.822465, "o", "exampl"]
+[5.915684, "o", "e \"quo"]
+[6.007087, "o", "te_for"]
+[6.10071, "o", "(\\\"cou"]
+[6.195837, "o", "rage\\\""]
+[6.286422, "o", ") => \\"]
+[6.381516, "o", "\"Do on"]
+[6.476611, "o", "e thin"]
+[6.571658, "o", "g ever"]
+[6.662525, "o", "y day "]
+[6.753662, "o", "that s"]
+[6.846472, "o", "cares "]
+[6.941302, "o", "you.\\\""]
+[7.122417, "o", "\")"]
+[7.123818, "o", "\r\n"]
+[7.148877, "o", "\r\n"]
+[7.148959, "o", "\u001b[1;34m$ \u001b[0m"]
+[7.15794, "o", "lex-co"]
+[7.346622, "o", "de \"--"]
+[7.439066, "o", "issue="]
+[7.530615, "o", "$ISSUE"]
+[7.621425, "o", "_ID\" -"]
+[7.716517, "o", "-ollam"]
+[7.810069, "o", "a | gr"]
+[7.904085, "o", "ep -E "]
+[7.996481, "o", "\"^\\[to"]
+[8.087206, "o", "ol: |I"]
+[8.182252, "o", "SSUE_V"]
+[8.277457, "o", "ERDICT"]
+[8.370191, "o", "\""]
+[8.371316, "o", "\r\n"]
+[37.221287, "o", "[tool: issue_show]\r\n"]
+[37.548407, "o", "[tool: read]\r\n"]
+[37.922018, "o", "[tool: glob]\r\n"]
+[48.592724, "o", "[tool: grep]\r\n"]
+[48.959167, "o", "[tool: read]\r\n"]
+[81.881012, "o", "[tool: grep]\r\n"]
+[82.277277, "o", "[tool: lex_stdlib]\r\n"]
+[82.895755, "o", "[tool: glob]\r\n"]
+[87.01346, "o", "[tool: bash]\r\n"]
+[87.4263, "o", "[tool: lex_cli_help]\r\n"]
+[438.060202, "o", "[tool: bash]\r\n"]
+[476.650233, "o", "[tool: bash]\r\n"]
+[477.16504, "o", "[tool: lex_guide]\r\n"]
+[498.585221, "o", "[tool: lex_stdlib]\r\n"]
+[501.336417, "o", "[tool: bash]\r\n"]
+[787.84748, "o", "[tool: bash]\r\n"]
+[796.823437, "o", "[tool: bash]\r\n"]
+[816.308868, "o", "[tool: write]\r\n"]
+[827.747232, "o", "[tool: edit]\r\n"]
+[850.249565, "o", "[tool: edit]\r\n"]
+[868.044565, "o", "[tool: write]\r\n"]
+[893.397371, "o", "[tool: lex_run]\r\n"]
+[895.559692, "o", "[tool: issue_verify]\r\n"]
+[943.96841, "o", "[ISSUE_VERDICT]\tverified\t72fa4f17455dfb8d7624412a4449444cc85c747b09c2db423df32679e8f743ae\r\n"]
+[943.995021, "o", "\r\n"]
+[944.013733, "o", "\u001b[1;34m$ \u001b[0m"]
+[944.022891, "o", "grep -"]
+[944.212051, "o", "n 'imp"]
+[944.307079, "o", "ort\\|^"]
+[944.40208, "o", "fn ' s"]
+[944.495827, "o", "rc/quo"]
+[944.59085, "o", "te_api"]
+[944.685886, "o", ".lex"]
+[944.68657, "o", "\r\n"]
+[944.689857, "o", "14:import \"std.net\" as net\r\n16:import \"std.str\" as str\r\n18:import \"lex-web/src/router\" as router\r\n20:import \"lex-web/src/ctx\" as ctx\r\n22:import \"lex-web/src/response\" as resp\r\n26:fn quote_for(topic :: Str) -> Str\r\n"]
+[944.689869, "o", "48:fn handle_quote(c :: ctx.Ctx) -> resp.Response {\r\n57:fn build_router() -> router.Router {\r\n67:fn main() -> [net] Nil {\r\n"]
+[944.690061, "o", "\r\n"]
+[944.876647, "o", "\u001b[1;34m$ \u001b[0m"]
+[944.883834, "o", "lex ru"]
+[945.070347, "o", "n --al"]
+[945.165359, "o", "low-ef"]
+[945.260371, "o", "fects "]
+[945.354052, "o", "approv"]
+[945.448633, "o", "al,con"]
+[945.542768, "o", "curren"]
+[945.635042, "o", "t,cryp"]
+[945.725312, "o", "to,fs_"]
+[945.816489, "o", "read,f"]
+[945.909902, "o", "s_writ"]
+[946.003464, "o", "e,io,l"]
+[946.098566, "o", "lm,net"]
+[946.192669, "o", ",proc,"]
+[946.28763, "o", "random"]
+[946.476496, "o", ",sql,t"]
+[946.567765, "o", "ime sr"]
+[946.660557, "o", "c/quot"]
+[946.752023, "o", "e_api."]
+[946.844001, "o", "lex ma"]
+[946.934841, "o", "in &"]
+[946.937787, "o", "\r\n"]
+[949.952311, "o", "\u001b[1;34m$ \u001b[0m"]
+[949.963661, "o", "curl -"]
+[950.153902, "o", "s loca"]
+[950.245637, "o", "lhost:"]
+[950.340618, "o", "8931/h"]
+[950.43569, "o", "ealth"]
+[950.437779, "o", "\r\n"]
+[950.463486, "o", "{\"ok\":true}"]
+[950.463867, "o", "\r\n"]
+[950.463904, "o", "\u001b[1;34m$ \u001b[0m"]
+[950.470258, "o", "curl -"]
+[950.656505, "o", "s loca"]
+[950.748068, "o", "lhost:"]
+[950.841548, "o", "8931/q"]
+[950.936631, "o", "uote/c"]
+[951.031653, "o", "ourage"]
+[951.032897, "o", "\r\n"]
+[951.050176, "o", "{\"topic\":\"courage\",\"quote\":\"Do one thing every day that scares you.\"}"]
+[951.050294, "o", "\r\n\u001b[1;34m$ \u001b[0m"]
+[951.059177, "o", "curl -"]
+[951.244931, "o", "s loca"]
+[951.336761, "o", "lhost:"]
+[951.429608, "o", "8931/q"]
+[951.52437, "o", "uote/w"]
+[951.615155, "o", "isdom"]
+[951.617937, "o", "\r\n"]
+[951.640659, "o", "{\"topic\":\"wisdom\",\"quote\":\"Every day is a fresh page.\"}"]
+[951.641311, "o", "\r\n"]
+[951.641367, "o", "\u001b[1;34m$ \u001b[0m"]
+[951.65307, "o", "curl -"]
+[951.841581, "o", "s loca"]
+[951.934984, "o", "lhost:"]
+[952.028596, "o", "8931/n"]
+[952.123617, "o", "ope"]
+[952.124881, "o", "\r\n"]
+[952.139596, "o", "{\"error\":\"not found\"}"]
+[952.140112, "o", "\r\n"]
diff --git a/site/index.html b/site/index.html
index 0783602..8c82022 100644
--- a/site/index.html
+++ b/site/index.html
@@ -134,19 +134,19 @@ What's a typed issue?
Work as a declared, checkable contract instead of a paragraph of prose — an API shape and
the examples that prove it, the acceptance a run either closes against or doesn't. Real
output, the same issue used in "Try it" below:
- $ lex issue show aea6613fc9e96953bb1c89fb3c45ac7200f62a379acdee2a47e29bab4c938ced
+ $ lex issue show 72fa4f17455dfb8d7624412a4449444cc85c747b09c2db423df32679e8f743ae
{
"acceptance": {
"api": [
- { "kind": "added", "name": "zip",
- "signature": "(xs :: List[A], ys :: List[B]) -> List[(A, B)]" }
+ { "kind": "added", "name": "quote_for", "signature": "(topic :: Str) -> Str" },
+ { "kind": "added", "name": "main", "signature": "() -> [net] Nil" }
],
- "examples": [ "zip([1,2],[\"a\",\"b\"]) => [(1,\"a\"),(2,\"b\")]" ],
+ "examples": [ "quote_for(\"courage\") => \"Do one thing every day that scares you.\"" ],
"shape": "typed_delta"
},
- "created_at": 1790252464,
- "issue_id": "aea6613fc9e96953bb1c89fb3c45ac7200f62a379acdee2a47e29bab4c938ced",
- "title": "add zip"
+ "body": "Add a tiny REST API on port 8931: GET /health -> {\"ok\":true}, GET /quote/:topic -> a short quote for that topic as JSON, anything else -> 404. Check this project's own dependencies (lex.toml) for something that already does routing/responses before hand-rolling it.",
+ "issue_id": "72fa4f17455dfb8d7624412a4449444cc85c747b09c2db423df32679e8f743ae",
+ "title": "add quote api"
}
Issues live in Lex's own op-log VCS: every accepted change is a content-addressed,
hash-chained op, and lex issue verify checks the acceptance against HEAD, not a
@@ -174,23 +174,30 @@
Try it
what that looks like live. For a result you can act on
without reading the diff, hand it a typed issue instead — it closes by proof, not by a
transcript claiming success:
- ISSUE_ID=$(lex issue create --title "add zip" --shape typed_delta \
- --api 'zip:(xs :: List[A], ys :: List[B]) -> List[(A, B)]' \
- --example 'zip([1,2],["a","b"]) => [(1,"a"),(2,"b")]')
+ ISSUE_ID=$(lex issue create --title "add quote api" --shape typed_delta \
+ --body 'Add a tiny REST API on port 8931: GET /health, GET /quote/:topic (JSON),
+ else 404. Check lex.toml for something that already does routing
+ before hand-rolling it.' \
+ --api 'quote_for:(topic :: Str) -> Str' \
+ --api 'main:() -> [net] Nil' \
+ --example 'quote_for("courage") => "Do one thing every day that scares you."')
-lex-code "--issue=$ISSUE_ID" --ollama > /tmp/lex-code.log 2>&1
-grep '^\[ISSUE_VERDICT\]' /tmp/lex-code.log
-# [ISSUE_VERDICT] verified <issue_id>
-
-awk '/^fn zip/,/^}/' src/list_lex.lex # what actually got written
+lex-code "--issue=$ISSUE_ID" --ollama # streams what the agent does
+# [ISSUE_VERDICT] verified <issue_id>
- The typed-issue flow above, live and unedited — same issue,
- same run, ending in the same verified line, then the actual function it
- wrote, not just the verdict.
+ A real, unedited run on a fresh clone: about sixteen minutes of a
+ local model, played with idle gaps capped at two seconds. Then the code it wrote, the
+ server it started, and real curl answers.
-
Both commands above are copy-paste real — run verbatim against this repo
- before shipping this page, closing verified.
+
Nobody told it which package to use. The prompt says only "check
+ lex.toml before hand-rolling it". The agent read this project's
+ dependencies, found lex-web, read its
+ source, and built the routes on its router — /quote/:topic included — then
+ closed the issue against the declared signatures and example.
+
One honest wrinkle: the run command in the recording grants many effects. Importing
+ lex-web's router widens what the program needs at runtime well beyond its declared
+ [net], and we're narrowing that.
No key, no waitlist, no account: the install script above sets up the Lex toolchain
too if you don't already have it, then you're running a real session in under a
minute.
@@ -279,7 +286,7 @@
OpenCode Go plan
poster: 'npt:0:01'
});
AsciinemaPlayer.create('demo/issue.cast', document.getElementById('cast-issue'), {
- cols: 100, rows: 24, theme: 'monokai', fit: 'width', preload: true,
+ cols: 100, rows: 30, theme: 'monokai', fit: 'width', preload: true,
poster: 'npt:0:01'
});