docs: how to expose a programmatic API, and the three gaps writing it found

[rjrodger]

A plugin can offer an application values of its own, and it always
could. §11's exports are read back with host.exports('<ref>/<key>'), 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. The
application-facing half appears in the design and in the reference table,
and nowhere as a how-to — so the question arrived from
sekreto as though the mechanism were
missing. It is not, and the answer to it needed no code.

Writing the how-to turned up three gaps, though, and this PR closes all
three, plus a fourth found while closing them. The corpus goes 572 -> 591
and every one of the 23 ports is green on it.

The how-to

DOCS.md §2 gains Expose a programmatic API, between Depend on
something and Hold a resource:

• inst.export(key, value) in define, host.exports('<ref>/<key>') to
  read it back
• a definition may publish as many exports as it likes, and the usual
  shape is two: one the host or its framework consumes, one the
  application does
• the unqualified alias, which filters by key before tag, and why it
  raises rather than picking one
• exports of a loaded instance are visible (export/key#loaded-visible
  pins it), and the getter convention for a value that only means
  something while live
• a capability is declared beside an export, never instead of one:
  inst.provides records selection metadata and host.capability(name)
  answers with refs, so neither carries a callable value
• the consuming half — inst.capability(name) for the provider this
  instance took, paired with host.exports(ref + '/key') to reach it

The worked example is sekreto's mini vault
(voxgig/sekreto#31), which
exports provider for the chain and vault for the application from one
define.

6.7 — every export entry read the key client

Seven reads of one key, plus one absent key. probe exported two keys
(client, and its own inst), and nothing read the second — but inst
is an instance api, shaped differently in every port, so no entry can
assert on it. probe now exports mark, the constant marked, and four
entries read a 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: 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 572-entry suite green — 0 failures. Against
the new entries each mutation is caught by its own group.

6.8 — a scoped definition had no export spelling

resolveexport split at the first /, so @acme/store/admin read as
the ref @acme with the key store/admin and answered undefined. §4's
checkname permits / in a name and resolvecandidates resolves a
scoped name verbatim, so scoped definitions were a supported case with no
way to read their exports. No export entry could see it: all of them
use probe, which has no slash.

Closed by splitting at the last /, canonical plus all 22 ports,
with four new export/key entries. The cost is stated in the design and
in 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
have no reverse search and take a documented workaround. Reverting the
canonical to indexOf fails export/key and nothing else.

6.9 — §11.1's inst.capability(name) did not exist

The design said "the first is bound, and inst.capability(name) returns
it", and the instance api had no such method. 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 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.

The first four entries did not earn the method, and mutating it is what
said so. Against them, 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 where the host ranks nothing), #named-first and
#named-second need an instance with two satisfied requirements, and
#reluctant plus #reluctant-host-ranks record the divergence the
design claims and nothing else stated. remember true rather than false
stays unpinnable, and the register says so.

A fourth, found while closing the third

Giving dep an activate meant reading the canonical's, which acquires
one synthetic resource per activation. c, cpp, ocaml, zig and
lean gave dep no activate at all — five of twenty-three ports where
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 diverged in silence. Fixed in all five, pinned by #dep-holds,
and DOCS.md §4.3 now says dep holds. Taking the acquire back out of
any one of them fails that entry and nothing else.

The lean CI job, fixed here

lean was red on this branch and red on main: the port pins Lean
v4.32.1 and ci.yml still fetched v4.15.0, so CI compiled the port's
sources with a compiler that predates the String.Slice changes
48392f5 was written for. The three modules that failed — Corpus,
Plugin.Env, Plugin.Version — are files this branch never touches.

a38ab7d bumps the asset to v4.32.1 and adds the comment saying the two
pins move together. lean is green on this branch now, and so are
the other 27 checks.

An earlier comment on this PR said an agent session cannot write
.github/workflows/ and delivered the change as a patch/ folder
instead. The push went through this time, so the folder is gone — which
is what applied looks like — and tools/check_prose.py drops the
patch entry it needed while it was there.

The review round

Codex found six things. Five were real and are fixed in 5c1df34: the
capability sentence above, the alias being key-specific, a { read: store.read } example that loses its receiver, the first-/ limit, and
the export/key#loaded-visible citation. The sixth cited a rule that
does not exist — AGENTS.md L247-255 is §5c, the prose gate, and says
nothing about behaviour statements naming their corpus entry. The change
was made anyway, on its merits, and the reply says the citation was
false. 6.8 and 6.9 both came out of that review.

Checks

