From fbc1638363b69899e66007bedcad9cbe40137646 Mon Sep 17 00:00:00 2001 From: Claude Date: Wed, 16 Sep 2026 08:50:47 +0000 Subject: [PATCH 1/9] docs: how to expose a programmatic API from a plugin MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit A plugin can offer an application values of its own, and it always could: §11's exports are read back with `host.exports('/')`, a definition may publish as many keys as it likes, and the unqualified alias lets a library ship a one-line accessor that works whether the instance is tagged or not. That was written down for plugin-to-plugin use only, so the question arrived from sekreto as though the mechanism were missing. DOCS.md §2 now carries "Expose a programmatic API": the two calls, the several-exports shape, the alias rule, exports of a `loaded` instance, and when to export versus provide a capability. No library change. Writing it surfaced a corpus coverage gap, recorded as register row 6.7 rather than closed here. Every `export` entry reads the key `client`: the `probe` definition exports two keys but nothing reads the second, so a port whose `export` overwrote rather than keyed could stay green depending on write order. Closing it needs `probe` to export a second SCALAR key, which is a probe-catalog change and so a 23-port change set. No port is known to be wrong; same class as gaps 2 and 3. Co-Authored-By: Claude Opus 5 Claude-Session: https://claude.ai/code/session_01CVMgjjwQfTJ2rXz637Wpk8 --- DOCS.md | 53 ++++++++++++++++++++++++++++++++++++++++++++ doc/plan/progress.md | 1 + doc/plan/status.md | 21 ++++++++++++++++++ 3 files changed, 75 insertions(+) diff --git a/DOCS.md b/DOCS.md index ed20755..a1c8620 100644 --- a/DOCS.md +++ b/DOCS.md @@ -179,6 +179,59 @@ holders. It guards *ad-hoc* deactivation only: `close()` and an `apply` plan removing the holders too are coordinated teardowns and proceed, consumers first. +### Expose a programmatic API + +A plugin can offer the application more than the host's own vocabulary. +**Export it.** `inst.export(key, value)` during `define` publishes a +value; `host.exports('/')` reads it back. + +```ts +define: (inst) => { + const store = openstore(inst.options) + inst.export('provider', { read: store.read }) // what the host wires up + inst.export('admin', store) // what the application calls +} +``` +```ts +const admin = host.exports('store$main/admin') +admin.write('api.token', 'tok01') +``` + +**A definition may publish as many as it likes**, and the host treats +them identically. Two is the usual shape: one the host or its framework +consumes, one the application does. A definition that publishes only +what the framework wants leaves an application with no way to reach +anything else the plugin can do. + +**The unqualified alias is what makes this pleasant to call.** +`store/admin` resolves to the untagged instance if there is one; if not, +and exactly one tagged instance exports that key, it resolves to that +one; if two do, it is `plugin_export_ambiguous`, naming both. So a +library can offer `adminof(host)` and have it work whether the store was +configured as `store` or as `store$main` — and say so rather than pick +one when there are two of them. + +**Exports of a `loaded` instance are visible**, before activation and +after deactivation. They are declared in `define`, they are data, and +hiding them would make the loaded state useless for introspection. An +export whose value only means something while the instance is live is +the plugin's to signal, and the convention is a getter closing over +`inst.state`. + +Export for the **application**; provide a **capability** (above) for +another plugin. The difference is not enforced and is worth keeping +anyway: a capability is a dependency the host resolves, orders and can +restart a consumer over, while an export is a value someone asks for by +name. Reaching for an export to avoid declaring a dependency gets a +reference the lifecycle knows nothing about. + +The worked example is +[sekreto](https://github.com/voxgig/sekreto)'s mini vault, where each +provider kind is a definition and the vault is the one that is written +to as well as read: it exports `provider` for the chain and `vault` for +the application, and ships a one-line `vaultof(secrets)` over the +alias rule above. + ### Hold a resource Acquire in `activate` and forget about it: diff --git a/doc/plan/progress.md b/doc/plan/progress.md index 4845e5e..86cac55 100644 --- a/doc/plan/progress.md +++ b/doc/plan/progress.md @@ -94,4 +94,5 @@ It did: see 4.1's note and [`handover.md`](handover.md) §13. | 6.6 The ref rule, everywhere the graph is examined | **DONE** | Codex's review of the gap-2 PR said the close was premature, and it was right — for a reason larger than the finding. §11.1 says a ref satisfies a requirement, and THREE places read a requirement name: runtime `providersof`, load-time `dependencycycle`, and whole-graph `resolve`. Only the first implemented the rule. **Four canonical defects, all now fixed and pinned.** (a) `providersof` canonicalized EVERY requirement name, so a capability called `2fa` or `my cap` — both legal, since §4's grammar is on plugin names and the design puts none on capability names — raised `plugin_bad_name` and killed a legal document; every capability name in the corpus happened to be a well-formed ref, and nine ports had independently worked around it with a try/except or a tolerant `canon`, so the canonical was the outlier and nothing caught it. (b) `dependencycycle` indexed providers by canonical ref and looked them up with the raw name, so the same cycle spelled `dep$`/`other$` produced no edges and EVADED the load-time check entirely. (c) `graph.candidates` never considered node refs at all, so `resolve()` answered `absent` about a provider the runtime binds — even in the canonical spelling. (d) The design text asserted ref loss always sends a consumer to `pending`; it follows the ordinary cardinality/policy rules, so mandatory-`dynamic` stays live and optional never gated. Canonical gains a tolerant `tryref`; every port uses its own existing tolerant spelling. Eleven new entries across `depend/byref`, `depend/cycle` and `graph/resolve`+`blocked`; each targeted mutant fails its group and no other. Corpus 561 -> 572. | | 6.1 Six tier-4 ports | **DONE (6/6)** | `c`, `cpp`, `ocaml`, `haskell`, `zig`, `lean` — all six pass all 572 entries, and **twenty-three implementations now do**. Toolchains all reachable: gcc/g++ 13.3.0 present, ghc 9.4.7 and ocaml 4.14.1 from apt, zig 0.13.0 from a ziglang.org tarball, lean 4.15.0 from a pinned GitHub release asset. **The six are deliberately not one port six times**, and §10.3's "tier-4" turned out to describe the LOADER, not the language: it says nothing about closures, exceptions or a garbage collector, and those three are what a port actually costs. `c` builds all three by hand (arena, setjmp/longjmp — safe *because* of the arena — and `volatile` on every local straddling a try, seven of which `-Wclobbered` found); `cpp`, `ocaml` and `haskell` use what their languages have and need none of it; `zig` has none of them and needed a fourth answer. **What each one found is in handover.md §19.** Four defects the corpus caught between them: `point/bail#null-declines` wants PRESENCE not non-null; `resource/scope#difference` wants an early-release handle; `cpp` inherited `c`'s POSIX-ERE regex dialect for the corpus `match` patterns, which are JavaScript literals; and `ocaml` found that a bad number must be a reported error, not a crash, or §9.5's parse-or-string fallback cannot catch it. **Two the corpus could NOT catch**: `check_probes.py` had no `c` row, so it reported `c` green without opening a file; and the `provider` probe carried a dead capability record in `c`, `cpp` and `ocaml` that haskell nearly turned into a real divergence — the lesson being *check the canonical, not the nearest port*. **Two languages refused the shape outright**, which is the durable finding: zig's errors carry no payload, so the diagnostic travels beside the error and every handler takes it first; and **Lean's kernel rejects the definition↔instance cycle every other port takes for granted** (`non positive occurrence of the datatypes being declared`), so the instance api became an explicit record of closures — which is what §6 says a plugin may touch anyway. | | 6.3 Corpus gap 1: shape validation at REGISTRATION | **DONE** | `declare/shape` (7 entries) pins §10.1's TIMING, which `config/optmergebad` says in its own comment it cannot: every entry stops at `define`, so a port deferring the check to resolution raises nothing and fails. Two entries also pin that a valid shape is KEPT rather than validated and dropped, one that a rejected registration leaves nothing behind. **The gap was not cheap and §18's "cheap" was wrong about it**: nothing carried a `shape` because the driver's `define` was a NO-OP in all seventeen ports — a documented three-key verb (DOCS.md §4.2) that registered nothing — so `catalog.add`'s check was unreachable by construction and the `probe` key was ignored by the ten entries passing it. `define` is now implemented everywhere, all three keys live, and `declare/register` (3 entries) pins `probe` distinct from `name`. DOCS.md's "default is `probe`" was wrong and is corrected to `name`; the literal default would have re-backed every `dep`, `noisy` and `greedy` definition with the wrong probe. **Implementing it found a canonical bug**: `apply` handed its resolved options map to `declare`, which ADOPTS it, then refilled that map from itself — so a first-time `apply` left the instance with **no options at all**, and only a second identical apply filled them in. Every `apply` entry asserted status, log or open and none a value the options decide. Fixed in canonical, go, javascript, python, ruby, perl, lua, dart; php, java, csharp, kotlin, rust, swift, scala, elixir, clojure never had it. Three new `apply/idempotent` entries pin it. Corpus 539 -> 552; `make check` green in all seventeen. | +| 6.7 Corpus gap 4: a second export key off ONE instance | OPEN | Found while writing DOCS.md §2's *Expose a programmatic API*, for sekreto's mini vault, which publishes `provider` and `vault` from one `define`. §11 says an instance publishes valueS and the `probe` definition exports two (`client` and its own `inst`), but **every `export` entry in the corpus reads the key `client`** — seven reads of one key, plus one absent key. So nothing distinguishes a correct keyed map from a port whose `export` overwrote, or whose `exports` collapsed to one value per instance; whether such a port stays green depends on which key `probe` writes last, which nothing specifies. Closing it needs a probe that exports a second SCALAR key: `probe`'s `inst` is an instance api, shaped differently in every port, so no entry can assert on it. That is a probe-catalog change, so it is a 23-port change set (DOCS.md §4.3) and is recorded here rather than taken on the side of a documentation change. No port is known to be wrong; this is a coverage gap of the same class as 6.4 and 6.5. | | 6.2 Does sdkgen adopt plugin? (§17.2) | DECISION NEEDED | Open, uncommitted, and carries a propagation cost across 23 template trees. Gates nested hosts *natively*, deletion of `transport`, and the seventeen-model change. | diff --git a/doc/plan/status.md b/doc/plan/status.md index 53bc4ce..4f769c1 100644 --- a/doc/plan/status.md +++ b/doc/plan/status.md @@ -206,6 +206,27 @@ table is the summary, that file is the authority. Neither blocks P1. ## Recently settled +- **"Can a plugin expose a programmatic API?" is answered, and the + answer needed no code.** It is §11's exports: `inst.export(key, value)` + in `define`, `host.exports('/')` to read it back, and the + unqualified alias so a library can offer a one-line accessor that works + whether the instance is tagged or not. The mechanism was documented for + plugin-to-plugin use and the application-facing half was not written + down, so DOCS.md §2 now carries **Expose a programmatic API**, including + when to export and when to provide a capability instead. The asker was + sekreto, whose mini vault publishes `provider` for the chain and `vault` + for the application from one `define`. + +- **A fourth corpus gap, found while writing that** and recorded as + register row 6.7 rather than closed: **every `export` entry reads the + key `client`**. The `probe` definition exports two keys, but nothing + reads the second, so a port whose `export` overwrote rather than keyed + could stay green depending on write order. Closing it needs `probe` to + export a second SCALAR key — its `inst` export is an instance api and no + entry can assert on it — and a probe-catalog change is a 23-port change + set. No port is known to be wrong; this is the same class as gaps 2 and + 3, which also needed no port change. + - **The scala and kotlin ports are built under both their compilers** — #29 and #30 made the ports accept two major versions each, and #31 delivered the CI job that builds the newer one, applied as `7c7e437` From b1111067607fd7e1919471e7aa9dfde6b1efd1e3 Mon Sep 17 00:00:00 2001 From: Claude Date: Wed, 16 Sep 2026 08:55:18 +0000 Subject: [PATCH 2/9] prose: the Vale half of the gate, which ran only in CI Three errors, all in the new how-to: a missing Oxford comma, and two `above`s where the house rule wants `preceding`. The second one also read better as a named section than as a direction. `make scan-prose` says out loud that it is skipping the Vale half when vale is not installed. Running `tools/check_prose.py` directly, as this branch did, does not -- it is only ever the second half of the gate. Co-Authored-By: Claude Opus 5 Claude-Session: https://claude.ai/code/session_01CVMgjjwQfTJ2rXz637Wpk8 --- DOCS.md | 15 ++++++++------- 1 file changed, 8 insertions(+), 7 deletions(-) diff --git a/DOCS.md b/DOCS.md index a1c8620..eeb7444 100644 --- a/DOCS.md +++ b/DOCS.md @@ -218,19 +218,20 @@ export whose value only means something while the instance is live is the plugin's to signal, and the convention is a getter closing over `inst.state`. -Export for the **application**; provide a **capability** (above) for -another plugin. The difference is not enforced and is worth keeping -anyway: a capability is a dependency the host resolves, orders and can -restart a consumer over, while an export is a value someone asks for by -name. Reaching for an export to avoid declaring a dependency gets a -reference the lifecycle knows nothing about. +Export for the **application**; provide a **capability** (*Depend on +something*, preceding) for another plugin. The difference is not +enforced and is worth keeping anyway: a capability is a dependency the +host resolves, orders, and can restart a consumer over, while an export +is a value someone asks for by name. Reaching for an export to avoid +declaring a dependency gets a reference the lifecycle knows nothing +about. The worked example is [sekreto](https://github.com/voxgig/sekreto)'s mini vault, where each provider kind is a definition and the vault is the one that is written to as well as read: it exports `provider` for the chain and `vault` for the application, and ships a one-line `vaultof(secrets)` over the -alias rule above. +preceding alias rule. ### Hold a resource From 5c1df3473b84849a24f7da84caba745fa42526b7 Mon Sep 17 00:00:00 2001 From: Claude Date: Wed, 16 Sep 2026 09:00:46 +0000 Subject: [PATCH 3/9] docs: five corrections to the export how-to, and two more gaps recorded MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit Codex's review, verified against the canonical. Five of its six findings were real; each is fixed here, and the two that turned out to be library-sized are register rows rather than edits. Corrected in DOCS.md: - A CAPABILITY IS NOT AN ALTERNATIVE TO AN EXPORT, and the text said it was. `inst.provides` records selection metadata and `host.capability(name)` answers with provider refs, so neither carries a callable value: the capability is the edge the host resolves and orders, and the API still travels as an export or a binding. A provider following the old sentence would have left its consumer with a name and nothing to call. - The unqualified alias filters by KEY before tag. `resolveexport` builds its candidate list from entries matching the key, so an untagged instance that exports something else does not shadow the tagged one that exports this. Reproduced both ways. - `{ read: store.read }` loses its receiver. A method reading `this` breaks the moment it is lifted off the object and the host calls it; the example is a closure now, and says why. - The spec splits at the FIRST `/`, so the `/` form addresses only a name without one. Stated, with the register row. - `export/key#loaded-visible` named as what pins loaded-export visibility. And `doc/plan/`: - 6.8: a scoped definition (`@acme/store`, legal under §4 and handled by `resolvecandidates`) has no export spelling. `@acme/store/admin` reads as ref `@acme`, key `store/admin`, and answers undefined. No `export` entry covers it — all of them use `probe`, which has no slash. - 6.9: §11.1 says `inst.capability(name)` returns the bound provider. The canonical instance api has no such method. A design statement no corpus entry can distinguish, which is handover.md §13's first kind. - The snapshot date, which said 2026-09-04 while this change added to it. The sixth finding cited a rule that does not exist: AGENTS.md §5c is the prose gate and says nothing about behaviour statements naming their corpus entry. The citation is added anyway, on its merits. Co-Authored-By: Claude Opus 5 Claude-Session: https://claude.ai/code/session_01CVMgjjwQfTJ2rXz637Wpk8 --- DOCS.md | 50 ++++++++++++++++++++++++++++++-------------- doc/plan/progress.md | 2 ++ doc/plan/status.md | 12 ++++++++--- 3 files changed, 45 insertions(+), 19 deletions(-) diff --git a/DOCS.md b/DOCS.md index eeb7444..9d9eb98 100644 --- a/DOCS.md +++ b/DOCS.md @@ -188,8 +188,11 @@ value; `host.exports('/')` reads it back. ```ts define: (inst) => { const store = openstore(inst.options) - inst.export('provider', { read: store.read }) // what the host wires up - inst.export('admin', store) // what the application calls + // A CLOSURE, not `store.read` lifted off the object: a method that + // reads `this` loses its receiver the moment it is copied, and the + // host calls what it is handed. + inst.export('provider', { read: (name) => store.read(name) }) + inst.export('admin', store) } ``` ```ts @@ -197,6 +200,14 @@ const admin = host.exports('store$main/admin') admin.write('api.token', 'tok01') ``` +**The spec splits at the FIRST `/`**, so this addresses a definition +whose name has no slash in it. §4's grammar permits one — `@acme/store` +is a legal name, and `resolvecandidates` resolves a scoped name +verbatim — and `@acme/store/admin` therefore reads as the ref `@acme` +with the key `store/admin`, which matches nothing. A scoped definition +has no spelling for its exports today; nothing in the corpus covers it, +and register row 6.8 carries it. + **A definition may publish as many as it likes**, and the host treats them identically. Two is the usual shape: one the host or its framework consumes, one the application does. A definition that publishes only @@ -204,27 +215,34 @@ what the framework wants leaves an application with no way to reach anything else the plugin can do. **The unqualified alias is what makes this pleasant to call.** -`store/admin` resolves to the untagged instance if there is one; if not, -and exactly one tagged instance exports that key, it resolves to that -one; if two do, it is `plugin_export_ambiguous`, naming both. So a -library can offer `adminof(host)` and have it work whether the store was -configured as `store` or as `store$main` — and say so rather than pick -one when there are two of them. +`store/admin` resolves to the untagged instance **if that one exports +the key**; if not, and exactly one tagged instance does, it resolves to +that one; if two do, it is `plugin_export_ambiguous`, naming both. The +key filters the candidates before the tag does, so an untagged instance +that publishes something else entirely does not shadow the tagged one +that publishes this. A library can therefore offer `adminof(host)` and +have it work whether the store was configured as `store` or as +`store$main` — and say so rather than pick one when there are two. **Exports of a `loaded` instance are visible**, before activation and -after deactivation. They are declared in `define`, they are data, and +after deactivation — `export/key#loaded-visible` pins it. They are +declared in `define`, they are data, and hiding them would make the loaded state useless for introspection. An export whose value only means something while the instance is live is the plugin's to signal, and the convention is a getter closing over `inst.state`. -Export for the **application**; provide a **capability** (*Depend on -something*, preceding) for another plugin. The difference is not -enforced and is worth keeping anyway: a capability is a dependency the -host resolves, orders, and can restart a consumer over, while an export -is a value someone asks for by name. Reaching for an export to avoid -declaring a dependency gets a reference the lifecycle knows nothing -about. +Export for the **application**. For another plugin, declare a +**capability** (*Depend on something*, preceding) as well — **not +instead**. The two do different jobs and a provider needs both: +`inst.provides` records what this instance is and what rank it has, and +`host.capability(name)` answers with provider REFS, so neither carries a +callable value. The capability is the edge the host resolves, orders, +and can restart a consumer over; the API itself still travels as an +export, or as a binding on an extension point. A provider that declares +a capability and exports nothing leaves its consumer with a name and +nothing to call. Going the other way — an export with no capability +declared — gets a reference the lifecycle knows nothing about. The worked example is [sekreto](https://github.com/voxgig/sekreto)'s mini vault, where each diff --git a/doc/plan/progress.md b/doc/plan/progress.md index 86cac55..4da6693 100644 --- a/doc/plan/progress.md +++ b/doc/plan/progress.md @@ -95,4 +95,6 @@ It did: see 4.1's note and [`handover.md`](handover.md) §13. | 6.1 Six tier-4 ports | **DONE (6/6)** | `c`, `cpp`, `ocaml`, `haskell`, `zig`, `lean` — all six pass all 572 entries, and **twenty-three implementations now do**. Toolchains all reachable: gcc/g++ 13.3.0 present, ghc 9.4.7 and ocaml 4.14.1 from apt, zig 0.13.0 from a ziglang.org tarball, lean 4.15.0 from a pinned GitHub release asset. **The six are deliberately not one port six times**, and §10.3's "tier-4" turned out to describe the LOADER, not the language: it says nothing about closures, exceptions or a garbage collector, and those three are what a port actually costs. `c` builds all three by hand (arena, setjmp/longjmp — safe *because* of the arena — and `volatile` on every local straddling a try, seven of which `-Wclobbered` found); `cpp`, `ocaml` and `haskell` use what their languages have and need none of it; `zig` has none of them and needed a fourth answer. **What each one found is in handover.md §19.** Four defects the corpus caught between them: `point/bail#null-declines` wants PRESENCE not non-null; `resource/scope#difference` wants an early-release handle; `cpp` inherited `c`'s POSIX-ERE regex dialect for the corpus `match` patterns, which are JavaScript literals; and `ocaml` found that a bad number must be a reported error, not a crash, or §9.5's parse-or-string fallback cannot catch it. **Two the corpus could NOT catch**: `check_probes.py` had no `c` row, so it reported `c` green without opening a file; and the `provider` probe carried a dead capability record in `c`, `cpp` and `ocaml` that haskell nearly turned into a real divergence — the lesson being *check the canonical, not the nearest port*. **Two languages refused the shape outright**, which is the durable finding: zig's errors carry no payload, so the diagnostic travels beside the error and every handler takes it first; and **Lean's kernel rejects the definition↔instance cycle every other port takes for granted** (`non positive occurrence of the datatypes being declared`), so the instance api became an explicit record of closures — which is what §6 says a plugin may touch anyway. | | 6.3 Corpus gap 1: shape validation at REGISTRATION | **DONE** | `declare/shape` (7 entries) pins §10.1's TIMING, which `config/optmergebad` says in its own comment it cannot: every entry stops at `define`, so a port deferring the check to resolution raises nothing and fails. Two entries also pin that a valid shape is KEPT rather than validated and dropped, one that a rejected registration leaves nothing behind. **The gap was not cheap and §18's "cheap" was wrong about it**: nothing carried a `shape` because the driver's `define` was a NO-OP in all seventeen ports — a documented three-key verb (DOCS.md §4.2) that registered nothing — so `catalog.add`'s check was unreachable by construction and the `probe` key was ignored by the ten entries passing it. `define` is now implemented everywhere, all three keys live, and `declare/register` (3 entries) pins `probe` distinct from `name`. DOCS.md's "default is `probe`" was wrong and is corrected to `name`; the literal default would have re-backed every `dep`, `noisy` and `greedy` definition with the wrong probe. **Implementing it found a canonical bug**: `apply` handed its resolved options map to `declare`, which ADOPTS it, then refilled that map from itself — so a first-time `apply` left the instance with **no options at all**, and only a second identical apply filled them in. Every `apply` entry asserted status, log or open and none a value the options decide. Fixed in canonical, go, javascript, python, ruby, perl, lua, dart; php, java, csharp, kotlin, rust, swift, scala, elixir, clojure never had it. Three new `apply/idempotent` entries pin it. Corpus 539 -> 552; `make check` green in all seventeen. | | 6.7 Corpus gap 4: a second export key off ONE instance | OPEN | Found while writing DOCS.md §2's *Expose a programmatic API*, for sekreto's mini vault, which publishes `provider` and `vault` from one `define`. §11 says an instance publishes valueS and the `probe` definition exports two (`client` and its own `inst`), but **every `export` entry in the corpus reads the key `client`** — seven reads of one key, plus one absent key. So nothing distinguishes a correct keyed map from a port whose `export` overwrote, or whose `exports` collapsed to one value per instance; whether such a port stays green depends on which key `probe` writes last, which nothing specifies. Closing it needs a probe that exports a second SCALAR key: `probe`'s `inst` is an instance api, shaped differently in every port, so no entry can assert on it. That is a probe-catalog change, so it is a 23-port change set (DOCS.md §4.3) and is recorded here rather than taken on the side of a documentation change. No port is known to be wrong; this is a coverage gap of the same class as 6.4 and 6.5. | +| 6.8 A scoped definition has no export spelling | OPEN | Found by Codex's review of the DOCS.md how-to, and reproduced against the canonical. `resolveexport` splits an export spec at the FIRST `/`, so `@acme/store/admin` reads as the ref `@acme` with the key `store/admin` and answers `undefined`. §4's `checkname` permits `/` in a NAME, and `resolvecandidates` has a branch for scoped names resolving verbatim, so scoped definitions are a supported case with no way to read their exports. Nothing in `export` covers it: every entry there uses `probe`, which has no slash. Closing it is a canonical decision first (an escape, a last-`/` split, or a narrower documented domain for an export spec), then the corpus, then 23 ports — so it is recorded rather than taken on the side of a documentation change. The how-to states the limit meanwhile. | +| 6.9 §11.1's `inst.capability(name)` does not exist | OPEN | Also from that review. The design says "the first is bound, and `inst.capability(name)` returns it", and the canonical instance api has no such method — `bind`, `export`, `provides`, `acquire`, `release`, `position`, `nest`, and no `capability`. What exists is `host.capability(name)`, which returns provider REFS. So a capability carries selection metadata and a lifecycle edge, and no callable value: a consumer reaches the provider's API through an export or an extension point. That is a design statement no corpus entry can distinguish, which is handover.md §13's first kind exactly. Either implement `inst.capability` or correct §11.1; the how-to documents the behaviour as it is meanwhile. | | 6.2 Does sdkgen adopt plugin? (§17.2) | DECISION NEEDED | Open, uncommitted, and carries a propagation cost across 23 template trees. Gates nested hosts *natively*, deletion of `transport`, and the seventeen-model change. | diff --git a/doc/plan/status.md b/doc/plan/status.md index 4f769c1..fb4bc3f 100644 --- a/doc/plan/status.md +++ b/doc/plan/status.md @@ -1,6 +1,6 @@ # Status — where the next session starts -Live snapshot, **2026-09-04**. The register in +Live snapshot, **2026-09-16**. The register in [`progress.md`](progress.md) is the per-item authority, [`contracts.md`](contracts.md) tracks what is owed across repos, and [`handover.md`](handover.md) is the durable record. This file says what @@ -217,8 +217,14 @@ table is the summary, that file is the authority. Neither blocks P1. sekreto, whose mini vault publishes `provider` for the chain and `vault` for the application from one `define`. -- **A fourth corpus gap, found while writing that** and recorded as - register row 6.7 rather than closed: **every `export` entry reads the +- **Three gaps found while writing that**, all recorded rather than + closed, because each is a 23-port change set and this was a + documentation change. Row **6.8**: `resolveexport` splits at the first + `/`, so a scoped definition name (`@acme/store`, which §4 permits and + `resolvecandidates` handles) has no spelling for its exports. Row + **6.9**: §11.1 says `inst.capability(name)` returns the bound provider + and the canonical instance api has no such method, so a capability + carries no callable value. And row **6.7**: **every `export` entry reads the key `client`**. The `probe` definition exports two keys, but nothing reads the second, so a port whose `export` overwrote rather than keyed could stay green depending on write order. Closing it needs `probe` to From 022464c0776b7b416bc064d536706dd5e4b24fe6 Mon Sep 17 00:00:00 2001 From: Claude Date: Wed, 16 Sep 2026 10:40:11 +0000 Subject: [PATCH 4/9] patch: build the lean port with the compiler it pins `lean` has failed on every CI run since 48392f5, including every run on `main`. That commit moved the port to Lean v4.32.1; `.github/workflows/ ci.yml` still fetches v4.15.0, so CI compiles 4.32.1 sources with a compiler predating the `String.Slice` changes the port was rewritten for. It fails at `make build-lean`, which reads as a port failure and is not one. REPRODUCED BOTH WAYS rather than inferred. Both compilers were fetched and the port built under each: v4.15.0 Some required builds logged failures: - Corpus - Plugin.Env - Plugin.Version v4.32.1 clean; 576 corpus entries across 19 sections, all pass The port's bump landed without the workflow because an agent session cannot write `.github/workflows/` -- the boundary AGENTS.md section 5b names, and the reason this folder exists. The patch adds a comment above the step saying the two versions move together, so the next bump has one place to look. `patch/` means work applied by nobody yet: apply it and delete the folder. Two things it needed beside itself. `tools/check_prose.py` called `patch/` a twenty-fourth port, because any top-level directory with a README.md is one and `patch/` predates the gate -- its README is a working document addressed to whoever applies it, so `NOT_PORTS` now carries it. And `doc/plan/status.md` still advised lean 4.15.0 as the pinned asset, under a heading about adding a new port. Co-Authored-By: Claude Opus 5 Claude-Session: https://claude.ai/code/session_01CVMgjjwQfTJ2rXz637Wpk8 --- doc/plan/status.md | 2 +- ...-lean-port-with-the-compiler-it-pins.patch | 51 +++++++++++ patch/README.md | 86 +++++++++++++++++++ tools/check_prose.py | 9 +- 4 files changed, 146 insertions(+), 2 deletions(-) create mode 100644 patch/0001-ci-build-the-lean-port-with-the-compiler-it-pins.patch create mode 100644 patch/README.md diff --git a/doc/plan/status.md b/doc/plan/status.md index fb4bc3f..4882641 100644 --- a/doc/plan/status.md +++ b/doc/plan/status.md @@ -160,7 +160,7 @@ exists and passes; see above. **If a new port is ever added**, the toolchain notes are worth keeping: gcc/g++ 13.3.0 ship in the image; **ghc 9.4.7 and ocaml 4.14.1 come -from apt**; **zig 0.13.0 from a ziglang.org tarball**; **lean 4.15.0 +from apt**; **zig 0.13.0 from a ziglang.org tarball**; **lean 4.32.1 from a pinned GitHub *release asset*** — release assets download fine through the proxy, while `api.github.com` answers 403, so a version-discovery call fails where the asset URL does not. Read the six diff --git a/patch/0001-ci-build-the-lean-port-with-the-compiler-it-pins.patch b/patch/0001-ci-build-the-lean-port-with-the-compiler-it-pins.patch new file mode 100644 index 0000000..960410d --- /dev/null +++ b/patch/0001-ci-build-the-lean-port-with-the-compiler-it-pins.patch @@ -0,0 +1,51 @@ +From 2933087df413a3dfa21b13f2dda6aee8bb29b0c1 Mon Sep 17 00:00:00 2001 +From: Claude +Date: Wed, 16 Sep 2026 10:26:45 +0000 +Subject: [PATCH] ci: build the lean port with the compiler it pins + +`lean/lean-toolchain` moved to v4.32.1 in 48392f5, for the reason that +commit gives: voxgig/struct's lean port and the sdkgen scaffold both pin +it, and four repositories vendored together as one checkpoint cannot be +compiled side by side on three different pins. + +This file still fetched v4.15.0, so CI compiled 4.32.1 sources with a +compiler that predates the `String.Slice` changes 48392f5 was written +for. `make build-lean` has failed on every run since, on `main` as well +as on every branch, and it reads as a port failure rather than a +toolchain mismatch. + +An agent session cannot write `.github/workflows/`, which is why the +port's bump landed without this. The comment now says the two must move +together, so the next bump has one place to look. + +Verified: the v4.32.1 linux asset resolves at the URL this builds. +--- + .github/workflows/ci.yml | 9 ++++++++- + 1 file changed, 8 insertions(+), 1 deletion(-) + +diff --git a/.github/workflows/ci.yml b/.github/workflows/ci.yml +index 9994820..36ec2c2 100644 +--- a/.github/workflows/ci.yml ++++ b/.github/workflows/ci.yml +@@ -232,10 +232,17 @@ jobs: + # The asset is `.tar.zst`; ubuntu-latest ships zstd, and the + # explicit `--use-compress-program` says so rather than relying on + # tar's suffix detection. ++ # ++ # THE VERSION HERE MUST MATCH `lean/lean-toolchain`, and an agent ++ # session cannot edit this file, so the two move in separate ++ # changes and the port's own bump lands first. When they drifted ++ # the job failed on `make build-lean` with the port's sources and ++ # the workflow's older compiler, which reads as a port failure and ++ # is not one. + - if: matrix.port == 'lean' + run: | + curl -fsSL -o /tmp/lean.tar.zst \ +- https://github.com/leanprover/lean4/releases/download/v4.15.0/lean-4.15.0-linux.tar.zst ++ https://github.com/leanprover/lean4/releases/download/v4.32.1/lean-4.32.1-linux.tar.zst + sudo mkdir -p /opt/lean + sudo tar --use-compress-program=unzstd -xf /tmp/lean.tar.zst \ + -C /opt/lean --strip-components=1 +-- +2.43.0 + diff --git a/patch/README.md b/patch/README.md new file mode 100644 index 0000000..419fc18 --- /dev/null +++ b/patch/README.md @@ -0,0 +1,86 @@ +# `patch/` — a change this session could not push + +`.github/workflows/` is refused to the session that wrote this change, on +both write paths: + +- **git push** — `refusing to allow an OAuth App to create or update workflow + .github/workflows/ci.yml without workflow scope` +- **the GitHub App's file API** — fails on that path while writing any other + file in the same breath + +The change is a workflow change, so it cannot travel as a branch. It travels +as a patch instead, and this folder is transient: delete it once the patch is +applied. + +## Apply it + +From any checkout that carries this folder — this branch, or `main` once the +delivery commit is merged: + +```sh +git am patch/0001-ci-build-the-lean-port-with-the-compiler-it-pins.patch +``` + +Read it from the worktree rather than from a branch ref: the source branch is +usually deleted after merging and a fresh clone never had it, so a command +naming that branch would fail exactly when it is most likely to be run. If you +would rather not check the branch out, name a ref that outlives it: + +```sh +git show origin/main:patch/0001-ci-build-the-lean-port-with-the-compiler-it-pins.patch | git am +``` + +## What it does + +One line, plus the comment that explains it. + +| | version | +|---|---| +| `lean/lean-toolchain` | `leanprover/lean4:v4.32.1` | +| `.github/workflows/ci.yml`, before | `v4.15.0` | +| `.github/workflows/ci.yml`, after | `v4.32.1` | + +## Why it is worth doing + +**The `lean` job has failed on every run since `48392f5`**, including every +run on `main`. That commit moved the port to 4.32.1, for the reason it gives: +voxgig/struct's lean port and the sdkgen scaffold both pin it, and four +repositories vendored together as one checkpoint cannot be compiled side by +side on three different pins. The workflow kept fetching 4.15.0, so CI +compiles 4.32.1 sources with a compiler that predates the `String.Slice` +changes the port was rewritten for. + +It fails at `make build-lean`, which reads as a port failure and is not one. +Anyone reading a red `lean` check on their own branch learns nothing true +about their change. + +The port's bump landed without this file because an agent session cannot write +it — the same boundary this folder exists for. The comment added above the +step now says the two versions must move together, so the next bump has one +place to look. + +## Checks + +**Both compilers were fetched and the port built under each**, so the +failure this fixes is reproduced rather than inferred. + +``` +v4.15.0 make build-lean + Some required builds logged failures: + - Corpus + - Plugin.Env + - Plugin.Version + error: build failed + +v4.32.1 make build-lean clean + make test-lean 572 corpus entries across 19 sections, all pass +``` + +- `git apply --check` of this patch onto `5c1df34`: clean +- `.github/workflows/ci.yml` parses as YAML after applying, four jobs: + `spec-freshness`, `parity`, `port`, `newer-toolchain` +- the v4.32.1 linux asset resolves at the URL the job builds: + `https://github.com/leanprover/lean4/releases/download/v4.32.1/lean-4.32.1-linux.tar.zst` + +The lean port itself is not touched and needs nothing. What this restores +is CI's ability to say so. diff --git a/tools/check_prose.py b/tools/check_prose.py index e46c60e..53a4931 100755 --- a/tools/check_prose.py +++ b/tools/check_prose.py @@ -74,8 +74,15 @@ # Multi-port layout: one directory per language, each carrying its own # README.md. Every other top-level directory is listed here so that a # directory holding a README.md is a port and nothing else is. +# +# `patch` is a TRANSIENT delivery folder for a change this repository's +# own AGENTS.md says a session cannot push (a workflow), and its README +# is a working document addressed to whoever applies it -- an apply +# command, a diff table, a list of what was checked. It is not a +# reader-facing page. It predates this gate, which is why the gate had +# never met one and called it a twenty-fourth port. PORT_DIRS = True -NOT_PORTS = ("doc", "docs", "spec", "test", "tools", "node_modules") +NOT_PORTS = ("doc", "docs", "patch", "spec", "test", "tools", "node_modules") PORT_PAGES = ("README.md",) # Where "we" is allowed: the tutorial. There is no tutorial PAGE here; From cffa6da2d88a9686efa04d951a62e5c1d448fb38 Mon Sep 17 00:00:00 2001 From: Claude Date: Wed, 16 Sep 2026 10:40:11 +0000 Subject: [PATCH 5/9] export: split the spec at the LAST slash, so a scoped name has exports Register row 6.8, found by Codex's review and reproduced against the canonical: `resolveexport('@acme/store/admin', ...)` answered `undefined`. Section 4's `checkname` permits `/` in a NAME -- `@acme/store` is legal, and section 10.2 resolves a scoped name verbatim -- so splitting at the FIRST `/` read that as the ref `@acme` with the key `store/admin`, which matches nothing. A scoped definition had no spelling for its exports at all. Every `export` entry in the corpus used `probe`, which has no slash, so nothing saw it. THE COST IS STATED RATHER THAN IMPLIED: an export key may not contain `/`. One separator cannot serve both. A name holds slashes because section 4 says so; a key held them only because nothing stopped it, and nothing in this repository or in sekreto declares one. Four corpus entries, all in `export/key`: a scoped ref qualified, the same untagged, the alias half (which has to split the same way or a scoped name resolves qualified and not unqualified), and a scoped miss still answering absent. Reverting the canonical to `indexOf` fails `export/key` and no other group. Canonical plus all 22 ports. Four had no reverse search and take a workaround the comment names: lua walks forward keeping the last hit, elixir takes `List.last(:binary.matches ...)`, haskell and lean split the REVERSED string and put the halves back the right way round. Design section 11 and DOCS.md now state the split and its cost. The design's alias sentence was corrected in the same pass: the key filters candidates before the tag does, so an untagged instance exporting something else does not shadow the tagged one exporting this. Corpus 572 -> 576. All 23 ports build and pass all 576. Co-Authored-By: Claude Opus 5 Claude-Session: https://claude.ai/code/session_01CVMgjjwQfTJ2rXz637Wpk8 --- DOCS.md | 13 ++-- c/src/export.c | 2 +- clojure/src/voxgig/plugin/export.clj | 2 +- cpp/src/export.cpp | 2 +- csharp/src/Export.cs | 2 +- dart/lib/export.dart | 2 +- doc/plan/progress.md | 2 +- docs/design/plugin.md | 23 +++++-- elixir/lib/voxgig_plugin/export.ex | 7 ++- go/plugin/export.go | 2 +- haskell/src/Export.hs | 13 +++- java/src/voxgig/plugin/Export.java | 2 +- javascript/src/export.js | 2 +- kotlin/src/Export.kt | 2 +- lean/src/Plugin/Export.lean | 8 ++- lua/src/plugin/export.lua | 11 +++- ocaml/src/export.ml | 4 +- perl/lib/Voxgig/Plugin/Export.pm | 2 +- php/src/Export.php | 2 +- python/voxgig_plugin/export.py | 2 +- ruby/lib/voxgig_plugin/export.rb | 2 +- rust/src/export.rs | 2 +- scala/src/Export.scala | 2 +- spec/plugin.aon | 48 +++++++++++++++ spec/plugin.json | 92 ++++++++++++++++++++++++++++ swift/src/Export.swift | 2 +- typescript/src/Export.ts | 13 +++- zig/src/export.zig | 2 +- 28 files changed, 227 insertions(+), 41 deletions(-) diff --git a/DOCS.md b/DOCS.md index 9d9eb98..73dc46b 100644 --- a/DOCS.md +++ b/DOCS.md @@ -200,13 +200,12 @@ const admin = host.exports('store$main/admin') admin.write('api.token', 'tok01') ``` -**The spec splits at the FIRST `/`**, so this addresses a definition -whose name has no slash in it. §4's grammar permits one — `@acme/store` -is a legal name, and `resolvecandidates` resolves a scoped name -verbatim — and `@acme/store/admin` therefore reads as the ref `@acme` -with the key `store/admin`, which matches nothing. A scoped definition -has no spelling for its exports today; nothing in the corpus covers it, -and register row 6.8 carries it. +**The spec splits at the LAST `/`**, so a scoped definition works: +`@acme/store/admin` is the ref `@acme/store` with the key `admin`. §4 +permits `/` in a name and `resolvecandidates` resolves a scoped name +verbatim, so the first-slash split left those definitions with no +spelling for their exports at all. The cost is that **an export key may +not contain `/`** — one separator cannot serve both. **A definition may publish as many as it likes**, and the host treats them identically. Two is the usual shape: one the host or its framework diff --git a/c/src/export.c b/c/src/export.c index 4a02667..ed25bbf 100644 --- a/c/src/export.c +++ b/c/src/export.c @@ -20,7 +20,7 @@ static int bytewise(const void *a, const void *b) { Value *resolveexport(Value *spec, Value *exported) { const char *s = visstr(spec) ? vasstr(spec) : ""; - const char *cut = strchr(s, '/'); + const char *cut = strrchr(s, '/'); if (NULL == cut) { size_t sz = strlen(s) + 40; char *text = (char *)arena_alloc(sz); diff --git a/clojure/src/voxgig/plugin/export.clj b/clojure/src/voxgig/plugin/export.clj index dbc75f4..4aa50fc 100644 --- a/clojure/src/voxgig/plugin/export.clj +++ b/clojure/src/voxgig/plugin/export.clj @@ -17,7 +17,7 @@ "`exported` is a list of `{:ref :key :value}` - an internal shape, never a corpus value, so it uses keyword keys where the data does not." [spec exported] - (let [cut (.indexOf ^String spec "/")] + (let [cut (.lastIndexOf ^String spec "/")] (when (neg? cut) (t/fail "plugin_export_ambiguous" (str "export spec needs a key: " spec) {"spec" spec})) diff --git a/cpp/src/export.cpp b/cpp/src/export.cpp index 2934be1..3ff2695 100644 --- a/cpp/src/export.cpp +++ b/cpp/src/export.cpp @@ -17,7 +17,7 @@ namespace plugin { V resolveexport(const V& spec, const V& exported) { const std::string s = isstr(spec) ? asstr(spec) : ""; - size_t cut = s.find('/'); + size_t cut = s.rfind('/'); if (std::string::npos == cut) { fail("plugin_export_ambiguous", "export spec needs a key: " + s, details1("spec", vstr(s))); diff --git a/csharp/src/Export.cs b/csharp/src/Export.cs index 5ba2bf9..8c4ce6a 100644 --- a/csharp/src/Export.cs +++ b/csharp/src/Export.cs @@ -34,7 +34,7 @@ public Exported(string eref, string key, object value) public static object ResolveExport(string spec, List exported) { - var cut = spec.IndexOf('/'); + var cut = spec.LastIndexOf('/'); if (cut < 0) { Types.Fail("plugin_export_ambiguous", "export spec needs a key: " + spec, diff --git a/dart/lib/export.dart b/dart/lib/export.dart index e8c7d0b..2339c04 100644 --- a/dart/lib/export.dart +++ b/dart/lib/export.dart @@ -23,7 +23,7 @@ class Exported { } dynamic resolveExport(String spec, List exported) { - final cut = spec.indexOf('/'); + final cut = spec.lastIndexOf('/'); if (cut < 0) { t.fail('plugin_export_ambiguous', 'export spec needs a key: $spec', {'spec': spec}); diff --git a/doc/plan/progress.md b/doc/plan/progress.md index 4da6693..a73e40a 100644 --- a/doc/plan/progress.md +++ b/doc/plan/progress.md @@ -95,6 +95,6 @@ It did: see 4.1's note and [`handover.md`](handover.md) §13. | 6.1 Six tier-4 ports | **DONE (6/6)** | `c`, `cpp`, `ocaml`, `haskell`, `zig`, `lean` — all six pass all 572 entries, and **twenty-three implementations now do**. Toolchains all reachable: gcc/g++ 13.3.0 present, ghc 9.4.7 and ocaml 4.14.1 from apt, zig 0.13.0 from a ziglang.org tarball, lean 4.15.0 from a pinned GitHub release asset. **The six are deliberately not one port six times**, and §10.3's "tier-4" turned out to describe the LOADER, not the language: it says nothing about closures, exceptions or a garbage collector, and those three are what a port actually costs. `c` builds all three by hand (arena, setjmp/longjmp — safe *because* of the arena — and `volatile` on every local straddling a try, seven of which `-Wclobbered` found); `cpp`, `ocaml` and `haskell` use what their languages have and need none of it; `zig` has none of them and needed a fourth answer. **What each one found is in handover.md §19.** Four defects the corpus caught between them: `point/bail#null-declines` wants PRESENCE not non-null; `resource/scope#difference` wants an early-release handle; `cpp` inherited `c`'s POSIX-ERE regex dialect for the corpus `match` patterns, which are JavaScript literals; and `ocaml` found that a bad number must be a reported error, not a crash, or §9.5's parse-or-string fallback cannot catch it. **Two the corpus could NOT catch**: `check_probes.py` had no `c` row, so it reported `c` green without opening a file; and the `provider` probe carried a dead capability record in `c`, `cpp` and `ocaml` that haskell nearly turned into a real divergence — the lesson being *check the canonical, not the nearest port*. **Two languages refused the shape outright**, which is the durable finding: zig's errors carry no payload, so the diagnostic travels beside the error and every handler takes it first; and **Lean's kernel rejects the definition↔instance cycle every other port takes for granted** (`non positive occurrence of the datatypes being declared`), so the instance api became an explicit record of closures — which is what §6 says a plugin may touch anyway. | | 6.3 Corpus gap 1: shape validation at REGISTRATION | **DONE** | `declare/shape` (7 entries) pins §10.1's TIMING, which `config/optmergebad` says in its own comment it cannot: every entry stops at `define`, so a port deferring the check to resolution raises nothing and fails. Two entries also pin that a valid shape is KEPT rather than validated and dropped, one that a rejected registration leaves nothing behind. **The gap was not cheap and §18's "cheap" was wrong about it**: nothing carried a `shape` because the driver's `define` was a NO-OP in all seventeen ports — a documented three-key verb (DOCS.md §4.2) that registered nothing — so `catalog.add`'s check was unreachable by construction and the `probe` key was ignored by the ten entries passing it. `define` is now implemented everywhere, all three keys live, and `declare/register` (3 entries) pins `probe` distinct from `name`. DOCS.md's "default is `probe`" was wrong and is corrected to `name`; the literal default would have re-backed every `dep`, `noisy` and `greedy` definition with the wrong probe. **Implementing it found a canonical bug**: `apply` handed its resolved options map to `declare`, which ADOPTS it, then refilled that map from itself — so a first-time `apply` left the instance with **no options at all**, and only a second identical apply filled them in. Every `apply` entry asserted status, log or open and none a value the options decide. Fixed in canonical, go, javascript, python, ruby, perl, lua, dart; php, java, csharp, kotlin, rust, swift, scala, elixir, clojure never had it. Three new `apply/idempotent` entries pin it. Corpus 539 -> 552; `make check` green in all seventeen. | | 6.7 Corpus gap 4: a second export key off ONE instance | OPEN | Found while writing DOCS.md §2's *Expose a programmatic API*, for sekreto's mini vault, which publishes `provider` and `vault` from one `define`. §11 says an instance publishes valueS and the `probe` definition exports two (`client` and its own `inst`), but **every `export` entry in the corpus reads the key `client`** — seven reads of one key, plus one absent key. So nothing distinguishes a correct keyed map from a port whose `export` overwrote, or whose `exports` collapsed to one value per instance; whether such a port stays green depends on which key `probe` writes last, which nothing specifies. Closing it needs a probe that exports a second SCALAR key: `probe`'s `inst` is an instance api, shaped differently in every port, so no entry can assert on it. That is a probe-catalog change, so it is a 23-port change set (DOCS.md §4.3) and is recorded here rather than taken on the side of a documentation change. No port is known to be wrong; this is a coverage gap of the same class as 6.4 and 6.5. | -| 6.8 A scoped definition has no export spelling | OPEN | Found by Codex's review of the DOCS.md how-to, and reproduced against the canonical. `resolveexport` splits an export spec at the FIRST `/`, so `@acme/store/admin` reads as the ref `@acme` with the key `store/admin` and answers `undefined`. §4's `checkname` permits `/` in a NAME, and `resolvecandidates` has a branch for scoped names resolving verbatim, so scoped definitions are a supported case with no way to read their exports. Nothing in `export` covers it: every entry there uses `probe`, which has no slash. Closing it is a canonical decision first (an escape, a last-`/` split, or a narrower documented domain for an export spec), then the corpus, then 23 ports — so it is recorded rather than taken on the side of a documentation change. The how-to states the limit meanwhile. | +| 6.8 A scoped definition has no export spelling | **DONE** | Found by Codex's review of the DOCS.md how-to, and reproduced against the canonical. `resolveexport` splits an export spec at the FIRST `/`, so `@acme/store/admin` reads as the ref `@acme` with the key `store/admin` and answers `undefined`. §4's `checkname` permits `/` in a NAME, and `resolvecandidates` has a branch for scoped names resolving verbatim, so scoped definitions are a supported case with no way to read their exports. Nothing in `export` covers it: every entry there uses `probe`, which has no slash. **Closed by the last-`/` split**, canonical plus all 22 ports, and four `export/key` entries (`#scoped`, `#scoped-untagged`, `#scoped-alias`, and a scoped miss). The cost is stated in design §11 and DOCS.md: an export key may not contain `/`, because one separator cannot serve both and a name holds slashes because §4 says so. Four ports had no reverse search and take a documented workaround — lua walks forward keeping the last hit, elixir takes `List.last(:binary.matches ...)`, haskell and lean split the REVERSED string and put the halves back. Reverting the canonical to `indexOf` fails `export/key` and nothing else. Corpus 572 -> 576; all 23 ports green. | | 6.9 §11.1's `inst.capability(name)` does not exist | OPEN | Also from that review. The design says "the first is bound, and `inst.capability(name)` returns it", and the canonical instance api has no such method — `bind`, `export`, `provides`, `acquire`, `release`, `position`, `nest`, and no `capability`. What exists is `host.capability(name)`, which returns provider REFS. So a capability carries selection metadata and a lifecycle edge, and no callable value: a consumer reaches the provider's API through an export or an extension point. That is a design statement no corpus entry can distinguish, which is handover.md §13's first kind exactly. Either implement `inst.capability` or correct §11.1; the how-to documents the behaviour as it is meanwhile. | | 6.2 Does sdkgen adopt plugin? (§17.2) | DECISION NEEDED | Open, uncommitted, and carries a propagation cost across 23 template trees. Gates nested hosts *natively*, deletion of `transport`, and the seventeen-model change. | diff --git a/docs/design/plugin.md b/docs/design/plugin.md index c5b9887..321a557 100644 --- a/docs/design/plugin.md +++ b/docs/design/plugin.md @@ -1623,12 +1623,23 @@ plainly rather than implying a sandbox it does not have: the application: `inst.export('client', theClient)` during `define`. Read with `host.exports('retry$fast/client')`. -The unqualified alias `retry/client` resolves to the **untagged** -instance if one exists. If it does not, and exactly one tagged instance -exports that key, it resolves to that one. If two do, it is -`plugin_export_ambiguous` — deliberately diverging from seneca's silent -last-wins, because with multi-instance as a headline feature, an -ambiguous alias is a defect waiting for production. +**The spec splits at the LAST `/`.** §4 permits `/` in a *name* — +`@acme/store` is legal, and §10.2 resolves a scoped name verbatim — so +splitting at the first one read `@acme/store/client` as the ref `@acme` +with the key `store/client` and answered absent. A scoped definition had +no spelling for its exports at all. The cost is stated rather than +implied: **an export key may not contain `/`**. One separator cannot +serve both, a name holds slashes because §4 says so, and a key held them +only because nothing stopped it. `export/key#scoped` pins it. + +The unqualified alias `retry/client` resolves to the untagged instance +**if that one exports the key**. The key filters the candidates before +the tag does, so an untagged instance publishing something else does not +shadow the tagged one publishing this. If no untagged instance exports +it, and exactly one tagged instance does, it resolves to that one. If +two do, it is `plugin_export_ambiguous` — deliberately diverging from +seneca's silent last-wins, because with multi-instance as a headline +feature, an ambiguous alias is a defect waiting for production. Exports of a `loaded` (not live) instance are **visible**. They are declared in `define`, they are data, and hiding them would make the diff --git a/elixir/lib/voxgig_plugin/export.ex b/elixir/lib/voxgig_plugin/export.ex index 42dfe5e..8c4962b 100644 --- a/elixir/lib/voxgig_plugin/export.ex +++ b/elixir/lib/voxgig_plugin/export.ex @@ -20,8 +20,11 @@ defmodule Voxgig.Plugin.Export do never a corpus value, so it uses atom keys where the data does not. """ def resolve_export(spec, exported) do - case :binary.match(spec, "/") do - :nomatch -> + # THE LAST `/`, not the first: a NAME may hold slashes (§4), a key may + # not. `:binary.matches` returns every hit, so the last one is the + # split; `:binary.match` returns only the first. + case List.last(:binary.matches(spec, "/")) do + nil -> Types.fail("plugin_export_ambiguous", "export spec needs a key: #{spec}", %{"spec" => spec}) diff --git a/go/plugin/export.go b/go/plugin/export.go index 3f2f5ae..a3a7993 100644 --- a/go/plugin/export.go +++ b/go/plugin/export.go @@ -25,7 +25,7 @@ type Exported struct { } func ResolveExport(spec string, exported []Exported) (any, error) { - cut := strings.Index(spec, "/") + cut := strings.LastIndex(spec, "/") if -1 == cut { return nil, Fail("plugin_export_ambiguous", "export spec needs a key: "+spec, map[string]any{"spec": spec}) diff --git a/haskell/src/Export.hs b/haskell/src/Export.hs index 91d6b90..e84c534 100644 --- a/haskell/src/Export.hs +++ b/haskell/src/Export.hs @@ -19,14 +19,21 @@ import Value -- rather than a null Value. resolveExport :: Value -> Value -> IO (Maybe Value) resolveExport spec exported = - case break (== '/') s of - (_, []) -> + case rsplit s of + Nothing -> raise "plugin_export_ambiguous" ("export spec needs a key: " ++ s) (details1 "spec" (VStr s)) - (headS, _ : key) -> pick headS key + Just (headS, key) -> pick headS key where s = if isStr spec then asStr spec else "" + -- THE LAST `/`, not the first: a NAME may hold slashes (§4), a key + -- may not. `break` stops at the first, so the split is taken on the + -- REVERSED string and both halves are put back the right way round. + rsplit str = case break (== '/') (reverse str) of + (_, []) -> Nothing + (rkey, _ : rhead) -> Just (reverse rhead, reverse rkey) + pick headS key = canonRefS headS >>= go headS key -- A fully qualified ref: exactly one answer or none. diff --git a/java/src/voxgig/plugin/Export.java b/java/src/voxgig/plugin/Export.java index 928a059..2600fe2 100644 --- a/java/src/voxgig/plugin/Export.java +++ b/java/src/voxgig/plugin/Export.java @@ -38,7 +38,7 @@ public Exported(String ref, String key, Object value) { } public static Object resolveExport(String spec, List exported) { - int cut = spec.indexOf('/'); + int cut = spec.lastIndexOf('/'); if (cut < 0) { fail("plugin_export_ambiguous", "export spec needs a key: " + spec, details("spec", spec)); } diff --git a/javascript/src/export.js b/javascript/src/export.js index ad0473f..df05405 100644 --- a/javascript/src/export.js +++ b/javascript/src/export.js @@ -16,7 +16,7 @@ const { fail } = require('./types') const { parseref, canonref } = require('./ref') function resolveexport(spec, exported) { - const cut = spec.indexOf('/') + const cut = spec.lastIndexOf('/') if (-1 === cut) { fail('plugin_export_ambiguous', 'export spec needs a key: ' + spec, { spec }) } diff --git a/kotlin/src/Export.kt b/kotlin/src/Export.kt index a11001a..304769f 100644 --- a/kotlin/src/Export.kt +++ b/kotlin/src/Export.kt @@ -19,7 +19,7 @@ object Export { data class Exported(val ref: String, val key: String, val value: Any?) fun resolveExport(spec: String, exported: List): Any? { - val cut = spec.indexOf('/') + val cut = spec.lastIndexOf('/') if (0 > cut) { Types.fail( "plugin_export_ambiguous", "export spec needs a key: $spec", diff --git a/lean/src/Plugin/Export.lean b/lean/src/Plugin/Export.lean index a71b2b4..a130602 100644 --- a/lean/src/Plugin/Export.lean +++ b/lean/src/Plugin/Export.lean @@ -22,8 +22,12 @@ def resolveExport (spec exported : Value) : PluginM (Option Value) := do if !cs.contains '/' then raise "plugin_export_ambiguous" ("export spec needs a key: " ++ s) (details1 "spec" (.str s)) - let head := String.mk (cs.takeWhile (· != '/')) - let key := String.mk ((cs.dropWhile (· != '/')).drop 1) + -- THE LAST `/`, not the first: a NAME may hold slashes (§4), a key may + -- not. `takeWhile` stops at the first, so the split is taken on the + -- REVERSED list and both halves are put back the right way round. + let rcs := cs.reverse + let head := String.mk ((rcs.dropWhile (· != '/')).drop 1).reverse + let key := String.mk (rcs.takeWhile (· != '/')).reverse -- A fully qualified ref: exactly one answer or none. -- diff --git a/lua/src/plugin/export.lua b/lua/src/plugin/export.lua index 4b130ad..0111e49 100644 --- a/lua/src/plugin/export.lua +++ b/lua/src/plugin/export.lua @@ -18,7 +18,16 @@ local M = {} -- `exported` is a plain lua array of {ref=, key=, value=} records: an -- internal shape, never a corpus value, so it is not tagged. function M.resolve_export(spec, exported) - local cut = spec:find('/', 1, true) + -- THE LAST `/`, not the first: a NAME may hold slashes (§4), a key + -- may not. Lua's `find` has no reverse, so walk forward keeping the + -- last hit rather than reaching for a pattern, which would have to + -- escape the separator anyway. + local cut = nil + local at = spec:find('/', 1, true) + while nil ~= at do + cut = at + at = spec:find('/', at + 1, true) + end if nil == cut then T.fail('plugin_export_ambiguous', 'export spec needs a key: ' .. spec, T.map { spec = spec }) diff --git a/ocaml/src/export.ml b/ocaml/src/export.ml index 192d4ed..73047e3 100644 --- a/ocaml/src/export.ml +++ b/ocaml/src/export.ml @@ -15,7 +15,9 @@ module V = Value rather than a null Value. *) let resolveexport spec exported = let s = if V.is_str spec then V.as_str spec else "" in - match String.index_opt s '/' with + (* THE LAST `/`, not the first: a NAME may hold slashes (§4), a key + may not. *) + match String.rindex_opt s '/' with | None -> Types.fail "plugin_export_ambiguous" ("export spec needs a key: " ^ s) diff --git a/perl/lib/Voxgig/Plugin/Export.pm b/perl/lib/Voxgig/Plugin/Export.pm index a9af277..f4c0e74 100644 --- a/perl/lib/Voxgig/Plugin/Export.pm +++ b/perl/lib/Voxgig/Plugin/Export.pm @@ -22,7 +22,7 @@ our @EXPORT_OK = qw(resolve_export); sub resolve_export { my ($spec, $exported) = @_; - my $cut = index($spec, '/'); + my $cut = rindex($spec, '/'); fail_with('plugin_export_ambiguous', "export spec needs a key: $spec", { spec => $spec }) if $cut < 0; diff --git a/php/src/Export.php b/php/src/Export.php index 7d4d004..16dae1a 100644 --- a/php/src/Export.php +++ b/php/src/Export.php @@ -24,7 +24,7 @@ */ function resolve_export(string $spec, array $exported) { - $cut = strpos($spec, '/'); + $cut = strrpos($spec, '/'); if (false === $cut) { fail_with('plugin_export_ambiguous', 'export spec needs a key: ' . $spec, ['spec' => $spec]); diff --git a/python/voxgig_plugin/export.py b/python/voxgig_plugin/export.py index efaf701..f708f8d 100644 --- a/python/voxgig_plugin/export.py +++ b/python/voxgig_plugin/export.py @@ -16,7 +16,7 @@ def resolve_export(spec, exported): - cut = spec.find('/') + cut = spec.rfind('/') if -1 == cut: fail('plugin_export_ambiguous', 'export spec needs a key: ' + spec, {'spec': spec}) diff --git a/ruby/lib/voxgig_plugin/export.rb b/ruby/lib/voxgig_plugin/export.rb index 362ad07..a1490e4 100644 --- a/ruby/lib/voxgig_plugin/export.rb +++ b/ruby/lib/voxgig_plugin/export.rb @@ -17,7 +17,7 @@ module VoxgigPlugin def self.resolve_export(spec, exported) - cut = spec.index('/') + cut = spec.rindex('/') if cut.nil? fail_with('plugin_export_ambiguous', "export spec needs a key: #{spec}", { 'spec' => spec }) diff --git a/rust/src/export.rs b/rust/src/export.rs index 793f9dc..145ad61 100644 --- a/rust/src/export.rs +++ b/rust/src/export.rs @@ -23,7 +23,7 @@ pub struct Exported { } pub fn resolve_export(spec: &str, exported: &[Exported]) -> Result { - let cut = match spec.find('/') { + let cut = match spec.rfind('/') { Some(c) => c, None => { return fail( diff --git a/scala/src/Export.scala b/scala/src/Export.scala index 2aa320c..ecfd94f 100644 --- a/scala/src/Export.scala +++ b/scala/src/Export.scala @@ -18,7 +18,7 @@ object Export { final case class Exported(ref: String, key: String, value: Value) def resolveExport(spec: String, exported: List[Exported]): Value = { - val cut = spec.indexOf('/') + val cut = spec.lastIndexOf('/') if (cut < 0) { Types.fail( "plugin_export_ambiguous", "export spec needs a key: " + spec, diff --git a/spec/plugin.aon b/spec/plugin.aon index 212626e..737dcd1 100644 --- a/spec/plugin.aon +++ b/spec/plugin.aon @@ -3221,6 +3221,54 @@ primary: export: { in: [ { do: 'load', ref: 'probe$a' }, { do: 'export', key: 'probe$a/client' } ] match: { out: { result: 'probe$a' } } } + + # A SCOPED DEFINITION NAME, and the reason the spec splits at the + # LAST `/`. §4's `checkname` permits `/` in a NAME — `@acme/store` is + # legal, and §10.2 resolves a scoped name verbatim — so splitting at + # the FIRST one read this as the ref `@acme` with the key + # `probe$a/client`, matched nothing, and answered absent. A scoped + # definition had no spelling for its exports at all, and every entry + # in this section used `probe`, which has no slash, so nothing saw it. + { + id: 'export/key#scoped', doc: true + in: [ + { do: 'define', name: '@acme/probe', probe: 'probe' } + { do: 'ready', ref: '@acme/probe$a' } + { do: 'export', key: '@acme/probe$a/client' } + ] + match: { out: { result: '@acme/probe$a' } } + } + # Untagged, so the ref IS the name: the exact branch answers. + { + id: 'export/key#scoped-untagged' + in: [ + { do: 'define', name: '@acme/probe', probe: 'probe' } + { do: 'ready', ref: '@acme/probe' } + { do: 'export', key: '@acme/probe/client' } + ] + match: { out: { result: '@acme/probe' } } + } + # The ALIAS half splits the same way, or a scoped name would resolve + # qualified and not unqualified. + { + id: 'export/key#scoped-alias' + in: [ + { do: 'define', name: '@acme/probe', probe: 'probe' } + { do: 'ready', ref: '@acme/probe$a' } + { do: 'export', key: '@acme/probe/client' } + ] + match: { out: { result: '@acme/probe$a' } } + } + # A key nothing exports is still absent, scoped or not — the split + # moved, the answer for a miss did not. + { + in: [ + { do: 'define', name: '@acme/probe', probe: 'probe' } + { do: 'ready', ref: '@acme/probe$a' } + { do: 'export', key: '@acme/probe$a/nope' } + ] + match: { out: { result: '__NULL__' } } + } ] diff --git a/spec/plugin.json b/spec/plugin.json index ef30b2b..eed9910 100644 --- a/spec/plugin.json +++ b/spec/plugin.json @@ -8176,6 +8176,98 @@ "result": "probe$a" } } + }, + { + "doc": true, + "id": "export/key#scoped", + "in": [ + { + "do": "define", + "name": "@acme/probe", + "probe": "probe" + }, + { + "do": "ready", + "ref": "@acme/probe$a" + }, + { + "do": "export", + "key": "@acme/probe$a/client" + } + ], + "match": { + "out": { + "result": "@acme/probe$a" + } + } + }, + { + "id": "export/key#scoped-untagged", + "in": [ + { + "do": "define", + "name": "@acme/probe", + "probe": "probe" + }, + { + "do": "ready", + "ref": "@acme/probe" + }, + { + "do": "export", + "key": "@acme/probe/client" + } + ], + "match": { + "out": { + "result": "@acme/probe" + } + } + }, + { + "id": "export/key#scoped-alias", + "in": [ + { + "do": "define", + "name": "@acme/probe", + "probe": "probe" + }, + { + "do": "ready", + "ref": "@acme/probe$a" + }, + { + "do": "export", + "key": "@acme/probe/client" + } + ], + "match": { + "out": { + "result": "@acme/probe$a" + } + } + }, + { + "in": [ + { + "do": "define", + "name": "@acme/probe", + "probe": "probe" + }, + { + "do": "ready", + "ref": "@acme/probe$a" + }, + { + "do": "export", + "key": "@acme/probe$a/nope" + } + ], + "match": { + "out": { + "result": "__NULL__" + } + } } ] } diff --git a/swift/src/Export.swift b/swift/src/Export.swift index 62d1e0c..1fe23e7 100644 --- a/swift/src/Export.swift +++ b/swift/src/Export.swift @@ -25,7 +25,7 @@ public enum Export { } public static func resolveExport(_ spec: String, _ exported: [Exported]) throws -> Value { - guard let cut = spec.firstIndex(of: "/") else { + guard let cut = spec.lastIndex(of: "/") else { throw Types.fail( "plugin_export_ambiguous", "export spec needs a key: \(spec)", ["spec": .str(spec)] diff --git a/typescript/src/Export.ts b/typescript/src/Export.ts index 96d613d..bcefdcf 100644 --- a/typescript/src/Export.ts +++ b/typescript/src/Export.ts @@ -16,7 +16,18 @@ import { parseref, canonref } from './Ref' export type Exported = { ref: string, key: string, value: any } export function resolveexport(spec: string, exported: Exported[]): any { - const cut = spec.indexOf('/') + // THE LAST SLASH, not the first. §4's `checkname` permits `/` in a + // NAME — `@acme/store` is legal, and `resolvecandidates` has a branch + // for resolving a scoped name verbatim — so splitting at the first one + // read `@acme/store/client` as the ref `@acme` with the key + // `store/client`, which matches nothing. A scoped definition had no + // spelling for its exports at all, and said so by answering absent. + // + // The cost is that an export KEY may not contain `/`. Nothing declares + // one, no port shipped one, and the two cannot both be reachable with + // one separator: a name may hold slashes because §4 says so, a key + // holds them because nobody stopped it. + const cut = spec.lastIndexOf('/') if (-1 === cut) { fail('plugin_export_ambiguous', 'export spec needs a key: ' + spec, { spec }) } diff --git a/zig/src/export.zig b/zig/src/export.zig index 73ef509..cfe6872 100644 --- a/zig/src/export.zig +++ b/zig/src/export.zig @@ -21,7 +21,7 @@ fn lessStr(_: void, a: []const u8, b: []const u8) bool { /// rather than a null Value. pub fn resolveexport(spec: ?*v.Value, exported: ?*v.Value) t.Err!?*v.Value { const s = if (v.isStr(spec)) v.asStr(spec) else ""; - const cut = std.mem.indexOfScalar(u8, s, '/') orelse + const cut = std.mem.lastIndexOfScalar(u8, s, '/') orelse return t.fail("plugin_export_ambiguous", v.print("export spec needs a key: {s}", .{s}), t.details1("spec", v.vstr(s))); const head = s[0..cut]; const key = s[cut + 1 ..]; From 7e4191b545ec3be4124b2eae08d30d6c8a403e89 Mon Sep 17 00:00:00 2001 From: Claude Date: Wed, 16 Sep 2026 10:47:12 +0000 Subject: [PATCH 6/9] export: a second scalar key on `probe`, and what it actually pins Register row 6.7. `probe` exports `mark`, the constant `marked`, beside `client` and `inst`, and four entries read a second key off one instance: `export/key#second-key`, `#two-keys`, `#two-keys-reversed` and `export/alias#second-key`. THE GAP AS FIRST WRITTEN WAS OVERSTATED, and measuring it is what said so. The claim was that a port whose `export` overwrote rather than keyed could stay green. It could not: `probe` writes `client` before `inst`, so an overwriting `export` hands an instance api back for `client` and fails outright, and a lookup that IGNORES the key is caught by the absent-key entry `probe$a/nope`, because ignoring the key makes a missing key present. What nothing could distinguish is narrower and more plausible: a lookup that CHECKS the key is present and then answers with the instance's FIRST export. Presence-checked, position-answered. Mutated both branches that way and measured against both corpora: exact branch, 572 entries export/key and export/alias GREEN (featurehost-bridge and resource/scope fail, but only because the DRIVER reads exports(ref + '/inst') for `stray` -- not an entry asserting anything) exact branch, 580 entries export/key fails alias branch, 572 entries the WHOLE suite green, 0 failures alias branch, 580 entries export/alias fails, and nothing else So a port could have got exports wrong and been told by a resource test, which is the wrong place to learn it, or not told at all. A CONSTANT rather than the tag or the name, because it is the same literal in twenty-three languages and needs no accessor; `inst` cannot close the gap because it is an instance api, shaped differently in every port, and no entry can assert on it. 23 drivers, DOCS.md section 4.3's probe table. Corpus 576 -> 580, all 23 ports build and pass all 580. Co-Authored-By: Claude Opus 5 Claude-Session: https://claude.ai/code/session_01CVMgjjwQfTJ2rXz637Wpk8 --- DOCS.md | 2 +- c/test/driver.c | 2 + clojure/test/voxgig/plugin/driver.clj | 2 + cpp/test/driver.cpp | 2 + csharp/test/Driver.cs | 2 + dart/test/driver.dart | 2 + doc/plan/progress.md | 2 +- doc/plan/status.md | 16 ++--- elixir/test/driver.exs | 2 + go/test/driver.go | 2 + haskell/test/Driver.hs | 2 + java/test/voxgig/plugin/test/Driver.java | 2 + javascript/test/driver.js | 2 + kotlin/test/Driver.kt | 2 + lean/test/Driver.lean | 2 + lua/test/driver.lua | 2 + ocaml/test/driver.ml | 2 + perl/test/Driver.pm | 2 + php/test/driver.php | 2 + python/test/driver.py | 2 + ruby/test/driver.rb | 2 + rust/tests/support/driver.rs | 2 + scala/test/Driver.scala | 2 + spec/plugin.aon | 44 +++++++++++++ spec/plugin.json | 81 ++++++++++++++++++++++++ swift/test/Driver.swift | 2 + typescript/test/driver.ts | 6 ++ zig/test/driver.zig | 2 + 28 files changed, 185 insertions(+), 10 deletions(-) diff --git a/DOCS.md b/DOCS.md index 73dc46b..7101144 100644 --- a/DOCS.md +++ b/DOCS.md @@ -470,7 +470,7 @@ in the same way. | probe | behaviour | |---|---| -| `probe` | The workhorse. Records every callback it receives into the log, binds one hook point (`p`), wraps one chain point (`c`), holds an integer counter in its state, and **acquires exactly one synthetic resource per activation**. It also exports its own instance api as `inst`, which is how the `stray` command reaches `release` from *outside* a lifecycle callback. | +| `probe` | The workhorse. Records every callback it receives into the log, binds one hook point (`p`), wraps one chain point (`c`), holds an integer counter in its state, and **acquires exactly one synthetic resource per activation**. It exports three keys: `client`, its own ref; `mark`, the constant `marked`; and `inst`, its own instance api, which is how the `stray` command reaches `release` from *outside* a lifecycle callback. **`mark` is there so an entry can read a SECOND key off one instance** — every `export` entry once read `client`, so a port whose `exports` ignored the key and answered with the instance's first export passed all of them, and `inst` cannot close that because no entry can assert on an instance api. | | `noisy` | Fails on demand. `options.fail` names the callback that raises — `define`, `activate`, `deactivate` or `close` — and `options.code` the error code. `options.bare` raises with **no code at all**, which is the ordinary library error §12's `plugin__failed` codes exist to wrap. Everything else is `probe`. | | `greedy` | Acquires `options.acquire` resources on activation and releases `options.release` of them explicitly, so the difference is what the instance scope must unwind (§8.3). `options.early` acquires in **`define`** instead, where §8.1 says capture does not belong. `options.bind` names the callback (`activate` or `deactivate`) that declares a **binding** outside `define`, which is §8.1's other half and §12's `plugin_bind_scope`. `options.mark` additionally registers that many **foreign** releases through `release`, each recording its own index into `state.unwound` as it runs — which is the only way the *direction* of the unwind is observable, since an acquired handle is an idempotent counter decrement that reads the same either way. `options.markfail` makes each of those releases **raise**, which is the only way §8.3's `plugin_release_failed` and its `failed` status are reachable. | | `dep` | Declares requirements. `options.requires` is a list of refs or capability names, `options.optional` those that are optional rather than mandatory. | diff --git a/c/test/driver.c b/c/test/driver.c index f783131..fcf429f 100644 --- a/c/test/driver.c +++ b/c/test/driver.c @@ -110,6 +110,8 @@ static void probe_define(Inst *i) { inst_bind(i, "p", probe_hook, NULL, i, band); inst_bind(i, "c", NULL, probe_chain, i, band); inst_export(i, "client", vstr(inst_ref(i))); + /* A SECOND SCALAR KEY; see typescript/test/driver.ts. */ + inst_export(i, "mark", vstr("marked")); /* The instance api itself, so the driver's `stray` command can call * `release` from OUTSIDE a lifecycle callback — which is the only way * to exercise §8.3's scope guard. C cannot put a pointer in a Value, diff --git a/clojure/test/voxgig/plugin/driver.clj b/clojure/test/voxgig/plugin/driver.clj index 341fd8d..525262a 100644 --- a/clojure/test/voxgig/plugin/driver.clj +++ b/clojure/test/voxgig/plugin/driver.clj @@ -81,6 +81,8 @@ ;; backwards and make every chain expectation read wrong. (h/bind! i "c" (fn [nxt v] (str (or (opt i "wrap") ":") (nxt v))) band)) (h/export! i "client" (h/inst-ref i)) + ;; A SECOND SCALAR KEY; see typescript/test/driver.ts. + (h/export! i "mark" "marked") ;; The instance api itself, so the driver's `stray` command can call ;; `release` from OUTSIDE a lifecycle callback. (h/export! i "inst" i) diff --git a/cpp/test/driver.cpp b/cpp/test/driver.cpp index 67f83f1..9539543 100644 --- a/cpp/test/driver.cpp +++ b/cpp/test/driver.cpp @@ -91,6 +91,8 @@ static void probedefine(Inst& i) { boom(i, "define"); bindprobe(i); i.exportvalue("client", vstr(i.ref())); + // A SECOND SCALAR KEY; see typescript/test/driver.ts. + i.exportvalue("mark", vstr("marked")); /* The instance api itself, so the driver's `stray` command can call * `release` from OUTSIDE a lifecycle callback — which is the only way * to exercise §8.3's scope guard. The driver looks the instance up by diff --git a/csharp/test/Driver.cs b/csharp/test/Driver.cs index 288cccc..4166abe 100644 --- a/csharp/test/Driver.cs +++ b/csharp/test/Driver.cs @@ -67,6 +67,8 @@ public static List Probes() return wrap + Text(inner); }, band); i.Export("client", i.Ref); + // A SECOND SCALAR KEY; see typescript/test/driver.ts. + i.Export("mark", "marked"); // The instance api itself, so the driver's `stray` command // can call `release` from OUTSIDE a lifecycle callback. i.Export("inst", i); diff --git a/dart/test/driver.dart b/dart/test/driver.dart index 7172254..da293c5 100644 --- a/dart/test/driver.dart +++ b/dart/test/driver.dart @@ -96,6 +96,8 @@ List probes() { // backwards and make every chain expectation read wrong. i.bind('c', (next, v) => '${_opt(i, 'wrap') ?? ':'}${next(v)}', band); i.export('client', i.ref); + // A SECOND SCALAR KEY; see typescript/test/driver.ts. + i.export('mark', 'marked'); // The instance api itself, so the driver's `stray` command can call // `release` from OUTSIDE a lifecycle callback. i.export('inst', i); diff --git a/doc/plan/progress.md b/doc/plan/progress.md index a73e40a..c9131b7 100644 --- a/doc/plan/progress.md +++ b/doc/plan/progress.md @@ -94,7 +94,7 @@ It did: see 4.1's note and [`handover.md`](handover.md) §13. | 6.6 The ref rule, everywhere the graph is examined | **DONE** | Codex's review of the gap-2 PR said the close was premature, and it was right — for a reason larger than the finding. §11.1 says a ref satisfies a requirement, and THREE places read a requirement name: runtime `providersof`, load-time `dependencycycle`, and whole-graph `resolve`. Only the first implemented the rule. **Four canonical defects, all now fixed and pinned.** (a) `providersof` canonicalized EVERY requirement name, so a capability called `2fa` or `my cap` — both legal, since §4's grammar is on plugin names and the design puts none on capability names — raised `plugin_bad_name` and killed a legal document; every capability name in the corpus happened to be a well-formed ref, and nine ports had independently worked around it with a try/except or a tolerant `canon`, so the canonical was the outlier and nothing caught it. (b) `dependencycycle` indexed providers by canonical ref and looked them up with the raw name, so the same cycle spelled `dep$`/`other$` produced no edges and EVADED the load-time check entirely. (c) `graph.candidates` never considered node refs at all, so `resolve()` answered `absent` about a provider the runtime binds — even in the canonical spelling. (d) The design text asserted ref loss always sends a consumer to `pending`; it follows the ordinary cardinality/policy rules, so mandatory-`dynamic` stays live and optional never gated. Canonical gains a tolerant `tryref`; every port uses its own existing tolerant spelling. Eleven new entries across `depend/byref`, `depend/cycle` and `graph/resolve`+`blocked`; each targeted mutant fails its group and no other. Corpus 561 -> 572. | | 6.1 Six tier-4 ports | **DONE (6/6)** | `c`, `cpp`, `ocaml`, `haskell`, `zig`, `lean` — all six pass all 572 entries, and **twenty-three implementations now do**. Toolchains all reachable: gcc/g++ 13.3.0 present, ghc 9.4.7 and ocaml 4.14.1 from apt, zig 0.13.0 from a ziglang.org tarball, lean 4.15.0 from a pinned GitHub release asset. **The six are deliberately not one port six times**, and §10.3's "tier-4" turned out to describe the LOADER, not the language: it says nothing about closures, exceptions or a garbage collector, and those three are what a port actually costs. `c` builds all three by hand (arena, setjmp/longjmp — safe *because* of the arena — and `volatile` on every local straddling a try, seven of which `-Wclobbered` found); `cpp`, `ocaml` and `haskell` use what their languages have and need none of it; `zig` has none of them and needed a fourth answer. **What each one found is in handover.md §19.** Four defects the corpus caught between them: `point/bail#null-declines` wants PRESENCE not non-null; `resource/scope#difference` wants an early-release handle; `cpp` inherited `c`'s POSIX-ERE regex dialect for the corpus `match` patterns, which are JavaScript literals; and `ocaml` found that a bad number must be a reported error, not a crash, or §9.5's parse-or-string fallback cannot catch it. **Two the corpus could NOT catch**: `check_probes.py` had no `c` row, so it reported `c` green without opening a file; and the `provider` probe carried a dead capability record in `c`, `cpp` and `ocaml` that haskell nearly turned into a real divergence — the lesson being *check the canonical, not the nearest port*. **Two languages refused the shape outright**, which is the durable finding: zig's errors carry no payload, so the diagnostic travels beside the error and every handler takes it first; and **Lean's kernel rejects the definition↔instance cycle every other port takes for granted** (`non positive occurrence of the datatypes being declared`), so the instance api became an explicit record of closures — which is what §6 says a plugin may touch anyway. | | 6.3 Corpus gap 1: shape validation at REGISTRATION | **DONE** | `declare/shape` (7 entries) pins §10.1's TIMING, which `config/optmergebad` says in its own comment it cannot: every entry stops at `define`, so a port deferring the check to resolution raises nothing and fails. Two entries also pin that a valid shape is KEPT rather than validated and dropped, one that a rejected registration leaves nothing behind. **The gap was not cheap and §18's "cheap" was wrong about it**: nothing carried a `shape` because the driver's `define` was a NO-OP in all seventeen ports — a documented three-key verb (DOCS.md §4.2) that registered nothing — so `catalog.add`'s check was unreachable by construction and the `probe` key was ignored by the ten entries passing it. `define` is now implemented everywhere, all three keys live, and `declare/register` (3 entries) pins `probe` distinct from `name`. DOCS.md's "default is `probe`" was wrong and is corrected to `name`; the literal default would have re-backed every `dep`, `noisy` and `greedy` definition with the wrong probe. **Implementing it found a canonical bug**: `apply` handed its resolved options map to `declare`, which ADOPTS it, then refilled that map from itself — so a first-time `apply` left the instance with **no options at all**, and only a second identical apply filled them in. Every `apply` entry asserted status, log or open and none a value the options decide. Fixed in canonical, go, javascript, python, ruby, perl, lua, dart; php, java, csharp, kotlin, rust, swift, scala, elixir, clojure never had it. Three new `apply/idempotent` entries pin it. Corpus 539 -> 552; `make check` green in all seventeen. | -| 6.7 Corpus gap 4: a second export key off ONE instance | OPEN | Found while writing DOCS.md §2's *Expose a programmatic API*, for sekreto's mini vault, which publishes `provider` and `vault` from one `define`. §11 says an instance publishes valueS and the `probe` definition exports two (`client` and its own `inst`), but **every `export` entry in the corpus reads the key `client`** — seven reads of one key, plus one absent key. So nothing distinguishes a correct keyed map from a port whose `export` overwrote, or whose `exports` collapsed to one value per instance; whether such a port stays green depends on which key `probe` writes last, which nothing specifies. Closing it needs a probe that exports a second SCALAR key: `probe`'s `inst` is an instance api, shaped differently in every port, so no entry can assert on it. That is a probe-catalog change, so it is a 23-port change set (DOCS.md §4.3) and is recorded here rather than taken on the side of a documentation change. No port is known to be wrong; this is a coverage gap of the same class as 6.4 and 6.5. | +| 6.7 Corpus gap 4: a second export key off ONE instance | **DONE** | `probe` now exports `mark`, the constant `marked`, beside `client` and `inst`; four entries read a second key (`export/key#second-key`, `#two-keys`, `#two-keys-reversed`, `export/alias#second-key`). **The gap as first written was overstated, and measuring it is what said so.** A port that IGNORED the key outright was already caught, by the absent-key entry `probe$a/nope`: ignoring the key makes a missing key present. What nothing could distinguish is a lookup that CHECKS the key is present and then answers with the instance's FIRST export — presence-checked, position-answered. Mutated both branches that way and measured: against the 572-entry corpus the exact branch left `export/key` and `export/alias` green (only `featurehost-bridge` and `resource/scope` failed, and both only because the DRIVER reads `exports(ref + '/inst')` for `stray`, which is not an entry asserting anything); the alias branch left the WHOLE suite green, 0 failures. Against 580 each is caught by its own group and nothing else. So a port could have got exports wrong and been told by a resource test, or not told at all. `inst` cannot close this — it is an instance api, shaped differently in every port, and no entry can assert on it; a constant can. 23 drivers, DOCS.md §4.3. Corpus 576 -> 580; all 23 ports green. | | 6.8 A scoped definition has no export spelling | **DONE** | Found by Codex's review of the DOCS.md how-to, and reproduced against the canonical. `resolveexport` splits an export spec at the FIRST `/`, so `@acme/store/admin` reads as the ref `@acme` with the key `store/admin` and answers `undefined`. §4's `checkname` permits `/` in a NAME, and `resolvecandidates` has a branch for scoped names resolving verbatim, so scoped definitions are a supported case with no way to read their exports. Nothing in `export` covers it: every entry there uses `probe`, which has no slash. **Closed by the last-`/` split**, canonical plus all 22 ports, and four `export/key` entries (`#scoped`, `#scoped-untagged`, `#scoped-alias`, and a scoped miss). The cost is stated in design §11 and DOCS.md: an export key may not contain `/`, because one separator cannot serve both and a name holds slashes because §4 says so. Four ports had no reverse search and take a documented workaround — lua walks forward keeping the last hit, elixir takes `List.last(:binary.matches ...)`, haskell and lean split the REVERSED string and put the halves back. Reverting the canonical to `indexOf` fails `export/key` and nothing else. Corpus 572 -> 576; all 23 ports green. | | 6.9 §11.1's `inst.capability(name)` does not exist | OPEN | Also from that review. The design says "the first is bound, and `inst.capability(name)` returns it", and the canonical instance api has no such method — `bind`, `export`, `provides`, `acquire`, `release`, `position`, `nest`, and no `capability`. What exists is `host.capability(name)`, which returns provider REFS. So a capability carries selection metadata and a lifecycle edge, and no callable value: a consumer reaches the provider's API through an export or an extension point. That is a design statement no corpus entry can distinguish, which is handover.md §13's first kind exactly. Either implement `inst.capability` or correct §11.1; the how-to documents the behaviour as it is meanwhile. | | 6.2 Does sdkgen adopt plugin? (§17.2) | DECISION NEEDED | Open, uncommitted, and carries a propagation cost across 23 template trees. Gates nested hosts *natively*, deletion of `transport`, and the seventeen-model change. | diff --git a/doc/plan/status.md b/doc/plan/status.md index 4882641..df42c08 100644 --- a/doc/plan/status.md +++ b/doc/plan/status.md @@ -224,14 +224,14 @@ table is the summary, that file is the authority. Neither blocks P1. `resolvecandidates` handles) has no spelling for its exports. Row **6.9**: §11.1 says `inst.capability(name)` returns the bound provider and the canonical instance api has no such method, so a capability - carries no callable value. And row **6.7**: **every `export` entry reads the - key `client`**. The `probe` definition exports two keys, but nothing - reads the second, so a port whose `export` overwrote rather than keyed - could stay green depending on write order. Closing it needs `probe` to - export a second SCALAR key — its `inst` export is an instance api and no - entry can assert on it — and a probe-catalog change is a 23-port change - set. No port is known to be wrong; this is the same class as gaps 2 and - 3, which also needed no port change. + carries no callable value. And row **6.7**: no `export` entry read a + SECOND key off one instance. **All three are now closed**, and 6.7's + first description was overstated: a port that ignored the key outright + was already caught by the absent-key entry, because ignoring the key + makes a missing key present. What nothing could distinguish is a lookup + that checks the key is present and then answers with the instance's + first export. Mutated that way, the alias branch left the whole suite + green. Measuring the gap is what corrected the claim about it. - **The scala and kotlin ports are built under both their compilers** — #29 and #30 made the ports accept two major versions each, and #31 diff --git a/elixir/test/driver.exs b/elixir/test/driver.exs index 3510737..acfb4e8 100644 --- a/elixir/test/driver.exs +++ b/elixir/test/driver.exs @@ -62,6 +62,8 @@ defmodule Driver do # backwards and make every chain expectation read wrong. Inst.bind(i, "c", fn next, v -> "#{opt(i, "wrap") || ":"}#{next.(v)}" end, band) Inst.export(i, "client", Inst.ref(i)) + # A SECOND SCALAR KEY; see typescript/test/driver.ts. + Inst.export(i, "mark", "marked") # The instance api itself, so the driver's `stray` command can call # `release` from OUTSIDE a lifecycle callback. Inst.export(i, "inst", i) diff --git a/go/test/driver.go b/go/test/driver.go index 14ea879..e68f725 100644 --- a/go/test/driver.go +++ b/go/test/driver.go @@ -65,6 +65,8 @@ func Probes() []plugin.Definition { return err } i.Export("client", i.Ref()) + // A SECOND SCALAR KEY; see typescript/test/driver.ts. + i.Export("mark", "marked") // The instance api itself, so the driver's `stray` command // can call Release from OUTSIDE a lifecycle callback. i.Export("inst", i) diff --git a/haskell/test/Driver.hs b/haskell/test/Driver.hs index 068923c..d204aec 100644 --- a/haskell/test/Driver.hs +++ b/haskell/test/Driver.hs @@ -127,6 +127,8 @@ probeDefine i = do boom i "define" bindProbe i instExport i "client" (VStr (iRef i)) + -- A SECOND SCALAR KEY; see typescript/test/driver.ts. + instExport i "mark" (VStr "marked") -- The instance api itself, so the driver's @stray@ command can call -- @release@ from OUTSIDE a lifecycle callback — which is the only way -- to exercise §8.3's scope guard. The driver looks the instance up by diff --git a/java/test/voxgig/plugin/test/Driver.java b/java/test/voxgig/plugin/test/Driver.java index eccd99c..f6839f3 100644 --- a/java/test/voxgig/plugin/test/Driver.java +++ b/java/test/voxgig/plugin/test/Driver.java @@ -79,6 +79,8 @@ public static List probes() { }, band); i.export("client", i.ref); + // A SECOND SCALAR KEY; see typescript/test/driver.ts. + i.export("mark", "marked"); // The instance api itself, so the driver's `stray` command can // call `release` from OUTSIDE a lifecycle callback. i.export("inst", i); diff --git a/javascript/test/driver.js b/javascript/test/driver.js index bddc1c8..4b5f0a9 100644 --- a/javascript/test/driver.js +++ b/javascript/test/driver.js @@ -32,6 +32,8 @@ function probes() { i.bind('c', (next, v) => (i.options && i.options.wrap ? i.options.wrap : ':') + next(v), i.options && i.options.band) i.export('client', i.ref) + // A SECOND SCALAR KEY; see typescript/test/driver.ts. + i.export('mark', 'marked') // The instance api itself, so the driver's `stray` command can // call `release` from OUTSIDE a lifecycle callback. i.export('inst', i) diff --git a/kotlin/test/Driver.kt b/kotlin/test/Driver.kt index d6ed9fd..16c1500 100644 --- a/kotlin/test/Driver.kt +++ b/kotlin/test/Driver.kt @@ -117,6 +117,8 @@ object Driver { "${opt(i, "wrap") ?: ":"}${inner(v)}" }, band) i.export("client", i.ref) + // A SECOND SCALAR KEY; see typescript/test/driver.ts. + i.export("mark", "marked") // The instance api itself, so the driver's `stray` command can // call `release` from OUTSIDE a lifecycle callback. i.export("inst", i) diff --git a/lean/test/Driver.lean b/lean/test/Driver.lean index e5b374b..77a63d2 100644 --- a/lean/test/Driver.lean +++ b/lean/test/Driver.lean @@ -80,6 +80,8 @@ def probeDefine (i : InstApi) : PluginM Unit := do boom i "define" bindProbe i i.exportValue "client" (.str i.ref) + -- A SECOND SCALAR KEY; see typescript/test/driver.ts. + i.exportValue "mark" (.str "marked") -- The instance api itself, so the driver's `stray` command can call -- `release` from OUTSIDE a lifecycle callback — which is the only way -- to exercise §8.3's scope guard. The driver looks the instance up by diff --git a/lua/test/driver.lua b/lua/test/driver.lua index bf2e3fb..043e1fb 100644 --- a/lua/test/driver.lua +++ b/lua/test/driver.lua @@ -106,6 +106,8 @@ function M.probes() return wrap .. text(nxt(v)) end, band) i:export('client', i.ref) + -- A SECOND SCALAR KEY; see typescript/test/driver.ts. + i:export('mark', 'marked') -- The instance api itself, so the driver's `stray` command can call -- `release` from OUTSIDE a lifecycle callback. i:export('inst', i) diff --git a/ocaml/test/driver.ml b/ocaml/test/driver.ml index c2bc8da..dafb6d2 100644 --- a/ocaml/test/driver.ml +++ b/ocaml/test/driver.ml @@ -140,6 +140,8 @@ let probedefine (i : inst) = boom i "define"; bindprobe i; Host.exportvalue i "client" (V.vstr i.iref); + (* A SECOND SCALAR KEY; see typescript/test/driver.ts. *) + Host.exportvalue i "mark" (V.vstr "marked"); (* The instance api itself, so the driver's `stray` command can call `release` from OUTSIDE a lifecycle callback — which is the only way to exercise §8.3's scope guard. The driver looks the instance diff --git a/perl/test/Driver.pm b/perl/test/Driver.pm index 1afb021..7e8e555 100644 --- a/perl/test/Driver.pm +++ b/perl/test/Driver.pm @@ -58,6 +58,8 @@ sub probes { return ($i->options->{wrap} // ':') . $nxt->($v); }, $band); $i->export('client', $i->ref); + # A SECOND SCALAR KEY; see typescript/test/driver.ts. + $i->export('mark', 'marked'); # The instance api itself, so the driver's `stray` command can # call `release` from OUTSIDE a lifecycle callback. $i->export('inst', $i); diff --git a/php/test/driver.php b/php/test/driver.php index d124baa..13ea62d 100644 --- a/php/test/driver.php +++ b/php/test/driver.php @@ -77,6 +77,8 @@ public static function probes(): array return ($i->options()['wrap'] ?? ':') . $nxt($v); }, $band); $i->export('client', $i->ref); + // A SECOND SCALAR KEY; see typescript/test/driver.ts. + $i->export('mark', 'marked'); // The instance api itself, so the driver's `stray` command // can call `release` from OUTSIDE a lifecycle callback. $i->export('inst', $i); diff --git a/python/test/driver.py b/python/test/driver.py index 84e9030..9ad51b3 100644 --- a/python/test/driver.py +++ b/python/test/driver.py @@ -33,6 +33,8 @@ def probe_define(i): i.bind('c', lambda nxt, v: (i.options.get('wrap') or ':') + str(nxt(v)), band) i.export('client', i.ref) + # A SECOND SCALAR KEY; see typescript/test/driver.ts. + i.export('mark', 'marked') # The instance api itself, so the driver's `stray` command can # call `release` from OUTSIDE a lifecycle callback. i.export('inst', i) diff --git a/ruby/test/driver.rb b/ruby/test/driver.rb index fb6f6d9..7e1229e 100644 --- a/ruby/test/driver.rb +++ b/ruby/test/driver.rb @@ -38,6 +38,8 @@ def self.probes # spell it backwards and make every chain expectation read wrong. i.bind('c', ->(nxt, v) { "#{i.options['wrap'] || ':'}#{nxt.call(v)}" }, band) i.export('client', i.ref) + # A SECOND SCALAR KEY; see typescript/test/driver.ts. + i.export('mark', 'marked') # The instance api itself, so the driver's `stray` command can # call `release` from OUTSIDE a lifecycle callback. i.export('inst', i) diff --git a/rust/tests/support/driver.rs b/rust/tests/support/driver.rs index 73ed628..6cad37f 100644 --- a/rust/tests/support/driver.rs +++ b/rust/tests/support/driver.rs @@ -73,6 +73,8 @@ pub fn probes() -> Vec { i.bind("c", chainfn, &band)?; i.export("client", Value::str(&i.eref)); + // A SECOND SCALAR KEY; see typescript/test/driver.ts. + i.export("mark", Value::str("marked")); // The instance api itself, so the driver's `stray` command can // call `release` from OUTSIDE a lifecycle callback. i.export("inst", Value::Opaque(Rc::new(i.clone()))); diff --git a/scala/test/Driver.scala b/scala/test/Driver.scala index 9011670..aaaaecb 100644 --- a/scala/test/Driver.scala +++ b/scala/test/Driver.scala @@ -111,6 +111,8 @@ object Driver { VStr(wrap + inner.asString.getOrElse(inner.json)) }, band) i.`export`("client", VStr(i.ref)) + // A SECOND SCALAR KEY; see typescript/test/driver.ts. + i.`export`("mark", VStr("marked")) // The instance api itself, so the driver's `stray` command can call // `release` from OUTSIDE a lifecycle callback. i.`export`("inst", VOpaque(i)) diff --git a/spec/plugin.aon b/spec/plugin.aon index 737dcd1..2ad355c 100644 --- a/spec/plugin.aon +++ b/spec/plugin.aon @@ -3222,6 +3222,43 @@ primary: export: { match: { out: { result: 'probe$a' } } } + # A SECOND KEY OFF ONE INSTANCE, which is what makes the map a MAP. + # + # Every other entry here reads `client`, so a port whose `exports` + # ignored the key and answered with the instance's first export + # passed all of them. `probe` exports `client` (its ref), `mark` (a + # constant) and `inst` (its own api) -- and `inst` cannot close this, + # because it is shaped differently in every port and no entry can + # assert on it. A constant can. + { + id: 'export/key#second-key', doc: true + in: [ { do: 'ready', ref: 'probe$a' }, { do: 'export', key: 'probe$a/mark' } ] + match: { out: { result: 'marked' } } + } + # BOTH ORDERS, because one of them is what a first-export-wins port + # would pass: reading `client` then `mark` must answer `marked`... + { + id: 'export/key#two-keys' + in: [ + { do: 'ready', ref: 'probe$a' } + { do: 'export', key: 'probe$a/client' } + { do: 'export', key: 'probe$a/mark' } + ] + match: { out: { result: 'marked' } } + } + # ...and reading `mark` then `client` must answer the ref. A port + # answering from position rather than from the key fails one of these + # whichever position it picks. + { + id: 'export/key#two-keys-reversed' + in: [ + { do: 'ready', ref: 'probe$a' } + { do: 'export', key: 'probe$a/mark' } + { do: 'export', key: 'probe$a/client' } + ] + match: { out: { result: 'probe$a' } } + } + # A SCOPED DEFINITION NAME, and the reason the spec splits at the # LAST `/`. §4's `checkname` permits `/` in a NAME — `@acme/store` is # legal, and §10.2 resolves a scoped name verbatim — so splitting at @@ -3293,6 +3330,13 @@ primary: export: { in: [ { do: 'ready', ref: 'probe$a' }, { do: 'export', key: 'probe/client' } ] match: { out: { result: 'probe$a' } } } + # ...and the alias keys the same way the qualified form does, which + # is a second branch and so a second place to get it wrong. + { + id: 'export/alias#second-key' + in: [ { do: 'ready', ref: 'probe$a' }, { do: 'export', key: 'probe/mark' } ] + match: { out: { result: 'marked' } } + } # Two tagged and no untagged: ERROR, not last-wins. { id: 'export/alias#ambiguous' diff --git a/spec/plugin.json b/spec/plugin.json index eed9910..bc95b03 100644 --- a/spec/plugin.json +++ b/spec/plugin.json @@ -8074,6 +8074,24 @@ } } }, + { + "id": "export/alias#second-key", + "in": [ + { + "do": "ready", + "ref": "probe$a" + }, + { + "do": "export", + "key": "probe/mark" + } + ], + "match": { + "out": { + "result": "marked" + } + } + }, { "err": true, "id": "export/alias#ambiguous", @@ -8177,6 +8195,69 @@ } } }, + { + "doc": true, + "id": "export/key#second-key", + "in": [ + { + "do": "ready", + "ref": "probe$a" + }, + { + "do": "export", + "key": "probe$a/mark" + } + ], + "match": { + "out": { + "result": "marked" + } + } + }, + { + "id": "export/key#two-keys", + "in": [ + { + "do": "ready", + "ref": "probe$a" + }, + { + "do": "export", + "key": "probe$a/client" + }, + { + "do": "export", + "key": "probe$a/mark" + } + ], + "match": { + "out": { + "result": "marked" + } + } + }, + { + "id": "export/key#two-keys-reversed", + "in": [ + { + "do": "ready", + "ref": "probe$a" + }, + { + "do": "export", + "key": "probe$a/mark" + }, + { + "do": "export", + "key": "probe$a/client" + } + ], + "match": { + "out": { + "result": "probe$a" + } + } + }, { "doc": true, "id": "export/key#scoped", diff --git a/swift/test/Driver.swift b/swift/test/Driver.swift index 65aa9be..e54f6a5 100644 --- a/swift/test/Driver.swift +++ b/swift/test/Driver.swift @@ -113,6 +113,8 @@ enum Driver { return .str(wrap + (inner.asString ?? inner.json)) }, band) i.export("client", .str(i.ref)) + // A SECOND SCALAR KEY; see typescript/test/driver.ts. + i.export("mark", .str("marked")) // The instance api itself, so the driver's `stray` command can // call `release` from OUTSIDE a lifecycle callback. i.export("inst", .opaque(i)) diff --git a/typescript/test/driver.ts b/typescript/test/driver.ts index c114bf9..fae8e1a 100644 --- a/typescript/test/driver.ts +++ b/typescript/test/driver.ts @@ -31,6 +31,12 @@ export function probes(): Definition[] { i.bind('c', (next: any, v: any) => (i.options && i.options.wrap ? i.options.wrap : ':') + next(v), i.options && i.options.band) i.export('client', i.ref) + // A SECOND SCALAR KEY. Every `export` entry used to read + // `client`, so a port whose `exports` ignored the key and + // answered with the instance's first export passed all of them. + // `inst` below cannot close that: it is an instance api, shaped + // differently in every port, and no entry can assert on it. + i.export('mark', 'marked') // The instance api itself, so the driver's `stray` command can // call `release` from OUTSIDE a lifecycle callback — which is the // only way to exercise §8.3's scope guard, and which the command diff --git a/zig/test/driver.zig b/zig/test/driver.zig index e76d2d3..95fa27d 100644 --- a/zig/test/driver.zig +++ b/zig/test/driver.zig @@ -113,6 +113,8 @@ fn probeDefine(i: *Inst) t.Err!void { try host.bind(i, "p", probeHook, null, i, band); try host.bind(i, "c", null, probeChain, i, band); host.exportvalue(i, "client", v.vstr(i.ref)); + // A SECOND SCALAR KEY; see typescript/test/driver.ts. + host.exportvalue(i, "mark", v.vstr("marked")); // The instance api itself, so the driver's `stray` command can call // `release` from OUTSIDE a lifecycle callback — which is the only // way to exercise §8.3's scope guard. The driver looks the instance From 7172ccf9bf3783d35fdc277d24971e03b89dd392 Mon Sep 17 00:00:00 2001 From: Claude Date: Wed, 16 Sep 2026 11:19:02 +0000 Subject: [PATCH 7/9] =?UTF-8?q?depend:=20=C2=A711.1's=20`inst.capability(n?= =?UTF-8?q?ame)`,=20and=20what=20the=20corpus=20had=20to=20say?= MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit Register row 6.9, the last of the three gaps the export how-to found. §11.1 said "the first is bound, and `inst.capability(name)` returns it" and the instance api had no such method: `bind`, `export`, `provides`, `acquire`, `release`, `position`, `nest`, and no `capability`. Implemented rather than struck, because `host.capability` cannot answer it. That one RANKS the live providers; this one answers with the provider THIS instance took, and §11.4's reluctant rebinding makes the two different refs at the same instant. It reaches `chosen` with `remember` true — the instance is asking, not introspection about it — and answers with a ref, so the API still travels as an export. A corpus entry reaches it through the `dep` probe's new `options.capof`, which names one of the instance's own requirements and exports the answer as `cap`, from `activate` because that is when the selection is made. Nothing else can: an instance api is shaped differently in every port and no entry can assert on one. The first four entries did not earn the method, and mutating it is what said so. Against the selected one, rank deciding it, an optional requirement nobody provides and a name this instance does not require, `host.capability(name)[0]` — the exact thing the method exists to not be — passed all 584, and so did `requirements[0]`, which never reads the name. Six more entries close both. `#by-ref` turns on §11.1's "a ref satisfies too": a ref is not a declared capability, so the instance answers `dep$p` where the host ranks nothing, and `#by-ref-host-disagrees` is the same run asking the host. `#named-first` and `#named-second` needed an instance with TWO satisfied requirements, which no other entry here has. `#reluctant` and `#reluctant-host-ranks` record the divergence the design claims and nothing else stated. `remember` true rather than false stays unpinnable: activation's own remember-all loop runs immediately after the callback that asks. Canonical plus all 22 ports, `c` taking a forward declaration because `chosen` is defined below it. Corpus 584 -> 590, all 23 ports green. Design §11.1 and §11.3 now describe something that exists; DOCS.md §2 gains the consuming half of the export how-to and §4.3 documents `capof`. Co-Authored-By: Claude Opus 5 Claude-Session: https://claude.ai/code/session_01CVMgjjwQfTJ2rXz637Wpk8 --- AGENTS.md | 4 +- CLAUDE.md | 2 +- DOCS.md | 11 +- README.md | 4 +- c/src/host.c | 23 ++ c/src/host.h | 1 + c/test/driver.c | 14 + clojure/src/voxgig/plugin/host.clj | 15 + clojure/test/voxgig/plugin/driver.clj | 7 +- cpp/src/host.cpp | 19 + cpp/src/host.hpp | 1 + cpp/test/driver.cpp | 13 + csharp/src/Host.cs | 7 + csharp/src/Inst.cs | 19 + csharp/test/Driver.cs | 11 +- dart/lib/host.dart | 19 + dart/test/driver.dart | 10 +- doc/plan/progress.md | 2 +- doc/plan/status.md | 21 +- elixir/lib/voxgig_plugin/host.ex | 11 + elixir/lib/voxgig_plugin/inst.ex | 13 + elixir/test/driver.exs | 10 +- go/plugin/host.go | 24 ++ go/test/driver.go | 18 +- haskell/src/Host.hs | 15 + haskell/test/Driver.hs | 12 +- java/src/voxgig/plugin/Host.java | 2 +- java/src/voxgig/plugin/Inst.java | 19 + java/test/voxgig/plugin/test/Driver.java | 11 +- javascript/src/host.js | 15 + javascript/test/driver.js | 9 +- kotlin/src/Host.kt | 19 + kotlin/test/Driver.kt | 9 +- lean/src/Plugin/Defs.lean | 1 + lean/src/Plugin/Host.lean | 15 + lean/src/Plugin/Machine.lean | 1 + lean/test/Driver.lean | 16 +- lua/src/plugin/host.lua | 16 + lua/test/driver.lua | 9 +- ocaml/src/host.ml | 16 + ocaml/test/driver.ml | 16 +- perl/lib/Voxgig/Plugin/Host.pm | 17 + perl/test/Driver.pm | 10 +- php/src/Host.php | 24 ++ php/test/driver.php | 6 + python/test/driver.py | 10 +- python/voxgig_plugin/host.py | 16 + ruby/lib/voxgig_plugin/host.rb | 14 + ruby/test/driver.rb | 7 +- rust/src/host.rs | 22 ++ rust/tests/support/driver.rs | 12 + scala/src/Host.scala | 17 + scala/test/Driver.scala | 9 +- spec/plugin.aon | 150 ++++++++ spec/plugin.json | 428 +++++++++++++++++++++++ swift/src/Host.swift | 15 + swift/test/Driver.swift | 13 +- typescript/src/Host.ts | 26 ++ typescript/test/driver.ts | 17 +- zig/src/host.zig | 16 + zig/test/driver.zig | 14 + 61 files changed, 1293 insertions(+), 30 deletions(-) diff --git a/AGENTS.md b/AGENTS.md index 0cf42ba..442bd21 100644 --- a/AGENTS.md +++ b/AGENTS.md @@ -5,7 +5,7 @@ Read this before changing anything. The design is below (§n) are to it. **Status: P6 COMPLETE — six of six. Every planned port exists.** All -**19 corpus sections** exist — 572 entries — with the driver contract +**19 corpus sections** exist — 590 entries — with the driver contract in `DOCS.md` §4, and **twenty-three implementations pass every one of them**: `typescript/` (canonical), `go/`, `python/`, `javascript/`, `ruby/`, `php/`, `perl/`, `rust/`, `java/`, `lua/`, `csharp/`, `elixir/`, `clojure/`, @@ -283,7 +283,7 @@ decide, and `handover.md` §19 says what the six of them found. **All three corpus gaps §18 of the handover records are CLOSED** — gap 1 by `declare/shape` and `declare/register`, gap 2 by `depend/byref`, -gap 3 by `nest/open`. The corpus is 572 entries and every one of them +gap 3 by `nest/open`. The corpus is 590 entries and every one of them is mutation-checked against the behaviour it names. **Gap 1 was the expensive one, and §18's "cheap" was wrong about it.** Nothing carried a diff --git a/CLAUDE.md b/CLAUDE.md index 2df6da2..11abc9d 100644 --- a/CLAUDE.md +++ b/CLAUDE.md @@ -24,7 +24,7 @@ Quick reminders (the full rationale is in `AGENTS.md`): Two gates enforce it, `vale` and `python3 tools/check_prose.py`; `make scan-prose` runs both. -**Status: P6 COMPLETE — six of six.** The corpus is 572 entries across +**Status: P6 COMPLETE — six of six.** The corpus is 590 entries across 19 sections, and **twenty-three implementations pass every one of them** — `typescript/` (canonical), `go/`, `python/`, `javascript/`, `ruby/`, `php/`, `perl/`, `rust/`, `java/`, `lua/`, `csharp/`, `elixir/`, `clojure/`, diff --git a/DOCS.md b/DOCS.md index 7101144..5f336fc 100644 --- a/DOCS.md +++ b/DOCS.md @@ -243,6 +243,15 @@ a capability and exports nothing leaves its consumer with a name and nothing to call. Going the other way — an export with no capability declared — gets a reference the lifecycle knows nothing about. +On the consuming side, `inst.capability(name)` answers with the ref of +the provider THIS instance is bound to, for one of its own declared +requirements, or absent when nothing provides it — pair it with +`host.exports(ref + '/key')` to reach the API. It is a different +question from `host.capability(name)`, which ranks every live provider: +rebinding is reluctant (*Depend on something*, preceding), so an +instance keeps a provider that a newcomer outranks and the two answers +part company. + The worked example is [sekreto](https://github.com/voxgig/sekreto)'s mini vault, where each provider kind is a definition and the vault is the one that is written @@ -473,7 +482,7 @@ in the same way. | `probe` | The workhorse. Records every callback it receives into the log, binds one hook point (`p`), wraps one chain point (`c`), holds an integer counter in its state, and **acquires exactly one synthetic resource per activation**. It exports three keys: `client`, its own ref; `mark`, the constant `marked`; and `inst`, its own instance api, which is how the `stray` command reaches `release` from *outside* a lifecycle callback. **`mark` is there so an entry can read a SECOND key off one instance** — every `export` entry once read `client`, so a port whose `exports` ignored the key and answered with the instance's first export passed all of them, and `inst` cannot close that because no entry can assert on an instance api. | | `noisy` | Fails on demand. `options.fail` names the callback that raises — `define`, `activate`, `deactivate` or `close` — and `options.code` the error code. `options.bare` raises with **no code at all**, which is the ordinary library error §12's `plugin__failed` codes exist to wrap. Everything else is `probe`. | | `greedy` | Acquires `options.acquire` resources on activation and releases `options.release` of them explicitly, so the difference is what the instance scope must unwind (§8.3). `options.early` acquires in **`define`** instead, where §8.1 says capture does not belong. `options.bind` names the callback (`activate` or `deactivate`) that declares a **binding** outside `define`, which is §8.1's other half and §12's `plugin_bind_scope`. `options.mark` additionally registers that many **foreign** releases through `release`, each recording its own index into `state.unwound` as it runs — which is the only way the *direction* of the unwind is observable, since an acquired handle is an idempotent counter decrement that reads the same either way. `options.markfail` makes each of those releases **raise**, which is the only way §8.3's `plugin_release_failed` and its `failed` status are reachable. | -| `dep` | Declares requirements. `options.requires` is a list of refs or capability names, `options.optional` those that are optional rather than mandatory. | +| `dep` | Declares requirements. `options.requires` is a list of refs or capability names, `options.optional` those that are optional rather than mandatory. `options.capof` names one of them and exports the answer of `inst.capability` as `cap` — **the only way an entry can see the instance-side question at all**, since `host.capability` answers with the ranking rather than with the provider this instance took, and reluctant rebinding (§11.4) makes those differ. | | `provider` | Binds a provider point named by `options.point`, returning `options.value`. `options.version` and `options.priority` feed the selection rank. | | `slow` | Behaviourally `probe`, and **it does not yield.** It is here because §18 settles transitions eagerly — the host calls a callback and does not await it — and a callback that yields therefore does not "complete later", it silently abandons everything after its first suspension point. So the probe cannot demonstrate eager settling by yielding; it would only demonstrate that half a callback vanished. The name is kept, and the catalog keeps six definitions, because the question it was invented for is still open (see below). | diff --git a/README.md b/README.md index 5cf6fb6..a7fce2c 100644 --- a/README.md +++ b/README.md @@ -26,7 +26,7 @@ programmatic API over the same normalized model. **P6 complete — six of six. Every planned port exists.** The design is complete and agreed with its first host, the contract is complete (all -19 corpus sections, 572 entries), and there are **twenty-three +19 corpus sections, 590 entries), and there are **twenty-three implementations**: `typescript/` the canonical, plus `go/`, `python/`, `javascript/`, `ruby/`, `php/`, `perl/`, `rust/`, `java/`, `lua/`, `csharp/`, `elixir/`, `clojure/`, `dart/`, `kotlin/`, `swift/`, @@ -73,7 +73,7 @@ testing found, not about what was there. |---|---| | design | complete — [`docs/design/plugin.md`](./docs/design/plugin.md) | | agreement with station | [reconciled](https://github.com/voxgig/station/blob/main/docs/design/station-and-plugin.md), and [sequenced](https://github.com/voxgig/station/blob/main/docs/design/station-and-plugin-plan.md) | -| corpus | **572 entries across all 19 sections** — the contract is complete | +| corpus | **590 entries across all 19 sections** — the contract is complete | | driver contract | [`DOCS.md`](./DOCS.md) §4 | | ports | **twenty-three, all passing every section** — `typescript/` (canonical), `go/`, `python/`, `javascript/`, `ruby/`, `php/`, `perl/`, `rust/`, `java/`, `lua/`, `csharp/`, `elixir/`, `clojure/`, `dart/`, `kotlin/`, `swift/`, `scala/`, `c/`, `cpp/`, `ocaml/`, `haskell/`, `zig/` and `lean/`. **No port work remains.** Next: P3.1's extraction (unblocked: station's Stages 2–3b merged). | diff --git a/c/src/host.c b/c/src/host.c index ec969b9..0a7a0e2 100644 --- a/c/src/host.c +++ b/c/src/host.c @@ -418,6 +418,29 @@ void inst_export(Inst *e, const char *key, Value *value) { void inst_provides(Inst *e, Value *p) { vpush(e->provides, p); } +/* Defined with the rest of §11.4's selection, below; `inst_capability` + * is the one caller that comes before it. */ +static const char *chosen(Host *h, Inst *e, Value *req, bool remember); + +/* WHICH provider this instance is bound to for `name` (§11.1), as a ref, + * or NULL when nothing provides it. + * + * The host's own `capability` answers with the live providers RANKED, + * not with the one THIS instance took; §11.4's reluctant rebinding makes + * those differ. A REF, not the instance. The selection is REMEMBERED, + * because this is the instance asking. */ +const char *inst_capability(Inst *e, const char *name) { + Value *reqs = requirements(e->options); + for (size_t i = 0; i < vlen(reqs); i++) { + Value *r = vat(reqs, i); + const char *rn = vasstr(vget(r, "name")); + if (NULL != rn && 0 == strcmp(rn, name)) { + return chosen(inst_host(e), e, r, true); + } + } + return NULL; +} + /* The scope entry carries the inner host as its context — C's stand-in * for the closure every other port writes here. */ static void closeinner(void *ctx) { host_close((Host *)ctx); } diff --git a/c/src/host.h b/c/src/host.h index a45980b..497f537 100644 --- a/c/src/host.h +++ b/c/src/host.h @@ -113,6 +113,7 @@ void inst_bind(Inst *i, const char *point, HookFn hook, ChainFn chain, void *ctx, Value *band); void inst_export(Inst *i, const char *key, Value *value); void inst_provides(Inst *i, Value *p); +const char *inst_capability(Inst *i, const char *name); /* Returns a handle a plugin can hand back early. The scope still holds * the entry and unwinding it twice is a no-op — releasing early must * not make teardown wrong. */ diff --git a/c/test/driver.c b/c/test/driver.c index fcf429f..66f09d7 100644 --- a/c/test/driver.c +++ b/c/test/driver.c @@ -236,6 +236,19 @@ static void dep_define(Inst *i) { } } +/* WHICH provider this instance took, when the entry asks. See + * typescript/test/driver.ts. + * + * `dep` has no `acquire` in this port and gains none here: the entries + * that read `cap` assert `result`, never `open`, so adding one would + * change what every other `dep` entry sees for nothing. */ +static void dep_activate(Inst *i) { + Value *capof = opt(i, "capof"); + if (!visstr(capof)) return; + const char *picked = inst_capability(i, vasstr(capof)); + inst_export(i, "cap", NULL == picked ? vnull() : vstr(picked)); +} + static void provider_define(Inst *i) { Value *st = inst_state(i); vset(st, "count", vnum(0)); @@ -287,6 +300,7 @@ static Definition *probedef(const char *name) { } else if (0 == strcmp(name, "dep")) { d->define = dep_define; + d->activate = dep_activate; } else if (0 == strcmp(name, "provider")) { d->define = provider_define; diff --git a/clojure/src/voxgig/plugin/host.clj b/clojure/src/voxgig/plugin/host.clj index 7899ea4..be7f48a 100644 --- a/clojure/src/voxgig/plugin/host.clj +++ b/clojure/src/voxgig/plugin/host.clj @@ -270,6 +270,21 @@ (entry-update! (.host i) (.ref i) #(assoc-in % ["exports" k] v)) nil) +(defn inst-capability + "WHICH provider this instance is bound to for `nm` (section 11.1), as a + ref, or nil when nothing provides it. + + The host's own `capability` answers with the live providers RANKED, not + with the one THIS instance took; section 11.4's reluctant rebinding + makes those differ. A REF, not the instance. The selection is + REMEMBERED, because this is the instance asking." + [^Instance i nm] + (let [h (.host i) + ref (.ref i) + req (first (filter #(= nm (t/get % "name")) + (dep/requirements (field h ref "options"))))] + (when (some? req) (chosen h ref req true)))) + (defn provides! "What this instance can do for others (section 11.1)." [^Instance i prov] diff --git a/clojure/test/voxgig/plugin/driver.clj b/clojure/test/voxgig/plugin/driver.clj index 525262a..716f3ee 100644 --- a/clojure/test/voxgig/plugin/driver.clj +++ b/clojure/test/voxgig/plugin/driver.clj @@ -159,7 +159,12 @@ (declare-provides i) (let [exports (or (opt i "exports") {})] (doseq [k (t/sorted-keys exports)] (h/export! i k (t/get exports k))))) - "activate" (fn [i] (h/acquire! i))}) + "activate" (fn [i] + (h/acquire! i) + ;; WHICH provider this instance took, when the entry asks. + ;; See typescript/test/driver.ts. + (when-let [capof (opt i "capof")] + (h/export! i "cap" (h/inst-capability i capof))))}) (defn- provider [] {"name" "provider" diff --git a/cpp/src/host.cpp b/cpp/src/host.cpp index f1c389e..32e309a 100644 --- a/cpp/src/host.cpp +++ b/cpp/src/host.cpp @@ -255,6 +255,25 @@ void Inst::exportvalue(const std::string& key, const V& value) { void Inst::provides(const V& p) { push(provides_, p); } +/* WHICH provider this instance is bound to for `name` (§11.1), as a + * ref, or null when nothing provides it. + * + * The host's own `capability` answers with the live providers RANKED, + * not with the one THIS instance took; §11.4's reluctant rebinding + * makes those differ. A REF, not the instance. The selection is + * REMEMBERED, because this is the instance asking. */ +V Inst::capability(const std::string& name) const { + V reqs = requirements(options_); + for (size_t i = 0; i < len(reqs); i++) { + V r = at(reqs, i); + V rn = get(r, "name"); + if (!isstr(rn) || asstr(rn) != name) continue; + const std::string picked = owner_->chosen(owner_->find(ref_), r, true); + return picked.empty() ? vnull() : vstr(picked); + } + return vnull(); +} + HostPtr Inst::nest(const HostOptions& opts) { if (!owner_->intransition_) { fail("plugin_release_scope", "nest called outside a lifecycle callback"); diff --git a/cpp/src/host.hpp b/cpp/src/host.hpp index e114132..606ea55 100644 --- a/cpp/src/host.hpp +++ b/cpp/src/host.hpp @@ -96,6 +96,7 @@ class Inst { void bindchain(const std::string& point, ChainFn chain, const V& band); void exportvalue(const std::string& key, const V& value); void provides(const V& p); + V capability(const std::string& name) const; /* Returns a handle a plugin can hand back early. The scope still * holds the entry and unwinding it twice is a no-op — releasing early * must not make teardown wrong. */ diff --git a/cpp/test/driver.cpp b/cpp/test/driver.cpp index 9539543..3acd5fc 100644 --- a/cpp/test/driver.cpp +++ b/cpp/test/driver.cpp @@ -185,6 +185,18 @@ static void depdefine(Inst& i) { } } +/* WHICH provider this instance took, when the entry asks. See + * typescript/test/driver.ts. + * + * `dep` has no `acquire` in this port and gains none here: the entries + * that read `cap` assert `result`, never `open`, so adding one would + * change what every other `dep` entry sees for nothing. */ +static void depactivate(Inst& i) { + V capof = opt(i, "capof"); + if (!isstr(capof)) return; + i.exportvalue("cap", i.capability(asstr(capof))); +} + static void providerdefine(Inst& i) { set(i.state(), "count", vnum(0)); Inst* self = &i; @@ -236,6 +248,7 @@ static DefinitionPtr probedef(const std::string& name) { } else if ("dep" == name) { d->define = depdefine; + d->activate = depactivate; } else if ("provider" == name) { d->define = providerdefine; diff --git a/csharp/src/Host.cs b/csharp/src/Host.cs index fd17607..778ad1e 100644 --- a/csharp/src/Host.cs +++ b/csharp/src/Host.cs @@ -646,6 +646,13 @@ private List UnmetOf(Entry entry) /// ABOUT an instance rather than BY it: introspection must not /// create a binding. /// + /// The instance api's way onto Chosen, which is + /// private. + internal string InstCapability(Entry entry, object req) + { + return Chosen(entry, req, true); + } + private string Chosen(Entry entry, object req, bool remember) { var cands = ProvidersOf(req); diff --git a/csharp/src/Inst.cs b/csharp/src/Inst.cs index 1c4e960..98bb68d 100644 --- a/csharp/src/Inst.cs +++ b/csharp/src/Inst.cs @@ -137,6 +137,25 @@ public void Export(string key, object value) } /// What this instance can do for others (§11.1). + /// WHICH provider this instance is bound to for + /// name (§11.1), as a ref, or null when nothing provides + /// it. The host's own Capability answers with the live providers + /// RANKED, not with the one THIS instance took; §11.4's + /// reluctant rebinding makes those differ. A REF, not the + /// instance. The selection is REMEMBERED, because this is the + /// instance asking. + public string Capability(string name) + { + foreach (var req in Depend.Requirements(entry.Options)) + { + if (name == Types.Str(Types.Get(req, "name"))) + { + return HostRef.InstCapability(entry, req); + } + } + return null; + } + public void Provides(object prov) { entry.Provides.Add(prov); diff --git a/csharp/test/Driver.cs b/csharp/test/Driver.cs index 4166abe..f59b19b 100644 --- a/csharp/test/Driver.cs +++ b/csharp/test/Driver.cs @@ -213,7 +213,16 @@ public static List Probes() i.Export(k, Types.Get(exports, k)); } }; - dep.Activate = i => i.Acquire(); + dep.Activate = i => + { + i.Acquire(); + // WHICH provider this instance took, when the entry asks. See typescript/test/driver.ts. + var capof = Types.Get(i.Options(), "capof") as string; + if (null != capof) + { + i.Export("cap", i.Capability(capof)); + } + }; out_.Add(dep); var provider = new Definition("provider"); diff --git a/dart/lib/host.dart b/dart/lib/host.dart index 4dec745..30724d0 100644 --- a/dart/lib/host.dart +++ b/dart/lib/host.dart @@ -146,6 +146,22 @@ class Inst { void export(String key, dynamic value) => _entry.exports[key] = value; /// What this instance can do for others (section 11.1). + /// WHICH provider this instance is bound to for [name] (§11.1), as a + /// ref, or null when nothing provides it. + /// + /// The host's own `capability` answers with the live providers RANKED, + /// not with the one THIS instance took; §11.4's reluctant rebinding + /// makes those differ. A REF, not the instance. The selection is + /// REMEMBERED, because this is the instance asking. + String? capability(String name) { + for (final req in dep.requirements(_entry.options)) { + if (name == req['name']) { + return host.instcapability(_entry, req); + } + } + return null; + } + void provides(dynamic prov) => _entry.provides.add(prov); /// Where this binding landed (section 6.6) - the plugin-side counterpart @@ -582,6 +598,9 @@ class Host { /// /// `remember` is false for the questions asked ABOUT an instance rather /// than BY it: introspection must not create a binding. + /// The instance api's way onto [_chosen], which is private. + String? instcapability(Entry entry, dynamic req) => _chosen(entry, req, true); + String? _chosen(Entry entry, dynamic req, bool remember) { final cands = _providersOf(req); if (cands.isEmpty) return null; diff --git a/dart/test/driver.dart b/dart/test/driver.dart index da293c5..bc1bb6c 100644 --- a/dart/test/driver.dart +++ b/dart/test/driver.dart @@ -199,7 +199,15 @@ List probes() { i.export(k, p.get(exports, k)); } }, - 'activate': (p.Inst i) => i.acquire(), + 'activate': (p.Inst i) { + i.acquire(); + // WHICH provider this instance took, when the entry asks. See + // typescript/test/driver.ts. + final capof = _opt(i, 'capof'); + if (capof is String) { + i.export('cap', i.capability(capof)); + } + }, }; final provider = { diff --git a/doc/plan/progress.md b/doc/plan/progress.md index c9131b7..95f2a8d 100644 --- a/doc/plan/progress.md +++ b/doc/plan/progress.md @@ -96,5 +96,5 @@ It did: see 4.1's note and [`handover.md`](handover.md) §13. | 6.3 Corpus gap 1: shape validation at REGISTRATION | **DONE** | `declare/shape` (7 entries) pins §10.1's TIMING, which `config/optmergebad` says in its own comment it cannot: every entry stops at `define`, so a port deferring the check to resolution raises nothing and fails. Two entries also pin that a valid shape is KEPT rather than validated and dropped, one that a rejected registration leaves nothing behind. **The gap was not cheap and §18's "cheap" was wrong about it**: nothing carried a `shape` because the driver's `define` was a NO-OP in all seventeen ports — a documented three-key verb (DOCS.md §4.2) that registered nothing — so `catalog.add`'s check was unreachable by construction and the `probe` key was ignored by the ten entries passing it. `define` is now implemented everywhere, all three keys live, and `declare/register` (3 entries) pins `probe` distinct from `name`. DOCS.md's "default is `probe`" was wrong and is corrected to `name`; the literal default would have re-backed every `dep`, `noisy` and `greedy` definition with the wrong probe. **Implementing it found a canonical bug**: `apply` handed its resolved options map to `declare`, which ADOPTS it, then refilled that map from itself — so a first-time `apply` left the instance with **no options at all**, and only a second identical apply filled them in. Every `apply` entry asserted status, log or open and none a value the options decide. Fixed in canonical, go, javascript, python, ruby, perl, lua, dart; php, java, csharp, kotlin, rust, swift, scala, elixir, clojure never had it. Three new `apply/idempotent` entries pin it. Corpus 539 -> 552; `make check` green in all seventeen. | | 6.7 Corpus gap 4: a second export key off ONE instance | **DONE** | `probe` now exports `mark`, the constant `marked`, beside `client` and `inst`; four entries read a second key (`export/key#second-key`, `#two-keys`, `#two-keys-reversed`, `export/alias#second-key`). **The gap as first written was overstated, and measuring it is what said so.** A port that IGNORED the key outright was already caught, by the absent-key entry `probe$a/nope`: ignoring the key makes a missing key present. What nothing could distinguish is a lookup that CHECKS the key is present and then answers with the instance's FIRST export — presence-checked, position-answered. Mutated both branches that way and measured: against the 572-entry corpus the exact branch left `export/key` and `export/alias` green (only `featurehost-bridge` and `resource/scope` failed, and both only because the DRIVER reads `exports(ref + '/inst')` for `stray`, which is not an entry asserting anything); the alias branch left the WHOLE suite green, 0 failures. Against 580 each is caught by its own group and nothing else. So a port could have got exports wrong and been told by a resource test, or not told at all. `inst` cannot close this — it is an instance api, shaped differently in every port, and no entry can assert on it; a constant can. 23 drivers, DOCS.md §4.3. Corpus 576 -> 580; all 23 ports green. | | 6.8 A scoped definition has no export spelling | **DONE** | Found by Codex's review of the DOCS.md how-to, and reproduced against the canonical. `resolveexport` splits an export spec at the FIRST `/`, so `@acme/store/admin` reads as the ref `@acme` with the key `store/admin` and answers `undefined`. §4's `checkname` permits `/` in a NAME, and `resolvecandidates` has a branch for scoped names resolving verbatim, so scoped definitions are a supported case with no way to read their exports. Nothing in `export` covers it: every entry there uses `probe`, which has no slash. **Closed by the last-`/` split**, canonical plus all 22 ports, and four `export/key` entries (`#scoped`, `#scoped-untagged`, `#scoped-alias`, and a scoped miss). The cost is stated in design §11 and DOCS.md: an export key may not contain `/`, because one separator cannot serve both and a name holds slashes because §4 says so. Four ports had no reverse search and take a documented workaround — lua walks forward keeping the last hit, elixir takes `List.last(:binary.matches ...)`, haskell and lean split the REVERSED string and put the halves back. Reverting the canonical to `indexOf` fails `export/key` and nothing else. Corpus 572 -> 576; all 23 ports green. | -| 6.9 §11.1's `inst.capability(name)` does not exist | OPEN | Also from that review. The design says "the first is bound, and `inst.capability(name)` returns it", and the canonical instance api has no such method — `bind`, `export`, `provides`, `acquire`, `release`, `position`, `nest`, and no `capability`. What exists is `host.capability(name)`, which returns provider REFS. So a capability carries selection metadata and a lifecycle edge, and no callable value: a consumer reaches the provider's API through an export or an extension point. That is a design statement no corpus entry can distinguish, which is handover.md §13's first kind exactly. Either implement `inst.capability` or correct §11.1; the how-to documents the behaviour as it is meanwhile. | +| 6.9 §11.1's `inst.capability(name)` does not exist | **DONE** | Also from that review. The design said "the first is bound, and `inst.capability(name)` returns it", and the canonical instance api had no such method — `bind`, `export`, `provides`, `acquire`, `release`, `position`, `nest`, and no `capability`. **Implemented rather than struck**, because the question it asks is one the host cannot answer: `host.capability(name)` RANKS the live providers, and §11.4's reluctant rebinding means the instance keeps a provider a newcomer outranks, so the two answers part company exactly when it matters. It reaches `chosen` with `remember` TRUE — this is the instance asking, not introspection about it — and answers with a REF, so the API still travels as an export. Visible to the corpus only through the `dep` probe's new `options.capof`, which exports the answer as `cap`; without it no entry could reach an instance api. **The first four entries did not earn the method, and mutating it is what said so.** The selected one, rank deciding it, an optional requirement nobody provides, and a name this instance does not require: against those four, `host.capability(name)[0]` — the shortest wrong implementation there is, and the exact thing the method exists to not be — passed the whole 584-entry suite, and so did `requirements[0]`, which never reads the name. Both are now caught. `#by-ref` closes the first: §11.1 says a ref satisfies a requirement, and a ref is not a declared capability, so the instance answers `dep$p` where the host ranks nothing at all — `#by-ref-host-disagrees` is the same run asking the host. `#named-second` and `#named-first` close the second, and needed an instance with TWO satisfied requirements, which no other entry here has. `#reluctant` and `#reluctant-host-ranks` record §11.4 seen from outside — `dep$c` keeps `dep$lo` while the host ranks the newcomer `dep$hi` first — which is the divergence the design claims and nothing else in the corpus states. One thing stays unpinnable: `remember` true rather than false is invisible, because activation's own remember-all loop runs immediately after the callback that asks. Canonical plus all 22 ports, DOCS.md §2 and §4.3. Corpus 580 -> 590; all 23 ports green. | | 6.2 Does sdkgen adopt plugin? (§17.2) | DECISION NEEDED | Open, uncommitted, and carries a propagation cost across 23 template trees. Gates nested hosts *natively*, deletion of `transport`, and the seventeen-model change. | diff --git a/doc/plan/status.md b/doc/plan/status.md index df42c08..b48d501 100644 --- a/doc/plan/status.md +++ b/doc/plan/status.md @@ -15,7 +15,7 @@ a wrong status file is worse than none.** **Nothing. P6 is complete — six of six — and no port work remains on the plan.** `c`, `cpp`, `ocaml`, `haskell`, `zig` and `lean` all landed, -so **twenty-three implementations pass all 572 corpus entries** and +so **twenty-three implementations pass all 590 corpus entries** and `make check` runs every one of them. **The six tier-4 ports are deliberately not one port six times**, and @@ -223,9 +223,22 @@ table is the summary, that file is the authority. Neither blocks P1. `/`, so a scoped definition name (`@acme/store`, which §4 permits and `resolvecandidates` handles) has no spelling for its exports. Row **6.9**: §11.1 says `inst.capability(name)` returns the bound provider - and the canonical instance api has no such method, so a capability - carries no callable value. And row **6.7**: no `export` entry read a - SECOND key off one instance. **All three are now closed**, and 6.7's + and the canonical instance api had no such method. And row **6.7**: no + `export` entry read a SECOND key off one instance. **All three are now + closed.** 6.9 was implemented rather than struck, because the host + cannot answer the question it asks: `host.capability` ranks the live + providers, and reluctant rebinding (§11.4) means an instance keeps a + provider a newcomer outranks. It answers with a REF, so a capability + still carries no callable value and the API still travels as an + export. + +- **Both of those were measured, and both measurements corrected the + entry that prompted them.** Mutation is the only way to find out + whether an addition is pinned, and twice now the first draft of a + group was not. 6.9's first four entries left `host.capability(name)[0]` + — the exact thing `inst.capability` exists to not be — passing the + whole suite, and a lookup that never reads the name passing it too; + the six entries that close them are in the register. And 6.7's first description was overstated: a port that ignored the key outright was already caught by the absent-key entry, because ignoring the key makes a missing key present. What nothing could distinguish is a lookup diff --git a/elixir/lib/voxgig_plugin/host.ex b/elixir/lib/voxgig_plugin/host.ex index 24da982..373d66b 100644 --- a/elixir/lib/voxgig_plugin/host.ex +++ b/elixir/lib/voxgig_plugin/host.ex @@ -638,6 +638,17 @@ defmodule Voxgig.Plugin.Host do # # `remember` is false for the questions asked ABOUT an instance rather # than BY it: introspection must not create a binding. + @doc false + # The instance api's way onto `chosen`, which is private. + def instcapability(host, ref, name) do + Depend.requirements(field(host, ref, "options")) + |> Enum.find(fn req -> Types.get(req, "name") == name end) + |> case do + nil -> nil + req -> chosen(host, ref, req, true) + end + end + defp chosen(host, ref, req, remember) do cands = providersof(host, req) name = Types.get(req, "name") diff --git a/elixir/lib/voxgig_plugin/inst.ex b/elixir/lib/voxgig_plugin/inst.ex index 8ec2a36..3103778 100644 --- a/elixir/lib/voxgig_plugin/inst.ex +++ b/elixir/lib/voxgig_plugin/inst.ex @@ -102,6 +102,19 @@ defmodule Voxgig.Plugin.Inst do Host.entry_update(host, ref, &Map.put(&1, "exports", Map.put(&1["exports"], key, value))) end + @doc """ + WHICH provider this instance is bound to for `name` (section 11.1), as + a ref, or nil when nothing provides it. + + The host's own `capability` answers with the live providers RANKED, not + with the one THIS instance took; section 11.4's reluctant rebinding + makes those differ. A REF, not the instance. The selection is + REMEMBERED, because this is the instance asking. + """ + def capability(%__MODULE__{host: host, ref: ref}, name) do + Host.instcapability(host, ref, name) + end + @doc "What this instance can do for others (section 11.1)." def provides(%__MODULE__{host: host, ref: ref}, prov) do Host.entry_update(host, ref, &Map.put(&1, "provides", &1["provides"] ++ [prov])) diff --git a/elixir/test/driver.exs b/elixir/test/driver.exs index acfb4e8..200d1d4 100644 --- a/elixir/test/driver.exs +++ b/elixir/test/driver.exs @@ -160,7 +160,15 @@ defmodule Driver do exports = opt(i, "exports") || %{} Enum.each(Types.keys(exports), &Inst.export(i, &1, Types.get(exports, &1))) end, - "activate" => fn i -> Inst.acquire(i) end} + "activate" => fn i -> + Inst.acquire(i) + # WHICH provider this instance took, when the entry asks. See + # typescript/test/driver.ts. + case opt(i, "capof") do + nil -> :ok + capof -> Inst.export(i, "cap", Inst.capability(i, capof)) + end + end} end defp provider do diff --git a/go/plugin/host.go b/go/plugin/host.go index f6a108f..24e2421 100644 --- a/go/plugin/host.go +++ b/go/plugin/host.go @@ -390,6 +390,30 @@ func (i *Inst) Export(key string, value any) { i.e.exports[key] = value } // Provides declares what this instance can do for others (§11.1). func (i *Inst) Provides(p Provided) { i.e.provides = append(i.e.provides, p) } +// Capability is WHICH provider this instance is bound to for name +// (§11.1), as a ref, or "" when nothing provides it. +// +// §11.1 says "the first is bound, and inst.capability(name) returns it", +// and §11.3 gives the case that needs it: a plugin that works without +// metrics and uses metrics when it is there has to be able to ask. +// Host.Capability answers with the live providers RANKED -- not with the +// one THIS instance took, and §11.4's reluctant rebinding makes those +// differ: a better-ranked newcomer tops the ranking while the consumer +// keeps what it had. +// +// A REF, not the instance: every port can return a string and a corpus +// entry can assert on one. The selection is REMEMBERED, because this is +// the instance asking; `remember` is false only for questions asked +// ABOUT an instance, where answering must not create a binding. +func (i *Inst) Capability(name string) string { + for _, req := range Requirements(i.e.Options) { + if req.Name == name { + return i.h.chosen(i.e, req, true) + } + } + return "" +} + type Position struct { Index int `json:"index"` Count int `json:"count"` diff --git a/go/test/driver.go b/go/test/driver.go index e68f725..851fd15 100644 --- a/go/test/driver.go +++ b/go/test/driver.go @@ -229,7 +229,23 @@ func Probes() []plugin.Definition { } return nil }, - Activate: func(i *plugin.Inst) error { _, err := i.Acquire(); return err }, + Activate: func(i *plugin.Inst) error { + if _, err := i.Acquire(); nil != err { + return err + } + // WHICH provider this instance took, when the entry asks. + // See typescript/test/driver.ts: the host's own Capability + // answers with the RANKING, not with this instance's choice. + // "" is absent, and the corpus asserts absent as null. + if name, ok := i.Options()["capof"].(string); ok { + if ref := i.Capability(name); "" == ref { + i.Export("cap", nil) + } else { + i.Export("cap", ref) + } + } + return nil + }, } provider := plugin.Definition{ diff --git a/haskell/src/Host.hs b/haskell/src/Host.hs index 6660214..cd9ffe4 100644 --- a/haskell/src/Host.hs +++ b/haskell/src/Host.hs @@ -389,6 +389,21 @@ chosen h e req remember = do when remember $ modifyIORef' (iSelected e) (\m -> vset m name (VStr first)) return (Just first) +-- | WHICH provider this instance is bound to for @name@ (§11.1), as a +-- ref, or 'Nothing' when nothing provides it. +-- +-- The host's own @capability@ answers with the live providers RANKED, +-- not with the one THIS instance took; §11.4's reluctant rebinding +-- makes those differ. A REF, not the instance. The selection is +-- REMEMBERED, because this is the instance asking. +instCapability :: Inst -> String -> IO (Maybe String) +instCapability e name = do + opts <- readIORef (iOptions e) + let match r = isStr (vget r "name") && asStr (vget r "name") == name + case filter match (vitems (requirements opts)) of + [] -> return Nothing + (req : _) -> chosen (iOwner e) e req True + -- | The instance currently SELECTED for each of this one's -- restart-causing requirements. A BINDING IS TO AN INSTANCE, not to a -- capability (§11.1): the selected one going away restarts a @static@ diff --git a/haskell/test/Driver.hs b/haskell/test/Driver.hs index d204aec..0c42d5d 100644 --- a/haskell/test/Driver.hs +++ b/haskell/test/Driver.hs @@ -203,6 +203,16 @@ depDefine i = do exports <- opt i "exports" when (isMap exports) $ forM_ (vkeys exports) $ \k -> instExport i k (vget exports k) +-- | WHICH provider this instance took, when the entry asks. See +-- typescript/test/driver.ts. +depActivate :: Inst -> IO () +depActivate i = do + _ <- instAcquire i + capof <- opt i "capof" + when (isStr capof) $ do + picked <- instCapability i (asStr capof) + instExport i "cap" (maybe VNull VStr picked) + providerDefine :: Inst -> IO () providerDefine i = do modifyIORef' (iState i) (\st -> vset st "count" (VNum 0)) @@ -240,7 +250,7 @@ probeDef name = case name of , dActivate = Just (\i -> greedyCapture i >> greedyBindAt i "activate") , dDeactivate = Just (`greedyBindAt` "deactivate") } - "dep" -> base {dDefine = Just depDefine} + "dep" -> base {dDefine = Just depDefine, dActivate = Just depActivate} "provider" -> base {dDefine = Just providerDefine} _ -> base where diff --git a/java/src/voxgig/plugin/Host.java b/java/src/voxgig/plugin/Host.java index 5f8b829..a8d404f 100644 --- a/java/src/voxgig/plugin/Host.java +++ b/java/src/voxgig/plugin/Host.java @@ -566,7 +566,7 @@ private List unmetof(Entry entry) { *

{@code remember} is false for the questions asked ABOUT an instance * rather than BY it: introspection must not create a binding. */ - private String chosen(Entry entry, Object req, boolean remember) { + String chosen(Entry entry, Object req, boolean remember) { List cands = providersof(req); if (cands.isEmpty()) { return null; diff --git a/java/src/voxgig/plugin/Inst.java b/java/src/voxgig/plugin/Inst.java index 8087285..1be0ea7 100644 --- a/java/src/voxgig/plugin/Inst.java +++ b/java/src/voxgig/plugin/Inst.java @@ -137,6 +137,25 @@ public void export(String key, Object value) { entry.exports.put(key, value); } + /** + * WHICH provider this instance is bound to for {@code name} (§11.1), as + * a ref, or null when nothing provides it. + * + *

The host's own {@code capability} answers with the live providers + * RANKED, not with the one THIS instance took; §11.4's reluctant + * rebinding makes those differ. A REF, not the instance: every port can + * return a string and a corpus entry can assert on one. The selection + * is REMEMBERED, because this is the instance asking. + */ + public String capability(String name) { + for (Object req : Depend.requirements(entry.options)) { + if (name.equals(Types.get(req, "name"))) { + return host.chosen(entry, req, true); + } + } + return null; + } + /** What this instance can do for others (§11.1). */ public void provides(Object prov) { entry.provides.add(prov); diff --git a/java/test/voxgig/plugin/test/Driver.java b/java/test/voxgig/plugin/test/Driver.java index f6839f3..05231b1 100644 --- a/java/test/voxgig/plugin/test/Driver.java +++ b/java/test/voxgig/plugin/test/Driver.java @@ -209,7 +209,16 @@ public static List probes() { i.export(k, Types.get(exports, k)); } }; - dep.activate = i -> i.acquire(); + dep.activate = + i -> { + i.acquire(); + // WHICH provider this instance took, when the entry asks. See + // typescript/test/driver.ts. + Object capof = Types.get(i.options(), "capof"); + if (capof instanceof String) { + i.export("cap", i.capability((String) capof)); + } + }; out.add(dep); Definition provider = new Definition("provider"); diff --git a/javascript/src/host.js b/javascript/src/host.js index 03a5d09..0412bc2 100644 --- a/javascript/src/host.js +++ b/javascript/src/host.js @@ -191,6 +191,21 @@ function makehost(options) { /** Published for other plugins and for the application (§11). */ export: (key, value) => { e.exports[key] = value }, + /** WHICH provider this instance is bound to for `name` (§11.1), + * as a ref, or undefined when nothing provides it. + * + * The host's own `capability` answers with the live providers + * RANKED, not with the one THIS instance took; §11.4's reluctant + * rebinding makes those differ. A REF, not the instance: every + * port can return a string and a corpus entry can assert on one. + * The selection is REMEMBERED, because this is the instance + * asking. */ + capability: (name) => { + const req = requirements(e.options).find((r) => r.name === name) + if (undefined === req) return undefined + return chosen(e, req, true) + }, + /** What this instance can do for others (§11.1). */ provides: (p) => { e.provides.push(p) }, diff --git a/javascript/test/driver.js b/javascript/test/driver.js index 4b5f0a9..f17fd4a 100644 --- a/javascript/test/driver.js +++ b/javascript/test/driver.js @@ -132,7 +132,14 @@ function probes() { for (const k of Object.keys(i.options.exports)) i.export(k, i.options.exports[k]) } }, - activate: (i) => { i.acquire() }, + activate: (i) => { + i.acquire() + // WHICH provider this instance took, when the entry asks. See + // typescript/test/driver.ts. + if (i.options && i.options.capof) { + i.export('cap', i.capability(i.options.capof)) + } + }, } const provider = { diff --git a/kotlin/src/Host.kt b/kotlin/src/Host.kt index b431b14..273954d 100644 --- a/kotlin/src/Host.kt +++ b/kotlin/src/Host.kt @@ -146,6 +146,22 @@ class Inst(val host: Host, private val entry: Entry) { } /** What this instance can do for others (section 11.1). */ + /** WHICH provider this instance is bound to for [name] (§11.1), as a + * ref, or null when nothing provides it. + * + * The host's own `capability` answers with the live providers + * RANKED, not with the one THIS instance took; §11.4's reluctant + * rebinding makes those differ. A REF, not the instance. The + * selection is REMEMBERED, because this is the instance asking. */ + fun capability(name: String): String? { + for (req in Depend.requirements(entry.options)) { + if (name == Types.get(req, "name")) { + return host.instcapability(entry, req) + } + } + return null + } + fun provides(prov: Any?) { entry.provides.add(prov) } @@ -622,6 +638,9 @@ class Host @JvmOverloads constructor(options: Any? = null) { * `remember` is false for the questions asked ABOUT an instance rather than * BY it: introspection must not create a binding. */ + /** The instance api's way onto [chosen], which is private. */ + internal fun instcapability(entry: Entry, req: Any?): String? = chosen(entry, req, true) + private fun chosen(entry: Entry, req: Any?, remember: Boolean): String? { val cands = providersOf(req) if (cands.isEmpty()) return null diff --git a/kotlin/test/Driver.kt b/kotlin/test/Driver.kt index 16c1500..9a12174 100644 --- a/kotlin/test/Driver.kt +++ b/kotlin/test/Driver.kt @@ -214,7 +214,14 @@ object Driver { val exports = opt(i, "exports") for (k in Types.keys(exports)) i.export(k, Types.get(exports, k)) }, - "activate" to { i: Inst -> i.acquire() } + "activate" to { i: Inst -> + i.acquire() + // WHICH provider this instance took, when the entry asks. See typescript/test/driver.ts. + val capof = Types.get(i.options, "capof") as? String + if (null != capof) { + i.export("cap", i.capability(capof)) + } + } ) val provider = mapOf( diff --git a/lean/src/Plugin/Defs.lean b/lean/src/Plugin/Defs.lean index aef08c2..faaf1ed 100644 --- a/lean/src/Plugin/Defs.lean +++ b/lean/src/Plugin/Defs.lean @@ -68,6 +68,7 @@ structure InstApi where bindChain : String → ((Value → PluginM Value) → Value → PluginM Value) → Value → PluginM Unit exportValue : String → Value → PluginM Unit provides : Value → PluginM Unit + capability : String → PluginM (Option String) /-- Answers a handle a plugin can hand back early. The scope still holds the entry and unwinding it twice is a no-op — releasing early must not make teardown wrong. -/ diff --git a/lean/src/Plugin/Host.lean b/lean/src/Plugin/Host.lean index 1487f69..ad39ad8 100644 --- a/lean/src/Plugin/Host.lean +++ b/lean/src/Plugin/Host.lean @@ -232,6 +232,21 @@ def chosen (h : HostState) (e : InstState) (req : Value) (remember : Bool) if remember then e.selected.set ((← e.selected.get).set name (.str first)) return some first +/-- WHICH provider this instance is bound to for `name` (§11.1), as a +ref, or `none` when nothing provides it. + +The host's own `capability` answers with the live providers RANKED, not +with the one THIS instance took; §11.4's reluctant rebinding makes those +differ. A REF, not the instance. The selection is REMEMBERED, because +this is the instance asking. -/ +def instCapability (h : HostState) (e : InstState) (name : String) + : PluginM (Option String) := do + for r in (requirements (← e.options.get)).items do + let rn := r.get "name" + if !rn.isStr || rn.asStr != name then continue + return ← chosen h e r true + return none + /-- The instance currently SELECTED for each of this one's restart-causing requirements. A BINDING IS TO AN INSTANCE, not to a capability (§11.1): the selected one going away restarts a `static` diff --git a/lean/src/Plugin/Machine.lean b/lean/src/Plugin/Machine.lean index ec56e8e..602062e 100644 --- a/lean/src/Plugin/Machine.lean +++ b/lean/src/Plugin/Machine.lean @@ -94,6 +94,7 @@ partial def instApi (h : HostState) (e : InstState) : InstApi := { bindChain := fun p f band => instBind h e p none (some f) band exportValue := fun k v => do e.exports.set ((← e.exports.get).set k v) provides := fun p => do e.provides.set ((← e.provides.get).push p) + capability := fun n => instCapability h e n acquire := instAcquire h e giveback := instGiveback h e release := instRelease h e diff --git a/lean/test/Driver.lean b/lean/test/Driver.lean index 77a63d2..ee9a261 100644 --- a/lean/test/Driver.lean +++ b/lean/test/Driver.lean @@ -149,6 +149,19 @@ def depDefine (i : InstApi) : PluginM Unit := do if exports.isMap then for k in exports.keys do i.exportValue k (exports.get k) +/-- WHICH provider this instance took, when the entry asks. See +typescript/test/driver.ts. + +`dep` has no `acquire` in this port and gains none here: the entries +that read `cap` assert `result`, never `open`, so adding one would +change what every other `dep` entry sees for nothing. -/ +def depActivate (i : InstApi) : PluginM Unit := do + let capof ← opt i "capof" + if !capof.isStr then return + match ← i.capability capof.asStr with + | some r => i.exportValue "cap" (.str r) + | none => i.exportValue "cap" .null + def providerDefine (i : InstApi) : PluginM Unit := do i.setState ((← i.getState).set "count" (.num 0.0)) let point ← opt i "point" @@ -189,7 +202,8 @@ def probeDef (name : String) : Definition := define := some greedyDefine activate := some (fun i => do greedyCapture i; greedyBindAt i "activate") deactivate := some (fun i => greedyBindAt i "deactivate") } - else if name == "dep" then { base with define := some depDefine } + else if name == "dep" then + { base with define := some depDefine, activate := some depActivate } else if name == "provider" then { base with define := some providerDefine } else base diff --git a/lua/src/plugin/host.lua b/lua/src/plugin/host.lua index 3872f62..fb42501 100644 --- a/lua/src/plugin/host.lua +++ b/lua/src/plugin/host.lua @@ -141,6 +141,22 @@ function Inst:export(key, value) self.entry.exportkeys[key] = true end +-- WHICH provider this instance is bound to for `name` (11.1), as a ref, +-- or nil when nothing provides it. +-- +-- The host's own `capability` answers with the live providers RANKED, +-- not with the one THIS instance took; 11.4's reluctant rebinding makes +-- those differ. A REF, not the instance. The selection is REMEMBERED, +-- because this is the instance asking. +function Inst:capability(name) + for _, req in ipairs(Dep.requirements(self.entry.options)) do + if req.name == name then + return self.host:chosen(self.entry, req, true) + end + end + return nil +end + -- What this instance can do for others (section 11.1). function Inst:provides(prov) table.insert(self.entry.provides, prov) diff --git a/lua/test/driver.lua b/lua/test/driver.lua index 043e1fb..4766d53 100644 --- a/lua/test/driver.lua +++ b/lua/test/driver.lua @@ -213,7 +213,14 @@ function M.probes() i:export(k, exports[k]) end end, - activate = function(i) i:acquire() end, + activate = function(i) + i:acquire() + -- WHICH provider this instance took, when the entry asks. See typescript/test/driver.ts. + local capof = T.getv(i:options(), 'capof') + if capof then + i:export('cap', i:capability(capof)) + end + end, } out[#out + 1] = { diff --git a/ocaml/src/host.ml b/ocaml/src/host.ml index 648915e..d2d466d 100644 --- a/ocaml/src/host.ml +++ b/ocaml/src/host.ml @@ -355,6 +355,22 @@ let chosen h e req remember = Some first end +(* WHICH provider this instance is bound to for `name` (§11.1), as a + ref, or None when nothing provides it. + + The host's own `capability` answers with the live providers RANKED, + not with the one THIS instance took; §11.4's reluctant rebinding + makes those differ. A REF, not the instance. The selection is + REMEMBERED, because this is the instance asking. *) +let instcapability e name = + match + List.find_opt + (fun r -> V.is_str (V.get r "name") && V.as_str (V.get r "name") = name) + (V.items (Depend.requirements e.options)) + with + | None -> None + | Some req -> chosen e.owner e req true + (* The instance currently SELECTED for each of this one's restart-causing requirements. A BINDING IS TO AN INSTANCE, not to a capability (§11.1): the selected one going away restarts a `static` diff --git a/ocaml/test/driver.ml b/ocaml/test/driver.ml index dafb6d2..aa97838 100644 --- a/ocaml/test/driver.ml +++ b/ocaml/test/driver.ml @@ -205,6 +205,20 @@ let depdefine (i : inst) = if V.is_map exports then List.iter (fun k -> Host.exportvalue i k (V.get exports k)) (V.keys exports) +(* WHICH provider this instance took, when the entry asks. See + typescript/test/driver.ts. + + `dep` has no `acquire` in this port and gains none here: the entries + that read `cap` assert `result`, never `open`, so adding one would + change what every other `dep` entry sees for nothing. *) +let depactivate (i : inst) = + let capof = opt i "capof" in + if V.is_str capof then + Host.exportvalue i "cap" + (match Host.instcapability i (V.as_str capof) with + | None -> V.vnull + | Some r -> V.vstr r) + let providerdefine (i : inst) = V.set i.istate "count" (V.vnum 0.0); let point = opt i "point" in @@ -269,7 +283,7 @@ and probedef name = define = Some greedydefine; activate = Some (fun i -> greedycapture i; greedybindat i "activate"); deactivate = Some (fun i -> greedybindat i "deactivate") } - | "dep" -> { base with define = Some depdefine } + | "dep" -> { base with define = Some depdefine; activate = Some depactivate } | "provider" -> { base with define = Some providerdefine } | _ -> base diff --git a/perl/lib/Voxgig/Plugin/Host.pm b/perl/lib/Voxgig/Plugin/Host.pm index 83fd6fd..9727087 100644 --- a/perl/lib/Voxgig/Plugin/Host.pm +++ b/perl/lib/Voxgig/Plugin/Host.pm @@ -156,6 +156,23 @@ our @EXPORT_OK = qw(make_host); return; } + # WHICH provider this instance is bound to for $name (11.1), as a + # ref, or undef when nothing provides it. + # + # The host's own `capability` answers with the live providers + # RANKED, not with the one THIS instance took; 11.4's reluctant + # rebinding makes those differ. A REF, not the instance: every port + # can return a string and a corpus entry can assert on one. The + # selection is REMEMBERED, because this is the instance asking. + sub capability { + my ($self, $name) = @_; + for my $req (@{ Voxgig::Plugin::Depend::requirements($self->{entry}{options}) }) { + return $self->{host}->chosen($self->{entry}, $req, 1) + if ($req->{name} // '') eq $name; + } + return undef; + } + # What this instance can do for others (section 11.1). sub provides { my ($self, $prov) = @_; diff --git a/perl/test/Driver.pm b/perl/test/Driver.pm index 7e8e555..ac96b72 100644 --- a/perl/test/Driver.pm +++ b/perl/test/Driver.pm @@ -176,7 +176,15 @@ sub probes { $i->export($_, $exports->{$_}) for sortedkeys($exports); return; }, - activate => sub { $_[0]->acquire; return }, + activate => sub { + my ($i) = @_; + $i->acquire; + # WHICH provider this instance took, when the entry asks. + # See typescript/test/driver.ts. + my $capof = $i->options->{capof}; + $i->export('cap', $i->capability($capof)) if defined $capof; + return; + }, }; my $provider = { diff --git a/php/src/Host.php b/php/src/Host.php index ad6c01a..0574812 100644 --- a/php/src/Host.php +++ b/php/src/Host.php @@ -232,6 +232,24 @@ public function export(string $key, $value): void $this->entry->exports[$key] = $value; } + /** WHICH provider this instance is bound to for $name (§11.1), as a + * ref, or null when nothing provides it. + * + * The host's own `capability` answers with the live providers + * RANKED, not with the one THIS instance took; §11.4's reluctant + * rebinding makes those differ. A REF, not the instance: every port + * can return a string and a corpus entry can assert on one. The + * selection is REMEMBERED, because this is the instance asking. */ + public function capability(string $name): ?string + { + foreach (requirements($this->entry->options) as $req) { + if (($req['name'] ?? null) === $name) { + return $this->hostref->instcapability($this->entry, $req); + } + } + return null; + } + /** What this instance can do for others (§11.1). */ public function provides(array $prov): void { @@ -830,6 +848,12 @@ private function unmetof(Entry $entry): array * * @param array $req */ + /** The instance api's way onto `chosen`, which is private. */ + public function instcapability(Entry $entry, array $req): ?string + { + return $this->chosen($entry, $req, true); + } + private function chosen(Entry $entry, array $req, bool $remember): ?string { $cands = $this->providersof($req); diff --git a/php/test/driver.php b/php/test/driver.php index 13ea62d..e4c50fb 100644 --- a/php/test/driver.php +++ b/php/test/driver.php @@ -211,6 +211,12 @@ public static function probes(): array }, 'activate' => static function (Inst $i): void { $i->acquire(); + // WHICH provider this instance took, when the entry asks. + // See typescript/test/driver.ts. + $capof = $i->options()['capof'] ?? null; + if (null !== $capof) { + $i->export('cap', $i->capability($capof)); + } }, ]; diff --git a/python/test/driver.py b/python/test/driver.py index 9ad51b3..5e5a372 100644 --- a/python/test/driver.py +++ b/python/test/driver.py @@ -138,8 +138,16 @@ def dep_define(i): for key in sorted(i.options.get('exports') or {}): i.export(key, i.options['exports'][key]) + def dep_activate(i): + i.acquire() + # WHICH provider this instance took, when the entry asks. See + # typescript/test/driver.ts: the host's own `capability` answers + # with the RANKING, not with this instance's choice. + if i.options.get('capof'): + i.export('cap', i.capability(i.options['capof'])) + dep = {'name': 'dep', 'define': dep_define, - 'activate': lambda i: i.acquire()} + 'activate': dep_activate} def provider_define(i): i.state['count'] = 0 diff --git a/python/voxgig_plugin/host.py b/python/voxgig_plugin/host.py index 8242426..5992357 100644 --- a/python/voxgig_plugin/host.py +++ b/python/voxgig_plugin/host.py @@ -126,6 +126,22 @@ def export(self, key, value): 11).""" self._entry['exports'][key] = value + def capability(self, name): + """WHICH provider this instance is bound to for `name` (section + 11.1), as a ref, or None when nothing provides it. + + The host's own `capability` answers with the live providers + RANKED, not with the one THIS instance took; section 11.4's + reluctant rebinding makes those differ. A REF, not the instance: + every port can return a string and a corpus entry can assert on + one. The selection is REMEMBERED, because this is the instance + asking. + """ + for req in requirements(self._entry['options']): + if req['name'] == name: + return self._host._chosen(self._entry, req, True) + return None + def provides(self, prov): """What this instance can do for others (section 11.1).""" self._entry['provides'].append(prov) diff --git a/ruby/lib/voxgig_plugin/host.rb b/ruby/lib/voxgig_plugin/host.rb index c9413ac..ee56fe5 100644 --- a/ruby/lib/voxgig_plugin/host.rb +++ b/ruby/lib/voxgig_plugin/host.rb @@ -133,6 +133,20 @@ def export(key, value) @entry['exports'][key] = value end + # WHICH provider this instance is bound to for `name` (11.1), as a + # ref, or nil when nothing provides it. + # + # The host's own `capability` answers with the live providers + # RANKED, not with the one THIS instance took; 11.4's reluctant + # rebinding makes those differ. A REF, not the instance: every port + # can return a string and a corpus entry can assert on one. The + # selection is REMEMBERED, because this is the instance asking. + def capability(name) + req = VoxgigPlugin.requirements(@entry['options']).find { |r| r['name'] == name } + return nil if req.nil? + @host.send(:chosen, @entry, req, true) + end + # What this instance can do for others (section 11.1). def provides(prov) @entry['provides'] << prov diff --git a/ruby/test/driver.rb b/ruby/test/driver.rb index 7e1229e..bb2df89 100644 --- a/ruby/test/driver.rb +++ b/ruby/test/driver.rb @@ -134,7 +134,12 @@ def self.probes i.export(k, i.options['exports'][k]) end end, - 'activate' => ->(i) { i.acquire } + 'activate' => lambda do |i| + i.acquire + # WHICH provider this instance took, when the entry asks. See + # typescript/test/driver.ts. + i.export('cap', i.capability(i.options['capof'])) if i.options['capof'] + end } provider = { diff --git a/rust/src/host.rs b/rust/src/host.rs index 8f9b89b..c42ae80 100644 --- a/rust/src/host.rs +++ b/rust/src/host.rs @@ -1527,6 +1527,28 @@ impl Inst { .insert(key.to_string(), value); } + /// WHICH provider this instance is bound to for `name` (§11.1), as a + /// ref, or None when nothing provides it. + /// + /// The host's own `capability` answers with the live providers + /// RANKED, not with the one THIS instance took; §11.4's reluctant + /// rebinding makes those differ. A REF, not the instance: every port + /// can return a string and a corpus entry can assert on one. The + /// selection is REMEMBERED, because this is the instance asking. + pub fn capability(&self, name: &str) -> Option { + // THE BORROW ENDS BEFORE `chosen` DOES. `chosen` remembers the + // selection, which takes `borrow_mut` on the same entry -- so + // reading the requirements inline held a shared borrow across it + // and panicked at the write. Rust is the only port that says so. + let reqs = requirements(&self.entry.borrow().options); + for req in reqs { + if req.get("name").as_str() == Some(name) { + return self.host.chosen(&self.entry, &req, true); + } + } + None + } + /// What this instance can do for others (§11.1). pub fn provides(&self, prov: Value) { self.entry.borrow_mut().provides.push(prov); diff --git a/rust/tests/support/driver.rs b/rust/tests/support/driver.rs index 6cad37f..597f6b4 100644 --- a/rust/tests/support/driver.rs +++ b/rust/tests/support/driver.rs @@ -215,6 +215,18 @@ pub fn probes() -> Vec { })); dep.activate = Some(Rc::new(|i: &Inst| { i.acquire()?; + // WHICH provider this instance took, when the entry asks. See + // typescript/test/driver.ts. + let capof = i.options().get("capof"); + if let Some(name) = capof.as_str() { + i.export( + "cap", + match i.capability(name) { + Some(r) => Value::str(&r), + None => Value::Null, + }, + ); + } Ok(()) })); out.push(dep); diff --git a/scala/src/Host.scala b/scala/src/Host.scala index dfd6a7b..090dec6 100644 --- a/scala/src/Host.scala +++ b/scala/src/Host.scala @@ -243,6 +243,19 @@ final class Inst(val host: Host, private val entry: Entry) { } /** What this instance can do for others (section 11.1). */ + /** WHICH provider this instance is bound to for `name` (§11.1), as a + * ref, or None when nothing provides it. + * + * The host's own `capability` answers with the live providers RANKED, + * not with the one THIS instance took; §11.4's reluctant rebinding + * makes those differ. A REF, not the instance. The selection is + * REMEMBERED, because this is the instance asking. */ + def capability(name: String): Option[String] = + Depend + .requirements(entry.options) + .find(req => req.at("name").asString.contains(name)) + .flatMap(req => host.instcapability(entry, req)) + def provides(prov: Value): Unit = { entry.provides += prov; () } /** Where this binding landed (section 6.6) - the plugin-side counterpart to a @@ -661,6 +674,10 @@ final class Host(opts: HostOptions = HostOptions()) { * `remember` is false for the questions asked ABOUT an instance rather than * BY it: introspection must not create a binding. */ + /** The instance api's way onto `chosen`, which is private. */ + private[plugin] def instcapability(entry: Entry, req: Value): Option[String] = + chosen(entry, req, remember = true) + private def chosen(entry: Entry, req: Value, remember: Boolean): Option[String] = { val cands = providersOf(req) if (cands.isEmpty) return None diff --git a/scala/test/Driver.scala b/scala/test/Driver.scala index aaaaecb..88a3069 100644 --- a/scala/test/Driver.scala +++ b/scala/test/Driver.scala @@ -207,7 +207,14 @@ object Driver { val exports = opt(i, "exports") exports.keys.foreach(k => i.`export`(k, exports.at(k))) }, - activate = Some((i: Inst) => { i.acquire(); () }) + activate = Some((i: Inst) => { + i.acquire() + // WHICH provider this instance took, when the entry asks. See typescript/test/driver.ts. + i.options.at("capof").asString.foreach { capof => + i.`export`("cap", i.capability(capof).map(VStr(_)).getOrElse(VNull)) + } + () + }) ) val provider = Definition( diff --git a/spec/plugin.aon b/spec/plugin.aon index 2ad355c..1886d82 100644 --- a/spec/plugin.aon +++ b/spec/plugin.aon @@ -3402,6 +3402,156 @@ primary: depend: { ] + # `inst.capability(name)` — WHICH provider this instance is bound to. + bound: set: [ + # WHICH PROVIDER THIS INSTANCE TOOK (§11.1). The host's own + # `capability` answers with the live providers RANKED; this answers + # with the one THIS instance is bound to, which §11.4's reluctant + # rebinding makes a different question. `dep` exports the answer as + # `cap` when `capof` names one of its requirements. + { + id: 'depend/bound#selected', doc: true + in: [ + { do: 'ready', ref: 'dep$p', definition: 'dep', options: { provides: [ { name: 'clock' } ] } } + { do: 'ready', ref: 'dep$c', definition: 'dep' + options: { requires: ['clock'], capof: 'clock' } } + { do: 'export', key: 'dep$c/cap' } + ] + match: { out: { result: 'dep$p' } } + } + # RANK DECIDES WHICH ONE, and the answer is the instance's, not the + # first declared: `dep$hi` provides version 2 and wins over `dep$lo` + # at version 1 though it was declared second. + { + id: 'depend/bound#ranked' + in: [ + { do: 'ready', ref: 'dep$lo', definition: 'dep' + options: { provides: [ { name: 'clock', version: '1.0.0' } ] } } + { do: 'ready', ref: 'dep$hi', definition: 'dep' + options: { provides: [ { name: 'clock', version: '2.0.0' } ] } } + { do: 'ready', ref: 'dep$c', definition: 'dep' + options: { requires: ['clock'], capof: 'clock' } } + { do: 'export', key: 'dep$c/cap' } + ] + match: { out: { result: 'dep$hi' } } + } + # AN OPTIONAL REQUIREMENT WITH NOBODY PROVIDING IT is the case §11.3 + # names: a plugin that works without metrics and uses metrics when + # it is there has to be able to ask, and gets absent rather than a + # refusal. + { + id: 'depend/bound#optional-absent' + in: [ + { do: 'ready', ref: 'dep$c', definition: 'dep' + options: { requires: ['metrics'], optional: ['metrics'], capof: 'metrics' } } + { do: 'export', key: 'dep$c/cap' } + ] + match: { out: { result: '__NULL__' } } + } + # A NAME THIS INSTANCE DOES NOT REQUIRE is absent too, rather than + # answering with whoever happens to provide it: the question is what + # THIS instance is bound to. + { + id: 'depend/bound#not-required' + in: [ + { do: 'ready', ref: 'dep$p', definition: 'dep', options: { provides: [ { name: 'clock' } ] } } + { do: 'ready', ref: 'dep$c', definition: 'dep' + options: { requires: ['other'], optional: ['other'], capof: 'clock' } } + { do: 'export', key: 'dep$c/cap' } + ] + match: { out: { result: '__NULL__' } } + } + # THE NAME IS READ, not assumed. An instance with TWO satisfied + # requirements is the only shape that can tell a lookup from a + # lookup-shaped `requirements[0]`, and every other entry here has + # exactly one — so the shortest wrong implementation passed the lot + # of them. Both directions, because taking the LAST is as wrong as + # taking the first and neither entry alone says so. + { + id: 'depend/bound#named-second' + in: [ + { do: 'ready', ref: 'dep$o', definition: 'dep', options: { provides: [ { name: 'other' } ] } } + { do: 'ready', ref: 'dep$p', definition: 'dep', options: { provides: [ { name: 'clock' } ] } } + { do: 'ready', ref: 'dep$c', definition: 'dep' + options: { requires: ['other', 'clock'], capof: 'clock' } } + { do: 'export', key: 'dep$c/cap' } + ] + match: { out: { result: 'dep$p' } } + } + { + id: 'depend/bound#named-first' + in: [ + { do: 'ready', ref: 'dep$o', definition: 'dep', options: { provides: [ { name: 'other' } ] } } + { do: 'ready', ref: 'dep$p', definition: 'dep', options: { provides: [ { name: 'clock' } ] } } + { do: 'ready', ref: 'dep$c', definition: 'dep' + options: { requires: ['clock', 'other'], capof: 'clock' } } + { do: 'export', key: 'dep$c/cap' } + ] + match: { out: { result: 'dep$p' } } + } + # A REF REQUIREMENT ANSWERS WITH THE REF (§11.1's "a ref satisfies + # too"), and this is the pair that makes the instance-side question + # a DIFFERENT question rather than a spelling of the host's. The + # next entry asks `host.capability` for the same name and gets + # NOTHING: a ref is not a declared capability, so the host has no + # provider record to rank. Answering this one by ranking, the + # shortest wrong implementation there is, passes every other entry + # in this group. + { + id: 'depend/bound#by-ref', doc: true + in: [ + { do: 'ready', ref: 'dep$p', definition: 'dep' } + { do: 'ready', ref: 'dep$c', definition: 'dep' + options: { requires: ['dep$p'], capof: 'dep$p' } } + { do: 'export', key: 'dep$c/cap' } + ] + match: { out: { result: 'dep$p' } } + } + { + id: 'depend/bound#by-ref-host-disagrees' + in: [ + { do: 'ready', ref: 'dep$p', definition: 'dep' } + { do: 'ready', ref: 'dep$c', definition: 'dep' + options: { requires: ['dep$p'], capof: 'dep$p' } } + { do: 'capability', name: 'dep$p' } + ] + match: { out: { result: [] } } + } + # AND THEY PART COMPANY THE OTHER WAY TOO, which is §11.4's + # reluctance seen from the outside: `dep$c` binds `dep$lo`, then + # `dep$hi` arrives outranking it, and `dep$c` is NOT re-bound — so + # what this instance took and what the host ranks first are two + # different refs at the same instant. The next entry is the same + # run, asking the host. + { + id: 'depend/bound#reluctant', doc: true + in: [ + { do: 'ready', ref: 'dep$lo', definition: 'dep' + options: { provides: [ { name: 'clock', version: '1.0.0' } ] } } + { do: 'ready', ref: 'dep$c', definition: 'dep' + options: { requires: ['clock'], capof: 'clock' } } + { do: 'ready', ref: 'dep$hi', definition: 'dep' + options: { provides: [ { name: 'clock', version: '2.0.0' } ] } } + { do: 'export', key: 'dep$c/cap' } + ] + match: { out: { result: 'dep$lo' } } + } + { + id: 'depend/bound#reluctant-host-ranks' + in: [ + { do: 'ready', ref: 'dep$lo', definition: 'dep' + options: { provides: [ { name: 'clock', version: '1.0.0' } ] } } + { do: 'ready', ref: 'dep$c', definition: 'dep' + options: { requires: ['clock'], capof: 'clock' } } + { do: 'ready', ref: 'dep$hi', definition: 'dep' + options: { provides: [ { name: 'clock', version: '2.0.0' } ] } } + { do: 'capability', name: 'clock' } + ] + match: { out: { result: ['dep$hi', 'dep$lo'] } } + } + ] + + # A REF SATISFIES TOO (§11.1), AND THE COMPARISON IS CANONICAL # (§4 rule 5). # diff --git a/spec/plugin.json b/spec/plugin.json index bc95b03..6063680 100644 --- a/spec/plugin.json +++ b/spec/plugin.json @@ -4930,6 +4930,434 @@ } ] }, + "bound": { + "set": [ + { + "doc": true, + "id": "depend/bound#selected", + "in": [ + { + "definition": "dep", + "do": "ready", + "options": { + "provides": [ + { + "name": "clock" + } + ] + }, + "ref": "dep$p" + }, + { + "definition": "dep", + "do": "ready", + "options": { + "capof": "clock", + "requires": [ + "clock" + ] + }, + "ref": "dep$c" + }, + { + "do": "export", + "key": "dep$c/cap" + } + ], + "match": { + "out": { + "result": "dep$p" + } + } + }, + { + "id": "depend/bound#ranked", + "in": [ + { + "definition": "dep", + "do": "ready", + "options": { + "provides": [ + { + "name": "clock", + "version": "1.0.0" + } + ] + }, + "ref": "dep$lo" + }, + { + "definition": "dep", + "do": "ready", + "options": { + "provides": [ + { + "name": "clock", + "version": "2.0.0" + } + ] + }, + "ref": "dep$hi" + }, + { + "definition": "dep", + "do": "ready", + "options": { + "capof": "clock", + "requires": [ + "clock" + ] + }, + "ref": "dep$c" + }, + { + "do": "export", + "key": "dep$c/cap" + } + ], + "match": { + "out": { + "result": "dep$hi" + } + } + }, + { + "id": "depend/bound#optional-absent", + "in": [ + { + "definition": "dep", + "do": "ready", + "options": { + "capof": "metrics", + "optional": [ + "metrics" + ], + "requires": [ + "metrics" + ] + }, + "ref": "dep$c" + }, + { + "do": "export", + "key": "dep$c/cap" + } + ], + "match": { + "out": { + "result": "__NULL__" + } + } + }, + { + "id": "depend/bound#not-required", + "in": [ + { + "definition": "dep", + "do": "ready", + "options": { + "provides": [ + { + "name": "clock" + } + ] + }, + "ref": "dep$p" + }, + { + "definition": "dep", + "do": "ready", + "options": { + "capof": "clock", + "optional": [ + "other" + ], + "requires": [ + "other" + ] + }, + "ref": "dep$c" + }, + { + "do": "export", + "key": "dep$c/cap" + } + ], + "match": { + "out": { + "result": "__NULL__" + } + } + }, + { + "id": "depend/bound#named-second", + "in": [ + { + "definition": "dep", + "do": "ready", + "options": { + "provides": [ + { + "name": "other" + } + ] + }, + "ref": "dep$o" + }, + { + "definition": "dep", + "do": "ready", + "options": { + "provides": [ + { + "name": "clock" + } + ] + }, + "ref": "dep$p" + }, + { + "definition": "dep", + "do": "ready", + "options": { + "capof": "clock", + "requires": [ + "other", + "clock" + ] + }, + "ref": "dep$c" + }, + { + "do": "export", + "key": "dep$c/cap" + } + ], + "match": { + "out": { + "result": "dep$p" + } + } + }, + { + "id": "depend/bound#named-first", + "in": [ + { + "definition": "dep", + "do": "ready", + "options": { + "provides": [ + { + "name": "other" + } + ] + }, + "ref": "dep$o" + }, + { + "definition": "dep", + "do": "ready", + "options": { + "provides": [ + { + "name": "clock" + } + ] + }, + "ref": "dep$p" + }, + { + "definition": "dep", + "do": "ready", + "options": { + "capof": "clock", + "requires": [ + "clock", + "other" + ] + }, + "ref": "dep$c" + }, + { + "do": "export", + "key": "dep$c/cap" + } + ], + "match": { + "out": { + "result": "dep$p" + } + } + }, + { + "doc": true, + "id": "depend/bound#by-ref", + "in": [ + { + "definition": "dep", + "do": "ready", + "ref": "dep$p" + }, + { + "definition": "dep", + "do": "ready", + "options": { + "capof": "dep$p", + "requires": [ + "dep$p" + ] + }, + "ref": "dep$c" + }, + { + "do": "export", + "key": "dep$c/cap" + } + ], + "match": { + "out": { + "result": "dep$p" + } + } + }, + { + "id": "depend/bound#by-ref-host-disagrees", + "in": [ + { + "definition": "dep", + "do": "ready", + "ref": "dep$p" + }, + { + "definition": "dep", + "do": "ready", + "options": { + "capof": "dep$p", + "requires": [ + "dep$p" + ] + }, + "ref": "dep$c" + }, + { + "do": "capability", + "name": "dep$p" + } + ], + "match": { + "out": { + "result": [] + } + } + }, + { + "doc": true, + "id": "depend/bound#reluctant", + "in": [ + { + "definition": "dep", + "do": "ready", + "options": { + "provides": [ + { + "name": "clock", + "version": "1.0.0" + } + ] + }, + "ref": "dep$lo" + }, + { + "definition": "dep", + "do": "ready", + "options": { + "capof": "clock", + "requires": [ + "clock" + ] + }, + "ref": "dep$c" + }, + { + "definition": "dep", + "do": "ready", + "options": { + "provides": [ + { + "name": "clock", + "version": "2.0.0" + } + ] + }, + "ref": "dep$hi" + }, + { + "do": "export", + "key": "dep$c/cap" + } + ], + "match": { + "out": { + "result": "dep$lo" + } + } + }, + { + "id": "depend/bound#reluctant-host-ranks", + "in": [ + { + "definition": "dep", + "do": "ready", + "options": { + "provides": [ + { + "name": "clock", + "version": "1.0.0" + } + ] + }, + "ref": "dep$lo" + }, + { + "definition": "dep", + "do": "ready", + "options": { + "capof": "clock", + "requires": [ + "clock" + ] + }, + "ref": "dep$c" + }, + { + "definition": "dep", + "do": "ready", + "options": { + "provides": [ + { + "name": "clock", + "version": "2.0.0" + } + ] + }, + "ref": "dep$hi" + }, + { + "do": "capability", + "name": "clock" + } + ], + "match": { + "out": { + "result": [ + "dep$hi", + "dep$lo" + ] + } + } + } + ] + }, "byref": { "set": [ { diff --git a/swift/src/Host.swift b/swift/src/Host.swift index 7d3700b..5cc06ff 100644 --- a/swift/src/Host.swift +++ b/swift/src/Host.swift @@ -167,6 +167,21 @@ public final class Inst { entry.exports[key] = value } + /// WHICH provider this instance is bound to for `name` (section + /// 11.1), as a ref, or nil when nothing provides it. + /// + /// The host's own `capability` answers with the live providers + /// RANKED, not with the one THIS instance took; section 11.4's + /// reluctant rebinding makes those differ. A REF, not the instance. + /// The selection is REMEMBERED, because this is the instance asking. + public func capability(_ name: String) -> String? { + for req in Depend.requirements(entry.options) + where req.at("name").asString == name { + return host.chosen(entry, req, true) + } + return nil + } + /// What this instance can do for others (section 11.1). public func provides(_ prov: Value) { entry.provides.append(prov) diff --git a/swift/test/Driver.swift b/swift/test/Driver.swift index e54f6a5..7de9d07 100644 --- a/swift/test/Driver.swift +++ b/swift/test/Driver.swift @@ -211,7 +211,18 @@ enum Driver { let exports = opt(i, "exports") for k in exports.keys { i.export(k, exports.at(k)) } }, - activate: { i in _ = try i.acquire() } + activate: { i in + _ = try i.acquire() + // WHICH provider this instance took, when the entry asks. + // See typescript/test/driver.ts. + if let capof = opt(i, "capof").asString { + if let picked = i.capability(capof) { + i.export("cap", .str(picked)) + } else { + i.export("cap", .null) + } + } + } ) let provider = Definition( diff --git a/typescript/src/Host.ts b/typescript/src/Host.ts index 1e2de61..d2dfaad 100644 --- a/typescript/src/Host.ts +++ b/typescript/src/Host.ts @@ -264,6 +264,32 @@ export function makehost(options?: HostOptions) { /** Published for other plugins and for the application (§11). */ export: (key: string, value: any) => { e.exports[key] = value }, + /** WHICH provider this instance is bound to for `name` (§11.1), + * as a ref, or undefined when nothing provides it. + * + * §11.1 says "the first is bound, and `inst.capability(name)` + * returns it", and §11.3 gives the case that needs it: a plugin + * that works without metrics and uses metrics when it is there + * has to be able to ask. Every port had `host.capability(name)`, + * which answers with the live providers RANKED — not with the one + * THIS instance actually took. §11.4's reluctant rebinding makes + * those differ: a better-ranked newcomer tops the ranking while + * the consumer keeps what it had. + * + * A REF, not the instance. `host.capability` answers in refs, + * every port can return a string, and a corpus entry can assert + * on one — an instance api is shaped differently in each and + * cannot be asserted at all. + * + * The selection is REMEMBERED, because this is the instance + * asking. `chosen(..., false)` is for questions asked ABOUT an + * instance, where answering must not create a binding. */ + capability: (name: string): string | undefined => { + const req = requirements(e.options).find((r) => r.name === name) + if (undefined === req) return undefined + return chosen(e, req, true) + }, + /** What this instance can do for others (§11.1). */ provides: (p: Provided) => { e.provides.push(p) }, diff --git a/typescript/test/driver.ts b/typescript/test/driver.ts index fae8e1a..3a532da 100644 --- a/typescript/test/driver.ts +++ b/typescript/test/driver.ts @@ -150,7 +150,22 @@ export function probes(): Definition[] { for (const k of Object.keys(i.options.exports)) i.export(k, i.options.exports[k]) } }, - activate: (i: any) => { i.acquire() }, + activate: (i: any) => { + i.acquire() + // WHICH provider this instance took, when the entry asks for it. + // `options.capof` names one of this instance's requirements and + // the answer is exported as `cap`, which is the only way a corpus + // entry can see `inst.capability` at all: the host's own + // `capability` answers with the RANKING, not with the choice this + // instance made, and §11.4 makes those differ. + // + // From `activate` rather than `define`, because the selection is + // made at activation — and so a deactivate/reactivate cycle + // re-exports whatever the second activation chose. + if (i.options && i.options.capof) { + i.export('cap', i.capability(i.options.capof)) + } + }, } const provider: Definition = { diff --git a/zig/src/host.zig b/zig/src/host.zig index 6394bc3..4446e16 100644 --- a/zig/src/host.zig +++ b/zig/src/host.zig @@ -421,6 +421,22 @@ fn chosen(h: *Host, e: *Inst, req: ?*v.Value, remember: bool) ?[]const u8 { return first; } +/// WHICH provider this instance is bound to for `name` (§11.1), as a +/// ref, or null when nothing provides it. +/// +/// The host's own `capability` answers with the live providers RANKED, +/// not with the one THIS instance took; §11.4's reluctant rebinding +/// makes those differ. A REF, not the instance. The selection is +/// REMEMBERED, because this is the instance asking. +pub fn instcapability(e: *Inst, name: []const u8) ?[]const u8 { + for (v.items(dep.requirements(e.options))) |r| { + const rn = v.get(r, "name"); + if (!v.isStr(rn) or !std.mem.eql(u8, v.asStr(rn), name)) continue; + return chosen(e.owner, e, r, true); + } + return null; +} + /// The instance currently SELECTED for each of this one's /// restart-causing requirements. A BINDING IS TO AN INSTANCE, not to a /// capability (§11.1): the selected one going away restarts a `static` diff --git a/zig/test/driver.zig b/zig/test/driver.zig index 95fa27d..8e515a9 100644 --- a/zig/test/driver.zig +++ b/zig/test/driver.zig @@ -235,6 +235,19 @@ fn depDefine(i: *Inst) t.Err!void { } } +// WHICH provider this instance took, when the entry asks. See +// typescript/test/driver.ts. +// +// `dep` has no `acquire` in this port and gains none here: the entries +// that read `cap` assert `result`, never `open`, so adding one would +// change what every other `dep` entry sees for nothing. +fn depActivate(i: *Inst) t.Err!void { + const capof = opt(i, "capof"); + if (!v.isStr(capof)) return; + const picked = host.instcapability(i, v.asStr(capof)); + host.exportvalue(i, "cap", if (picked) |r| v.vstr(r) else v.vnull()); +} + fn providerDefine(i: *Inst) t.Err!void { v.set(i.state, "count", v.vnum(0)); const pt = opt(i, "point"); @@ -266,6 +279,7 @@ fn probedef(name: []const u8) *catalog.Definition { d.deactivate = greedyDeactivate; } else if (std.mem.eql(u8, name, "dep")) { d.define = depDefine; + d.activate = depActivate; } else if (std.mem.eql(u8, name, "provider")) { d.define = providerDefine; } From 2e5407333788b4f640c8240f5f0ba101efbc44e1 Mon Sep 17 00:00:00 2001 From: Claude Date: Wed, 16 Sep 2026 11:25:17 +0000 Subject: [PATCH 8/9] probe: `dep` holds a resource, in the five ports where it did not MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit The canonical `dep` acquires one synthetic resource per activation, the way `probe` does. `c`, `cpp`, `ocaml`, `zig` and `lean` gave it no `activate` at all, so in five of twenty-three ports it held nothing. The corpus could not tell. `open` is in every entry's `out`, and no entry with a live `dep` had ever asserted it — so the probe catalog, which DOCS.md §4.3 exists to keep identical, diverged in silence. Found while giving `dep` an `activate` for `options.capof`, by reading the canonical rather than the nearest port. `depend/bound#dep-holds` asserts `open: 2` for a provider and a consumer. Taking the `acquire` back out of any one of the five fails that entry and nothing else. Corpus 590 -> 591, all 23 ports green, and §4.3 now says `dep` holds. Co-Authored-By: Claude Opus 5 Claude-Session: https://claude.ai/code/session_01CVMgjjwQfTJ2rXz637Wpk8 --- AGENTS.md | 4 ++-- CLAUDE.md | 2 +- DOCS.md | 2 +- README.md | 4 ++-- c/test/driver.c | 8 +++----- cpp/test/driver.cpp | 8 +++----- doc/plan/progress.md | 2 +- doc/plan/status.md | 2 +- lean/test/Driver.lean | 8 +++----- ocaml/test/driver.ml | 8 +++----- spec/plugin.aon | 15 +++++++++++++++ spec/plugin.json | 38 ++++++++++++++++++++++++++++++++++++++ zig/test/driver.zig | 8 +++----- 13 files changed, 76 insertions(+), 33 deletions(-) diff --git a/AGENTS.md b/AGENTS.md index 442bd21..33d2d24 100644 --- a/AGENTS.md +++ b/AGENTS.md @@ -5,7 +5,7 @@ Read this before changing anything. The design is below (§n) are to it. **Status: P6 COMPLETE — six of six. Every planned port exists.** All -**19 corpus sections** exist — 590 entries — with the driver contract +**19 corpus sections** exist — 591 entries — with the driver contract in `DOCS.md` §4, and **twenty-three implementations pass every one of them**: `typescript/` (canonical), `go/`, `python/`, `javascript/`, `ruby/`, `php/`, `perl/`, `rust/`, `java/`, `lua/`, `csharp/`, `elixir/`, `clojure/`, @@ -283,7 +283,7 @@ decide, and `handover.md` §19 says what the six of them found. **All three corpus gaps §18 of the handover records are CLOSED** — gap 1 by `declare/shape` and `declare/register`, gap 2 by `depend/byref`, -gap 3 by `nest/open`. The corpus is 590 entries and every one of them +gap 3 by `nest/open`. The corpus is 591 entries and every one of them is mutation-checked against the behaviour it names. **Gap 1 was the expensive one, and §18's "cheap" was wrong about it.** Nothing carried a diff --git a/CLAUDE.md b/CLAUDE.md index 11abc9d..3d120b4 100644 --- a/CLAUDE.md +++ b/CLAUDE.md @@ -24,7 +24,7 @@ Quick reminders (the full rationale is in `AGENTS.md`): Two gates enforce it, `vale` and `python3 tools/check_prose.py`; `make scan-prose` runs both. -**Status: P6 COMPLETE — six of six.** The corpus is 590 entries across +**Status: P6 COMPLETE — six of six.** The corpus is 591 entries across 19 sections, and **twenty-three implementations pass every one of them** — `typescript/` (canonical), `go/`, `python/`, `javascript/`, `ruby/`, `php/`, `perl/`, `rust/`, `java/`, `lua/`, `csharp/`, `elixir/`, `clojure/`, diff --git a/DOCS.md b/DOCS.md index 5f336fc..ff1d555 100644 --- a/DOCS.md +++ b/DOCS.md @@ -482,7 +482,7 @@ in the same way. | `probe` | The workhorse. Records every callback it receives into the log, binds one hook point (`p`), wraps one chain point (`c`), holds an integer counter in its state, and **acquires exactly one synthetic resource per activation**. It exports three keys: `client`, its own ref; `mark`, the constant `marked`; and `inst`, its own instance api, which is how the `stray` command reaches `release` from *outside* a lifecycle callback. **`mark` is there so an entry can read a SECOND key off one instance** — every `export` entry once read `client`, so a port whose `exports` ignored the key and answered with the instance's first export passed all of them, and `inst` cannot close that because no entry can assert on an instance api. | | `noisy` | Fails on demand. `options.fail` names the callback that raises — `define`, `activate`, `deactivate` or `close` — and `options.code` the error code. `options.bare` raises with **no code at all**, which is the ordinary library error §12's `plugin__failed` codes exist to wrap. Everything else is `probe`. | | `greedy` | Acquires `options.acquire` resources on activation and releases `options.release` of them explicitly, so the difference is what the instance scope must unwind (§8.3). `options.early` acquires in **`define`** instead, where §8.1 says capture does not belong. `options.bind` names the callback (`activate` or `deactivate`) that declares a **binding** outside `define`, which is §8.1's other half and §12's `plugin_bind_scope`. `options.mark` additionally registers that many **foreign** releases through `release`, each recording its own index into `state.unwound` as it runs — which is the only way the *direction* of the unwind is observable, since an acquired handle is an idempotent counter decrement that reads the same either way. `options.markfail` makes each of those releases **raise**, which is the only way §8.3's `plugin_release_failed` and its `failed` status are reachable. | -| `dep` | Declares requirements. `options.requires` is a list of refs or capability names, `options.optional` those that are optional rather than mandatory. `options.capof` names one of them and exports the answer of `inst.capability` as `cap` — **the only way an entry can see the instance-side question at all**, since `host.capability` answers with the ranking rather than with the provider this instance took, and reluctant rebinding (§11.4) makes those differ. | +| `dep` | Declares requirements, and **acquires one synthetic resource per activation** like `probe` does. `options.requires` is a list of refs or capability names, `options.optional` those that are optional rather than mandatory. `options.capof` names one of them and exports the answer of `inst.capability` as `cap` — **the only way an entry can see the instance-side question at all**, since `host.capability` answers with the ranking rather than with the provider this instance took, and reluctant rebinding (§11.4) makes those differ. | | `provider` | Binds a provider point named by `options.point`, returning `options.value`. `options.version` and `options.priority` feed the selection rank. | | `slow` | Behaviourally `probe`, and **it does not yield.** It is here because §18 settles transitions eagerly — the host calls a callback and does not await it — and a callback that yields therefore does not "complete later", it silently abandons everything after its first suspension point. So the probe cannot demonstrate eager settling by yielding; it would only demonstrate that half a callback vanished. The name is kept, and the catalog keeps six definitions, because the question it was invented for is still open (see below). | diff --git a/README.md b/README.md index a7fce2c..a92fff0 100644 --- a/README.md +++ b/README.md @@ -26,7 +26,7 @@ programmatic API over the same normalized model. **P6 complete — six of six. Every planned port exists.** The design is complete and agreed with its first host, the contract is complete (all -19 corpus sections, 590 entries), and there are **twenty-three +19 corpus sections, 591 entries), and there are **twenty-three implementations**: `typescript/` the canonical, plus `go/`, `python/`, `javascript/`, `ruby/`, `php/`, `perl/`, `rust/`, `java/`, `lua/`, `csharp/`, `elixir/`, `clojure/`, `dart/`, `kotlin/`, `swift/`, @@ -73,7 +73,7 @@ testing found, not about what was there. |---|---| | design | complete — [`docs/design/plugin.md`](./docs/design/plugin.md) | | agreement with station | [reconciled](https://github.com/voxgig/station/blob/main/docs/design/station-and-plugin.md), and [sequenced](https://github.com/voxgig/station/blob/main/docs/design/station-and-plugin-plan.md) | -| corpus | **590 entries across all 19 sections** — the contract is complete | +| corpus | **591 entries across all 19 sections** — the contract is complete | | driver contract | [`DOCS.md`](./DOCS.md) §4 | | ports | **twenty-three, all passing every section** — `typescript/` (canonical), `go/`, `python/`, `javascript/`, `ruby/`, `php/`, `perl/`, `rust/`, `java/`, `lua/`, `csharp/`, `elixir/`, `clojure/`, `dart/`, `kotlin/`, `swift/`, `scala/`, `c/`, `cpp/`, `ocaml/`, `haskell/`, `zig/` and `lean/`. **No port work remains.** Next: P3.1's extraction (unblocked: station's Stages 2–3b merged). | diff --git a/c/test/driver.c b/c/test/driver.c index 66f09d7..6de1f04 100644 --- a/c/test/driver.c +++ b/c/test/driver.c @@ -237,12 +237,10 @@ static void dep_define(Inst *i) { } /* WHICH provider this instance took, when the entry asks. See - * typescript/test/driver.ts. - * - * `dep` has no `acquire` in this port and gains none here: the entries - * that read `cap` assert `result`, never `open`, so adding one would - * change what every other `dep` entry sees for nothing. */ + * typescript/test/driver.ts. The `acquire` is the canonical `dep`'s, + * and this port did not have it: `dep` had no `activate` at all. */ static void dep_activate(Inst *i) { + inst_acquire(i); Value *capof = opt(i, "capof"); if (!visstr(capof)) return; const char *picked = inst_capability(i, vasstr(capof)); diff --git a/cpp/test/driver.cpp b/cpp/test/driver.cpp index 3acd5fc..4ad4de9 100644 --- a/cpp/test/driver.cpp +++ b/cpp/test/driver.cpp @@ -186,12 +186,10 @@ static void depdefine(Inst& i) { } /* WHICH provider this instance took, when the entry asks. See - * typescript/test/driver.ts. - * - * `dep` has no `acquire` in this port and gains none here: the entries - * that read `cap` assert `result`, never `open`, so adding one would - * change what every other `dep` entry sees for nothing. */ + * typescript/test/driver.ts. The `acquire` is the canonical `dep`'s, + * and this port did not have it: `dep` had no `activate` at all. */ static void depactivate(Inst& i) { + i.acquire(); V capof = opt(i, "capof"); if (!isstr(capof)) return; i.exportvalue("cap", i.capability(asstr(capof))); diff --git a/doc/plan/progress.md b/doc/plan/progress.md index 95f2a8d..f85bc82 100644 --- a/doc/plan/progress.md +++ b/doc/plan/progress.md @@ -96,5 +96,5 @@ It did: see 4.1's note and [`handover.md`](handover.md) §13. | 6.3 Corpus gap 1: shape validation at REGISTRATION | **DONE** | `declare/shape` (7 entries) pins §10.1's TIMING, which `config/optmergebad` says in its own comment it cannot: every entry stops at `define`, so a port deferring the check to resolution raises nothing and fails. Two entries also pin that a valid shape is KEPT rather than validated and dropped, one that a rejected registration leaves nothing behind. **The gap was not cheap and §18's "cheap" was wrong about it**: nothing carried a `shape` because the driver's `define` was a NO-OP in all seventeen ports — a documented three-key verb (DOCS.md §4.2) that registered nothing — so `catalog.add`'s check was unreachable by construction and the `probe` key was ignored by the ten entries passing it. `define` is now implemented everywhere, all three keys live, and `declare/register` (3 entries) pins `probe` distinct from `name`. DOCS.md's "default is `probe`" was wrong and is corrected to `name`; the literal default would have re-backed every `dep`, `noisy` and `greedy` definition with the wrong probe. **Implementing it found a canonical bug**: `apply` handed its resolved options map to `declare`, which ADOPTS it, then refilled that map from itself — so a first-time `apply` left the instance with **no options at all**, and only a second identical apply filled them in. Every `apply` entry asserted status, log or open and none a value the options decide. Fixed in canonical, go, javascript, python, ruby, perl, lua, dart; php, java, csharp, kotlin, rust, swift, scala, elixir, clojure never had it. Three new `apply/idempotent` entries pin it. Corpus 539 -> 552; `make check` green in all seventeen. | | 6.7 Corpus gap 4: a second export key off ONE instance | **DONE** | `probe` now exports `mark`, the constant `marked`, beside `client` and `inst`; four entries read a second key (`export/key#second-key`, `#two-keys`, `#two-keys-reversed`, `export/alias#second-key`). **The gap as first written was overstated, and measuring it is what said so.** A port that IGNORED the key outright was already caught, by the absent-key entry `probe$a/nope`: ignoring the key makes a missing key present. What nothing could distinguish is a lookup that CHECKS the key is present and then answers with the instance's FIRST export — presence-checked, position-answered. Mutated both branches that way and measured: against the 572-entry corpus the exact branch left `export/key` and `export/alias` green (only `featurehost-bridge` and `resource/scope` failed, and both only because the DRIVER reads `exports(ref + '/inst')` for `stray`, which is not an entry asserting anything); the alias branch left the WHOLE suite green, 0 failures. Against 580 each is caught by its own group and nothing else. So a port could have got exports wrong and been told by a resource test, or not told at all. `inst` cannot close this — it is an instance api, shaped differently in every port, and no entry can assert on it; a constant can. 23 drivers, DOCS.md §4.3. Corpus 576 -> 580; all 23 ports green. | | 6.8 A scoped definition has no export spelling | **DONE** | Found by Codex's review of the DOCS.md how-to, and reproduced against the canonical. `resolveexport` splits an export spec at the FIRST `/`, so `@acme/store/admin` reads as the ref `@acme` with the key `store/admin` and answers `undefined`. §4's `checkname` permits `/` in a NAME, and `resolvecandidates` has a branch for scoped names resolving verbatim, so scoped definitions are a supported case with no way to read their exports. Nothing in `export` covers it: every entry there uses `probe`, which has no slash. **Closed by the last-`/` split**, canonical plus all 22 ports, and four `export/key` entries (`#scoped`, `#scoped-untagged`, `#scoped-alias`, and a scoped miss). The cost is stated in design §11 and DOCS.md: an export key may not contain `/`, because one separator cannot serve both and a name holds slashes because §4 says so. Four ports had no reverse search and take a documented workaround — lua walks forward keeping the last hit, elixir takes `List.last(:binary.matches ...)`, haskell and lean split the REVERSED string and put the halves back. Reverting the canonical to `indexOf` fails `export/key` and nothing else. Corpus 572 -> 576; all 23 ports green. | -| 6.9 §11.1's `inst.capability(name)` does not exist | **DONE** | Also from that review. The design said "the first is bound, and `inst.capability(name)` returns it", and the canonical instance api had no such method — `bind`, `export`, `provides`, `acquire`, `release`, `position`, `nest`, and no `capability`. **Implemented rather than struck**, because the question it asks is one the host cannot answer: `host.capability(name)` RANKS the live providers, and §11.4's reluctant rebinding means the instance keeps a provider a newcomer outranks, so the two answers part company exactly when it matters. It reaches `chosen` with `remember` TRUE — this is the instance asking, not introspection about it — and answers with a REF, so the API still travels as an export. Visible to the corpus only through the `dep` probe's new `options.capof`, which exports the answer as `cap`; without it no entry could reach an instance api. **The first four entries did not earn the method, and mutating it is what said so.** The selected one, rank deciding it, an optional requirement nobody provides, and a name this instance does not require: against those four, `host.capability(name)[0]` — the shortest wrong implementation there is, and the exact thing the method exists to not be — passed the whole 584-entry suite, and so did `requirements[0]`, which never reads the name. Both are now caught. `#by-ref` closes the first: §11.1 says a ref satisfies a requirement, and a ref is not a declared capability, so the instance answers `dep$p` where the host ranks nothing at all — `#by-ref-host-disagrees` is the same run asking the host. `#named-second` and `#named-first` close the second, and needed an instance with TWO satisfied requirements, which no other entry here has. `#reluctant` and `#reluctant-host-ranks` record §11.4 seen from outside — `dep$c` keeps `dep$lo` while the host ranks the newcomer `dep$hi` first — which is the divergence the design claims and nothing else in the corpus states. One thing stays unpinnable: `remember` true rather than false is invisible, because activation's own remember-all loop runs immediately after the callback that asks. Canonical plus all 22 ports, DOCS.md §2 and §4.3. Corpus 580 -> 590; all 23 ports green. | +| 6.9 §11.1's `inst.capability(name)` does not exist | **DONE** | Also from that review. The design said "the first is bound, and `inst.capability(name)` returns it", and the canonical instance api had no such method — `bind`, `export`, `provides`, `acquire`, `release`, `position`, `nest`, and no `capability`. **Implemented rather than struck**, because the question it asks is one the host cannot answer: `host.capability(name)` RANKS the live providers, and §11.4's reluctant rebinding means the instance keeps a provider a newcomer outranks, so the two answers part company exactly when it matters. It reaches `chosen` with `remember` TRUE — this is the instance asking, not introspection about it — and answers with a REF, so the API still travels as an export. Visible to the corpus only through the `dep` probe's new `options.capof`, which exports the answer as `cap`; without it no entry could reach an instance api. **The first four entries did not earn the method, and mutating it is what said so.** The selected one, rank deciding it, an optional requirement nobody provides, and a name this instance does not require: against those four, `host.capability(name)[0]` — the shortest wrong implementation there is, and the exact thing the method exists to not be — passed the whole 584-entry suite, and so did `requirements[0]`, which never reads the name. Both are now caught. `#by-ref` closes the first: §11.1 says a ref satisfies a requirement, and a ref is not a declared capability, so the instance answers `dep$p` where the host ranks nothing at all — `#by-ref-host-disagrees` is the same run asking the host. `#named-second` and `#named-first` close the second, and needed an instance with TWO satisfied requirements, which no other entry here has. `#reluctant` and `#reluctant-host-ranks` record §11.4 seen from outside — `dep$c` keeps `dep$lo` while the host ranks the newcomer `dep$hi` first — which is the divergence the design claims and nothing else in the corpus states. One thing stays unpinnable: `remember` true rather than false is invisible, because activation's own remember-all loop runs immediately after the callback that asks. **And writing the probe found a divergence of its own**: the canonical `dep` acquires one resource per activation and `c`, `cpp`, `ocaml`, `zig` and `lean` gave it no `activate` at all, which no entry could see because none with a live `dep` had ever asserted `open`. Fixed in all five, pinned by `#dep-holds`, documented in DOCS.md §4.3 — removing the `acquire` again fails that one entry and nothing else. Canonical plus all 22 ports, DOCS.md §2 and §4.3. Corpus 580 -> 591; all 23 ports green. | | 6.2 Does sdkgen adopt plugin? (§17.2) | DECISION NEEDED | Open, uncommitted, and carries a propagation cost across 23 template trees. Gates nested hosts *natively*, deletion of `transport`, and the seventeen-model change. | diff --git a/doc/plan/status.md b/doc/plan/status.md index b48d501..0b91fed 100644 --- a/doc/plan/status.md +++ b/doc/plan/status.md @@ -15,7 +15,7 @@ a wrong status file is worse than none.** **Nothing. P6 is complete — six of six — and no port work remains on the plan.** `c`, `cpp`, `ocaml`, `haskell`, `zig` and `lean` all landed, -so **twenty-three implementations pass all 590 corpus entries** and +so **twenty-three implementations pass all 591 corpus entries** and `make check` runs every one of them. **The six tier-4 ports are deliberately not one port six times**, and diff --git a/lean/test/Driver.lean b/lean/test/Driver.lean index ee9a261..4d913fc 100644 --- a/lean/test/Driver.lean +++ b/lean/test/Driver.lean @@ -150,12 +150,10 @@ def depDefine (i : InstApi) : PluginM Unit := do for k in exports.keys do i.exportValue k (exports.get k) /-- WHICH provider this instance took, when the entry asks. See -typescript/test/driver.ts. - -`dep` has no `acquire` in this port and gains none here: the entries -that read `cap` assert `result`, never `open`, so adding one would -change what every other `dep` entry sees for nothing. -/ +typescript/test/driver.ts. The `acquire` is the canonical `dep`'s, and +this port did not have it: `dep` had no `activate` at all. -/ def depActivate (i : InstApi) : PluginM Unit := do + let _ ← i.acquire let capof ← opt i "capof" if !capof.isStr then return match ← i.capability capof.asStr with diff --git a/ocaml/test/driver.ml b/ocaml/test/driver.ml index aa97838..ad6c541 100644 --- a/ocaml/test/driver.ml +++ b/ocaml/test/driver.ml @@ -206,12 +206,10 @@ let depdefine (i : inst) = List.iter (fun k -> Host.exportvalue i k (V.get exports k)) (V.keys exports) (* WHICH provider this instance took, when the entry asks. See - typescript/test/driver.ts. - - `dep` has no `acquire` in this port and gains none here: the entries - that read `cap` assert `result`, never `open`, so adding one would - change what every other `dep` entry sees for nothing. *) + typescript/test/driver.ts. The `acquire` is the canonical `dep`'s, + and this port did not have it: `dep` had no `activate` at all. *) let depactivate (i : inst) = + ignore (Host.acquire i); let capof = opt i "capof" in if V.is_str capof then Host.exportvalue i "cap" diff --git a/spec/plugin.aon b/spec/plugin.aon index 1886d82..a230691 100644 --- a/spec/plugin.aon +++ b/spec/plugin.aon @@ -3536,6 +3536,21 @@ primary: depend: { ] match: { out: { result: 'dep$lo' } } } + # AND `dep` HOLDS ONE RESOURCE PER ACTIVATION, like every other + # probe. Nothing said so: five ports gave `dep` no `activate` at + # all, and the corpus could not tell, because no entry with a live + # `dep` had ever asserted `open`. That is the probe catalog + # diverging silently, which is what DOCS.md §4.3 exists to stop. + { + id: 'depend/bound#dep-holds' + in: [ + { do: 'ready', ref: 'dep$p', definition: 'dep', options: { provides: [ { name: 'clock' } ] } } + { do: 'ready', ref: 'dep$c', definition: 'dep' + options: { requires: ['clock'], capof: 'clock' } } + { do: 'export', key: 'dep$c/cap' } + ] + match: { out: { result: 'dep$p', open: 2 } } + } { id: 'depend/bound#reluctant-host-ranks' in: [ diff --git a/spec/plugin.json b/spec/plugin.json index 6063680..e745400 100644 --- a/spec/plugin.json +++ b/spec/plugin.json @@ -5302,6 +5302,44 @@ } } }, + { + "id": "depend/bound#dep-holds", + "in": [ + { + "definition": "dep", + "do": "ready", + "options": { + "provides": [ + { + "name": "clock" + } + ] + }, + "ref": "dep$p" + }, + { + "definition": "dep", + "do": "ready", + "options": { + "capof": "clock", + "requires": [ + "clock" + ] + }, + "ref": "dep$c" + }, + { + "do": "export", + "key": "dep$c/cap" + } + ], + "match": { + "out": { + "open": 2, + "result": "dep$p" + } + } + }, { "id": "depend/bound#reluctant-host-ranks", "in": [ diff --git a/zig/test/driver.zig b/zig/test/driver.zig index 8e515a9..82a1fec 100644 --- a/zig/test/driver.zig +++ b/zig/test/driver.zig @@ -236,12 +236,10 @@ fn depDefine(i: *Inst) t.Err!void { } // WHICH provider this instance took, when the entry asks. See -// typescript/test/driver.ts. -// -// `dep` has no `acquire` in this port and gains none here: the entries -// that read `cap` assert `result`, never `open`, so adding one would -// change what every other `dep` entry sees for nothing. +// typescript/test/driver.ts. The `acquire` is the canonical `dep`'s, +// and this port did not have it: `dep` had no `activate` at all. fn depActivate(i: *Inst) t.Err!void { + _ = try host.acquire(i); const capof = opt(i, "capof"); if (!v.isStr(capof)) return; const picked = host.instcapability(i, v.asStr(capof)); From a38ab7d6b3dd3ebb81a60b47fa265acf28390542 Mon Sep 17 00:00:00 2001 From: Claude Date: Wed, 16 Sep 2026 11:44:32 +0000 Subject: [PATCH 9/9] ci: build the lean port with the compiler it pins `lean/lean-toolchain` moved to v4.32.1 in 48392f5, for the reason that commit gives: voxgig/struct's lean port and the sdkgen scaffold both pin it, and four repositories vendored together as one checkpoint cannot be compiled side by side on three different pins. This file still fetched v4.15.0, so CI compiled 4.32.1 sources with a compiler that predates the `String.Slice` changes 48392f5 was written for. `make build-lean` has failed on every run since, on `main` as well as on every branch, and it reads as a port failure rather than a toolchain mismatch: the three modules that fail are `Corpus`, `Plugin.Env` and `Plugin.Version`, on `String.dropEnd` and `String.toString` not existing. The comment now says the two must move together, so the next bump has one place to look. `doc/plan/progress.md` named the old asset and moves with it. `patch/` is gone, which is what applied looks like, and `tools/check_prose.py` drops the `patch` entry it needed while the folder was there. Verified: the v4.32.1 linux asset resolves at the URL this builds, and the port passes all 591 corpus entries under it locally. Co-Authored-By: Claude Opus 5 Claude-Session: https://claude.ai/code/session_01CVMgjjwQfTJ2rXz637Wpk8 --- .github/workflows/ci.yml | 7 +- doc/plan/progress.md | 2 +- ...-lean-port-with-the-compiler-it-pins.patch | 51 ----------- patch/README.md | 86 ------------------- tools/check_prose.py | 2 +- 5 files changed, 8 insertions(+), 140 deletions(-) delete mode 100644 patch/0001-ci-build-the-lean-port-with-the-compiler-it-pins.patch delete mode 100644 patch/README.md diff --git a/.github/workflows/ci.yml b/.github/workflows/ci.yml index 9994820..cb4d224 100644 --- a/.github/workflows/ci.yml +++ b/.github/workflows/ci.yml @@ -232,10 +232,15 @@ jobs: # The asset is `.tar.zst`; ubuntu-latest ships zstd, and the # explicit `--use-compress-program` says so rather than relying on # tar's suffix detection. + # + # THE VERSION HERE MUST MATCH `lean/lean-toolchain`. When they + # drifted the job failed on `make build-lean`, compiling the + # port's sources with an older compiler — which reads as a port + # failure and is not one. - if: matrix.port == 'lean' run: | curl -fsSL -o /tmp/lean.tar.zst \ - https://github.com/leanprover/lean4/releases/download/v4.15.0/lean-4.15.0-linux.tar.zst + https://github.com/leanprover/lean4/releases/download/v4.32.1/lean-4.32.1-linux.tar.zst sudo mkdir -p /opt/lean sudo tar --use-compress-program=unzstd -xf /tmp/lean.tar.zst \ -C /opt/lean --strip-components=1 diff --git a/doc/plan/progress.md b/doc/plan/progress.md index f85bc82..316fc2b 100644 --- a/doc/plan/progress.md +++ b/doc/plan/progress.md @@ -92,7 +92,7 @@ It did: see 4.1's note and [`handover.md`](handover.md) §13. | 6.4 Corpus gap 2: `providersof` without `canon` | **DONE** | `depend/byref`, 5 entries, no port change — all seventeen already agreed, which is what a COVERAGE gap rather than a divergence looks like. **Wider than its name.** The claim in §18 was that "§11.1 lets a REF satisfy a requirement" and only the canonicalization was unpinned. §11.1 said the opposite — "a dependency is on a capability, not on a ref" — and the exception lived nowhere but a comment in the canonical's `unmetof`. Replacing the whole branch with `if (false)` passed all 552 entries, so seventeen ports carried the behaviour because they copied the canonical, not because anything checked. Design §11.1 now states the rule, narrow and with its reason. The entries pin that a live ref satisfies, that `loaded` and `declared` do not, that losing it cascades — and the canonicalizing comparison, reachable only as `dep$` against `dep`, a trailing `$` parsing to the empty tag being the sole way two spellings of one ref can differ (§4). Both mutants (drop `canon`; delete the branch) die in this group and nowhere else. | | 6.5 Corpus gap 3: `nest` counting the inner host as open | **DONE** | `nest/open`, 4 entries, no port change. §6.5 puts the inner host's teardown in the outer instance's scope; whether that ALSO incremented `open` was free, because the three existing `nest` entries asserted `result` and `status` and never `open`. It counts nothing — a teardown is not an acquisition, and the inner host keeps its own counter. Pinned: a nested outer reports the same `open` as an unnested one, the count does not scale with the inner host's contents (two inner instances, still 1), and it unwinds to zero. A mutant incrementing `open` on `nest` dies in this group alone. Corpus 552 -> 561. | | 6.6 The ref rule, everywhere the graph is examined | **DONE** | Codex's review of the gap-2 PR said the close was premature, and it was right — for a reason larger than the finding. §11.1 says a ref satisfies a requirement, and THREE places read a requirement name: runtime `providersof`, load-time `dependencycycle`, and whole-graph `resolve`. Only the first implemented the rule. **Four canonical defects, all now fixed and pinned.** (a) `providersof` canonicalized EVERY requirement name, so a capability called `2fa` or `my cap` — both legal, since §4's grammar is on plugin names and the design puts none on capability names — raised `plugin_bad_name` and killed a legal document; every capability name in the corpus happened to be a well-formed ref, and nine ports had independently worked around it with a try/except or a tolerant `canon`, so the canonical was the outlier and nothing caught it. (b) `dependencycycle` indexed providers by canonical ref and looked them up with the raw name, so the same cycle spelled `dep$`/`other$` produced no edges and EVADED the load-time check entirely. (c) `graph.candidates` never considered node refs at all, so `resolve()` answered `absent` about a provider the runtime binds — even in the canonical spelling. (d) The design text asserted ref loss always sends a consumer to `pending`; it follows the ordinary cardinality/policy rules, so mandatory-`dynamic` stays live and optional never gated. Canonical gains a tolerant `tryref`; every port uses its own existing tolerant spelling. Eleven new entries across `depend/byref`, `depend/cycle` and `graph/resolve`+`blocked`; each targeted mutant fails its group and no other. Corpus 561 -> 572. | -| 6.1 Six tier-4 ports | **DONE (6/6)** | `c`, `cpp`, `ocaml`, `haskell`, `zig`, `lean` — all six pass all 572 entries, and **twenty-three implementations now do**. Toolchains all reachable: gcc/g++ 13.3.0 present, ghc 9.4.7 and ocaml 4.14.1 from apt, zig 0.13.0 from a ziglang.org tarball, lean 4.15.0 from a pinned GitHub release asset. **The six are deliberately not one port six times**, and §10.3's "tier-4" turned out to describe the LOADER, not the language: it says nothing about closures, exceptions or a garbage collector, and those three are what a port actually costs. `c` builds all three by hand (arena, setjmp/longjmp — safe *because* of the arena — and `volatile` on every local straddling a try, seven of which `-Wclobbered` found); `cpp`, `ocaml` and `haskell` use what their languages have and need none of it; `zig` has none of them and needed a fourth answer. **What each one found is in handover.md §19.** Four defects the corpus caught between them: `point/bail#null-declines` wants PRESENCE not non-null; `resource/scope#difference` wants an early-release handle; `cpp` inherited `c`'s POSIX-ERE regex dialect for the corpus `match` patterns, which are JavaScript literals; and `ocaml` found that a bad number must be a reported error, not a crash, or §9.5's parse-or-string fallback cannot catch it. **Two the corpus could NOT catch**: `check_probes.py` had no `c` row, so it reported `c` green without opening a file; and the `provider` probe carried a dead capability record in `c`, `cpp` and `ocaml` that haskell nearly turned into a real divergence — the lesson being *check the canonical, not the nearest port*. **Two languages refused the shape outright**, which is the durable finding: zig's errors carry no payload, so the diagnostic travels beside the error and every handler takes it first; and **Lean's kernel rejects the definition↔instance cycle every other port takes for granted** (`non positive occurrence of the datatypes being declared`), so the instance api became an explicit record of closures — which is what §6 says a plugin may touch anyway. | +| 6.1 Six tier-4 ports | **DONE (6/6)** | `c`, `cpp`, `ocaml`, `haskell`, `zig`, `lean` — all six pass all 572 entries, and **twenty-three implementations now do**. Toolchains all reachable: gcc/g++ 13.3.0 present, ghc 9.4.7 and ocaml 4.14.1 from apt, zig 0.13.0 from a ziglang.org tarball, lean 4.32.1 from a pinned GitHub release asset. **The six are deliberately not one port six times**, and §10.3's "tier-4" turned out to describe the LOADER, not the language: it says nothing about closures, exceptions or a garbage collector, and those three are what a port actually costs. `c` builds all three by hand (arena, setjmp/longjmp — safe *because* of the arena — and `volatile` on every local straddling a try, seven of which `-Wclobbered` found); `cpp`, `ocaml` and `haskell` use what their languages have and need none of it; `zig` has none of them and needed a fourth answer. **What each one found is in handover.md §19.** Four defects the corpus caught between them: `point/bail#null-declines` wants PRESENCE not non-null; `resource/scope#difference` wants an early-release handle; `cpp` inherited `c`'s POSIX-ERE regex dialect for the corpus `match` patterns, which are JavaScript literals; and `ocaml` found that a bad number must be a reported error, not a crash, or §9.5's parse-or-string fallback cannot catch it. **Two the corpus could NOT catch**: `check_probes.py` had no `c` row, so it reported `c` green without opening a file; and the `provider` probe carried a dead capability record in `c`, `cpp` and `ocaml` that haskell nearly turned into a real divergence — the lesson being *check the canonical, not the nearest port*. **Two languages refused the shape outright**, which is the durable finding: zig's errors carry no payload, so the diagnostic travels beside the error and every handler takes it first; and **Lean's kernel rejects the definition↔instance cycle every other port takes for granted** (`non positive occurrence of the datatypes being declared`), so the instance api became an explicit record of closures — which is what §6 says a plugin may touch anyway. | | 6.3 Corpus gap 1: shape validation at REGISTRATION | **DONE** | `declare/shape` (7 entries) pins §10.1's TIMING, which `config/optmergebad` says in its own comment it cannot: every entry stops at `define`, so a port deferring the check to resolution raises nothing and fails. Two entries also pin that a valid shape is KEPT rather than validated and dropped, one that a rejected registration leaves nothing behind. **The gap was not cheap and §18's "cheap" was wrong about it**: nothing carried a `shape` because the driver's `define` was a NO-OP in all seventeen ports — a documented three-key verb (DOCS.md §4.2) that registered nothing — so `catalog.add`'s check was unreachable by construction and the `probe` key was ignored by the ten entries passing it. `define` is now implemented everywhere, all three keys live, and `declare/register` (3 entries) pins `probe` distinct from `name`. DOCS.md's "default is `probe`" was wrong and is corrected to `name`; the literal default would have re-backed every `dep`, `noisy` and `greedy` definition with the wrong probe. **Implementing it found a canonical bug**: `apply` handed its resolved options map to `declare`, which ADOPTS it, then refilled that map from itself — so a first-time `apply` left the instance with **no options at all**, and only a second identical apply filled them in. Every `apply` entry asserted status, log or open and none a value the options decide. Fixed in canonical, go, javascript, python, ruby, perl, lua, dart; php, java, csharp, kotlin, rust, swift, scala, elixir, clojure never had it. Three new `apply/idempotent` entries pin it. Corpus 539 -> 552; `make check` green in all seventeen. | | 6.7 Corpus gap 4: a second export key off ONE instance | **DONE** | `probe` now exports `mark`, the constant `marked`, beside `client` and `inst`; four entries read a second key (`export/key#second-key`, `#two-keys`, `#two-keys-reversed`, `export/alias#second-key`). **The gap as first written was overstated, and measuring it is what said so.** A port that IGNORED the key outright was already caught, by the absent-key entry `probe$a/nope`: ignoring the key makes a missing key present. What nothing could distinguish is a lookup that CHECKS the key is present and then answers with the instance's FIRST export — presence-checked, position-answered. Mutated both branches that way and measured: against the 572-entry corpus the exact branch left `export/key` and `export/alias` green (only `featurehost-bridge` and `resource/scope` failed, and both only because the DRIVER reads `exports(ref + '/inst')` for `stray`, which is not an entry asserting anything); the alias branch left the WHOLE suite green, 0 failures. Against 580 each is caught by its own group and nothing else. So a port could have got exports wrong and been told by a resource test, or not told at all. `inst` cannot close this — it is an instance api, shaped differently in every port, and no entry can assert on it; a constant can. 23 drivers, DOCS.md §4.3. Corpus 576 -> 580; all 23 ports green. | | 6.8 A scoped definition has no export spelling | **DONE** | Found by Codex's review of the DOCS.md how-to, and reproduced against the canonical. `resolveexport` splits an export spec at the FIRST `/`, so `@acme/store/admin` reads as the ref `@acme` with the key `store/admin` and answers `undefined`. §4's `checkname` permits `/` in a NAME, and `resolvecandidates` has a branch for scoped names resolving verbatim, so scoped definitions are a supported case with no way to read their exports. Nothing in `export` covers it: every entry there uses `probe`, which has no slash. **Closed by the last-`/` split**, canonical plus all 22 ports, and four `export/key` entries (`#scoped`, `#scoped-untagged`, `#scoped-alias`, and a scoped miss). The cost is stated in design §11 and DOCS.md: an export key may not contain `/`, because one separator cannot serve both and a name holds slashes because §4 says so. Four ports had no reverse search and take a documented workaround — lua walks forward keeping the last hit, elixir takes `List.last(:binary.matches ...)`, haskell and lean split the REVERSED string and put the halves back. Reverting the canonical to `indexOf` fails `export/key` and nothing else. Corpus 572 -> 576; all 23 ports green. | diff --git a/patch/0001-ci-build-the-lean-port-with-the-compiler-it-pins.patch b/patch/0001-ci-build-the-lean-port-with-the-compiler-it-pins.patch deleted file mode 100644 index 960410d..0000000 --- a/patch/0001-ci-build-the-lean-port-with-the-compiler-it-pins.patch +++ /dev/null @@ -1,51 +0,0 @@ -From 2933087df413a3dfa21b13f2dda6aee8bb29b0c1 Mon Sep 17 00:00:00 2001 -From: Claude -Date: Wed, 16 Sep 2026 10:26:45 +0000 -Subject: [PATCH] ci: build the lean port with the compiler it pins - -`lean/lean-toolchain` moved to v4.32.1 in 48392f5, for the reason that -commit gives: voxgig/struct's lean port and the sdkgen scaffold both pin -it, and four repositories vendored together as one checkpoint cannot be -compiled side by side on three different pins. - -This file still fetched v4.15.0, so CI compiled 4.32.1 sources with a -compiler that predates the `String.Slice` changes 48392f5 was written -for. `make build-lean` has failed on every run since, on `main` as well -as on every branch, and it reads as a port failure rather than a -toolchain mismatch. - -An agent session cannot write `.github/workflows/`, which is why the -port's bump landed without this. The comment now says the two must move -together, so the next bump has one place to look. - -Verified: the v4.32.1 linux asset resolves at the URL this builds. ---- - .github/workflows/ci.yml | 9 ++++++++- - 1 file changed, 8 insertions(+), 1 deletion(-) - -diff --git a/.github/workflows/ci.yml b/.github/workflows/ci.yml -index 9994820..36ec2c2 100644 ---- a/.github/workflows/ci.yml -+++ b/.github/workflows/ci.yml -@@ -232,10 +232,17 @@ jobs: - # The asset is `.tar.zst`; ubuntu-latest ships zstd, and the - # explicit `--use-compress-program` says so rather than relying on - # tar's suffix detection. -+ # -+ # THE VERSION HERE MUST MATCH `lean/lean-toolchain`, and an agent -+ # session cannot edit this file, so the two move in separate -+ # changes and the port's own bump lands first. When they drifted -+ # the job failed on `make build-lean` with the port's sources and -+ # the workflow's older compiler, which reads as a port failure and -+ # is not one. - - if: matrix.port == 'lean' - run: | - curl -fsSL -o /tmp/lean.tar.zst \ -- https://github.com/leanprover/lean4/releases/download/v4.15.0/lean-4.15.0-linux.tar.zst -+ https://github.com/leanprover/lean4/releases/download/v4.32.1/lean-4.32.1-linux.tar.zst - sudo mkdir -p /opt/lean - sudo tar --use-compress-program=unzstd -xf /tmp/lean.tar.zst \ - -C /opt/lean --strip-components=1 --- -2.43.0 - diff --git a/patch/README.md b/patch/README.md deleted file mode 100644 index 419fc18..0000000 --- a/patch/README.md +++ /dev/null @@ -1,86 +0,0 @@ -# `patch/` — a change this session could not push - -`.github/workflows/` is refused to the session that wrote this change, on -both write paths: - -- **git push** — `refusing to allow an OAuth App to create or update workflow - .github/workflows/ci.yml without workflow scope` -- **the GitHub App's file API** — fails on that path while writing any other - file in the same breath - -The change is a workflow change, so it cannot travel as a branch. It travels -as a patch instead, and this folder is transient: delete it once the patch is -applied. - -## Apply it - -From any checkout that carries this folder — this branch, or `main` once the -delivery commit is merged: - -```sh -git am patch/0001-ci-build-the-lean-port-with-the-compiler-it-pins.patch -``` - -Read it from the worktree rather than from a branch ref: the source branch is -usually deleted after merging and a fresh clone never had it, so a command -naming that branch would fail exactly when it is most likely to be run. If you -would rather not check the branch out, name a ref that outlives it: - -```sh -git show origin/main:patch/0001-ci-build-the-lean-port-with-the-compiler-it-pins.patch | git am -``` - -## What it does - -One line, plus the comment that explains it. - -| | version | -|---|---| -| `lean/lean-toolchain` | `leanprover/lean4:v4.32.1` | -| `.github/workflows/ci.yml`, before | `v4.15.0` | -| `.github/workflows/ci.yml`, after | `v4.32.1` | - -## Why it is worth doing - -**The `lean` job has failed on every run since `48392f5`**, including every -run on `main`. That commit moved the port to 4.32.1, for the reason it gives: -voxgig/struct's lean port and the sdkgen scaffold both pin it, and four -repositories vendored together as one checkpoint cannot be compiled side by -side on three different pins. The workflow kept fetching 4.15.0, so CI -compiles 4.32.1 sources with a compiler that predates the `String.Slice` -changes the port was rewritten for. - -It fails at `make build-lean`, which reads as a port failure and is not one. -Anyone reading a red `lean` check on their own branch learns nothing true -about their change. - -The port's bump landed without this file because an agent session cannot write -it — the same boundary this folder exists for. The comment added above the -step now says the two versions must move together, so the next bump has one -place to look. - -## Checks - -**Both compilers were fetched and the port built under each**, so the -failure this fixes is reproduced rather than inferred. - -``` -v4.15.0 make build-lean - Some required builds logged failures: - - Corpus - - Plugin.Env - - Plugin.Version - error: build failed - -v4.32.1 make build-lean clean - make test-lean 572 corpus entries across 19 sections, all pass -``` - -- `git apply --check` of this patch onto `5c1df34`: clean -- `.github/workflows/ci.yml` parses as YAML after applying, four jobs: - `spec-freshness`, `parity`, `port`, `newer-toolchain` -- the v4.32.1 linux asset resolves at the URL the job builds: - `https://github.com/leanprover/lean4/releases/download/v4.32.1/lean-4.32.1-linux.tar.zst` - -The lean port itself is not touched and needs nothing. What this restores -is CI's ability to say so. diff --git a/tools/check_prose.py b/tools/check_prose.py index 53a4931..85fc6de 100755 --- a/tools/check_prose.py +++ b/tools/check_prose.py @@ -82,7 +82,7 @@ # reader-facing page. It predates this gate, which is why the gate had # never met one and called it a twenty-fourth port. PORT_DIRS = True -NOT_PORTS = ("doc", "docs", "patch", "spec", "test", "tools", "node_modules") +NOT_PORTS = ("doc", "docs", "spec", "test", "tools", "node_modules") PORT_PAGES = ("README.md",) # Where "we" is allowed: the tutorial. There is no tutorial PAGE here;