All 28 CI checks green. Locally make check exits 0: all 23 ports pass
591 entries, and make spec-check, make parity, make probes, make versions and make scan-prose (vale 3.14.0 + check_prose, 19 pages) all
pass. Every toolchain was installed and run locally rather than asserted.

🤖 Generated with Claude Code

https://claude.ai/code/session_01CVMgjjwQfTJ2rXz637Wpk8

[chatgpt-codex-connector]

Codex Review Summary

This comment shows the latest Codex review activity on this pull request.

Review	Status	Commit	Review trigger
📝 Code Review	✅ Completed 2026-09-16T08:58:14.177127Z	fbc1638	PR opened

ℹ️ About Codex in GitHub

Your team has set up Codex to review pull requests in this repo. Reviews are triggered when you

• Open a pull request for review
• Mark a draft as ready
• Comment "@codex review" or "@codex security review".

Codex reacts with 👀 while any review is running, comments if it has suggestions, and reacts with 👍 once all reviews finish with no findings.

[rjrodger]

lean is red, and it is not this PR's

lean fails at make build-lean. It is red on main too — the base tip
this branch came from,
91c4936,
and the run before it,
48392f5,
which is the commit that caused it. This PR changes three Markdown files
and nothing a compiler reads.

Root cause: the port and the workflow pin different Lean versions.

	version
lean/lean-toolchain	leanprover/lean4:v4.32.1
.github/workflows/ci.yml	v4.15.0

48392f5 moved the port to 4.32.1 for the reason its message gives — four
repositories are vendored together as one checkpoint and cannot be
compiled side by side on three different pins. The workflow still fetches
the 4.15.0 release asset, so CI builds 4.32.1 sources with a toolchain
that predates the String.Slice changes that commit was written for.
doc/plan/status.md still names 4.15.0 as the pinned asset, for the same
reason.

Why the workflow was not moved with it: an agent session cannot write
.github/workflows/. Both write paths refuse the path — git push rejects
the ref without workflow scope, and the App's file API fails on that path
alone. That is stated in AGENTS.md §5b, and it is why the port's bump
landed without its workflow counterpart.

The fix, for someone who can push a workflow:

--- a/.github/workflows/ci.yml
+++ b/.github/workflows/ci.yml
       - 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

Two lines nearby also name the old version and should move with it: the
comment above the step, and the lean 4.15.0 from a pinned GitHub *release asset* note in doc/plan/status.md.

I have not opened a patch/ folder for it. §5b's convention is that a
workflow change arrives as its own delivery, and putting an unrelated one
on a documentation PR would widen this PR rather than deliver that fix.
It wants its own branch.

No re-run: the mismatch is deterministic, so a second attempt fetches the
same 4.15.0 asset and fails the same way. Nothing here blocks this PR's
own content, and the prose gate — which was this PR's, and was real — is
fixed in b111106.

---

Generated by Claude Code

[chatgpt-codex-connector]

💡 Codex Review

Here are some automated review suggestions for this pull request.

Reviewed commit: fbc1638363

ℹ️ About Codex in GitHub

Your team has set up Codex to review pull requests in this repo. Reviews are triggered when you

• Open a pull request for review
• Mark a draft as ready
• Comment "@codex review".

If Codex has suggestions, it will comment; otherwise it will react with 👍.

Codex can also answer questions or update the PR. Try commenting "@codex address that feedback".

[rjrodger]

Correction to the lean comment above: the patch is here now

Two things in that comment have gone stale.

The patch/ folder exists. I said it wanted its own branch and I had
not opened one. Since then the PR grew from three Markdown files into the
change set that closes register rows 6.7, 6.8 and 6.9 — which touches
every port including lean, so the fix is no longer unrelated to this
PR, it is what lets CI check lean's share of it. It landed in
022464c as
patch/0001-ci-build-the-lean-port-with-the-compiler-it-pins.patch, with
a patch/README.md, per AGENTS.md §5b. Applying it is
git am patch/0001-*.patch from someone with workflow scope.

"Nothing a compiler reads" no longer holds. It does now. The
diagnosis stands unchanged though, and today's run says so directly: the
three modules that fail — Corpus, Plugin.Env, Plugin.Version — are
files this branch never touches, and they fail on String.dropEnd and
String.toString not existing, which is 4.15.0 lacking what 4.32.1 has.

Locally, under the 4.32.1 the port pins, lean compiles 18 modules and
passes all 591 corpus entries, the same as the other twenty-two ports.

Still no re-run: the mismatch is deterministic and a second attempt
fetches the same 4.15.0 asset.

---

Generated by Claude Code