A small reitit-ring web browser over a KB:
/ the upper ontology (contexts, types, core predicates, disjointness) /stats KB-wide counts, contexts by size, and the reasoning-health ledgers /find?q=<pattern> the terms whose name matches, from the index's term roster /term?q=<term> every sentex containing the term, grouped by the index root that reaches it (functor / argument-position / context / term-index) /sentex/:id a sentex (atomic or rule): its belief state (IN, or the why-not reason — superseded / defeated / unsupported), supports, dependents /justification/:id a justification: its supports (arguments) and dependent sentex /levels?q=<goal> the lookup-to-query stack: what each of the 8 levels answers /edit the multi-sentex editor (GET seeds it, POST saves) — a fragment /{term,find,levels}/rows one more page of a capped list, as bare rows
Run it with lein run -m vaelii.impl.web (serves a starter-loaded KB on :3000).
Handlers are pure request -> response, so they are testable without a server.
Every page is answered twice over: as a whole document, and — when htmx asks, which
is every navigation and search — as the #main fragment that actually lands. What a
page costs in KB reads is part of what this demonstrates, since the browser reads the
public surface alone and each read is a round-trip under --attach; see the view
section below and docs/web.md.
A small reitit-ring web browser over a KB:
/ the upper ontology (contexts, types, core predicates, disjointness)
/stats KB-wide counts, contexts by size, and the reasoning-health ledgers
/find?q=<pattern> the terms whose name matches, from the index's term roster
/term?q=<term> every sentex containing the term, grouped by the index root that
reaches it (functor / argument-position / context / term-index)
/sentex/:id a sentex (atomic or rule): its belief state (IN, or the why-not
reason — superseded / defeated / unsupported), supports, dependents
/justification/:id a justification: its supports (arguments) and dependent sentex
/levels?q=<goal> the lookup-to-query stack: what each of the 8 levels answers
/edit the multi-sentex editor (GET seeds it, POST saves) — a fragment
/{term,find,levels}/rows one more page of a capped list, as bare rows
Run it with `lein run -m vaelii.impl.web` (serves a starter-loaded KB on :3000).
Handlers are pure `request -> response`, so they are testable without a server.
Every page is answered twice over: as a whole document, and — when htmx asks, which
is every navigation and search — as the `#main` fragment that actually lands. What a
page costs in KB reads is part of what this demonstrates, since the browser reads the
public surface alone and each read is a round-trip under `--attach`; see the `view`
section below and docs/web.md.The model a proposal runs against, as {:kind <keyword> :provider <Provider>}, or nil
— the default — to resolve the configured backend per request. A caller binds it to
drive the panel against a scripted provider without a model, which is how the handlers
below stay testable as pure request -> response like the rest of this namespace.
The model a proposal runs against, as `{:kind <keyword> :provider <Provider>}`, or nil
— the default — to resolve the configured backend per request. A caller binds it to
drive the panel against a scripted provider without a model, which is how the handlers
below stay testable as pure `request -> response` like the rest of this namespace.(-main & args)Serve the browser.
lein run -m vaelii.impl.web ; a fresh starter-loaded in-process KB lein run -m vaelii.impl.web --port 8080 lein run -m vaelii.impl.web --listen 0.0.0.0 ; reachable off-machine (opt-in) lein run -m vaelii.impl.web --attach HOST PORT [WEBPORT]
--attach points the browser at a running daemon (vaelii.impl.serve) and renders
the KB it owns over the API — the way to inspect a live daemon whose single-writer
lock forbids opening its store directly (docs/operations.md). Every page reads the
same, since app is written against the access facade (v), which dispatches each
read to the local KB or the remote daemon.
The KB it reads and the interface it binds are independent axes: --listen says who
may reach the browser, --attach says whose KB it shows. The default is loopback —
/edit writes and nothing authenticates it, so a public bind is a deliberate act.
Whichever KB it starts on is registered with the catalog and made active, so it
appears in /kbs beside the ones that can be loaded — the starter it opens with is not
a special case, it is entry number one.
Serve the browser. lein run -m vaelii.impl.web ; a fresh starter-loaded in-process KB lein run -m vaelii.impl.web --port 8080 lein run -m vaelii.impl.web --listen 0.0.0.0 ; reachable off-machine (opt-in) lein run -m vaelii.impl.web --attach HOST PORT [WEBPORT] `--attach` points the browser at a running daemon (`vaelii.impl.serve`) and renders the KB it owns *over the API* — the way to inspect a live daemon whose single-writer lock forbids opening its store directly (docs/operations.md). Every page reads the same, since `app` is written against the access facade (`v`), which dispatches each read to the local KB or the remote daemon. The KB it reads and the interface it binds are independent axes: `--listen` says who may reach the browser, `--attach` says whose KB it shows. The default is loopback — `/edit` writes and nothing authenticates it, so a public bind is a deliberate act. Whichever KB it starts on is **registered with the catalog** and made active, so it appears in `/kbs` beside the ones that can be loaded — the starter it opens with is not a special case, it is entry number one.
(app target)The ring handler for a KB. Pure request -> response.
target is what each page reads: a KB, an access value (v/local / v/remote), or a
holder — anything deref-able, yielding whichever of those is current
(vaelii.impl.catalog/holder). A holder is what makes the KB switchable: every
handler resolves it per request, so activating another entry re-points the whole
browser without rebuilding the handler.
The ring handler for a KB. Pure `request -> response`. `target` is what each page reads: a KB, an access value (`v/local` / `v/remote`), or a **holder** — anything deref-able, yielding whichever of those is current (`vaelii.impl.catalog/holder`). A holder is what makes the KB switchable: every handler resolves it per request, so activating another entry re-points the whole browser without rebuilding the handler.
(assert-page view)(assert-page {:keys [kb sandbox] :as view} state result)The new-sentex page: the form, and — after a save — what it stored.
The new-sentex page: the form, and — after a save — what it stored.
(assert-post {:keys [kb sandbox] :as view}
{:keys [text ctx monotonic?] :as state})Assert what the new-sentex form holds: read the lines, check them all against the
KB, and — only when every one is admissible — apply them in one edit. Nothing
partial is ever written: a form with one bad line stores none of it, which is what
makes the page safe to retry.
Assert what the new-sentex form holds: read the lines, check them all against the KB, and — only when every one is admissible — apply them in one `edit`. Nothing partial is ever written: a form with one bad line stores none of it, which is what makes the page safe to retry.
(current target)The KB a request reads. A holder (anything deref-able —
vaelii.impl.catalog/holder) yields whichever KB is active right now; a KB or an
access value is itself. Every handler goes through here, which is what lets the
browser switch KBs under a running server.
The KB a request reads. A **holder** (anything deref-able — `vaelii.impl.catalog/holder`) yields whichever KB is active right now; a KB or an access value is itself. Every handler goes through here, which is what lets the browser switch KBs under a running server.
(default-page {:keys [kb types] :as view})(demo-apply kb sandbox op first-h)Do one step's write, and answer the first-handle to carry forward.
Split from the rendering because the page has to be built from a view taken after the write: whether the sandbox exists is a per-request read, and step 1 is the request that brings it into being.
Both adding steps open the sandbox first. Without its genlContext edge the sandbox
sees no shipped context, so BiologyContext's flight rule would not be visible from it
and the write would derive nothing at all — the demo would quietly do nothing rather
than fail.
Do one step's write, and answer the `first`-handle to carry forward. Split from the rendering because the page has to be built from a view taken *after* the write: whether the sandbox exists is a per-request read, and step 1 is the request that brings it into being. Both adding steps open the sandbox first. Without its `genlContext` edge the sandbox sees no shipped context, so BiologyContext's flight rule would not be visible from it and the write would derive nothing at all — the demo would quietly do nothing rather than fail.
(demo-page view)(demo-page {:keys [sandbox] :as view} first-h)The walkthrough: the script, the evidence for the conclusion under test, the next button, and what the KB currently holds about Pingu. Everything on it is read back out of the KB after the write, so the page cannot claim a state the engine is not in.
The walkthrough: the script, the evidence for the conclusion under test, the next button, and what the KB currently holds about Pingu. Everything on it is read back out of the KB *after* the write, so the page cannot claim a state the engine is not in.
(dev-repl)Start the browser for a REPL session and hand the prompt straight back.
What lein browser calls, and the only thing project.clj names. Port from
VAELII_WEB_PORT, else 3000; loopback only. A port already in use is reported, not
thrown — you asked for a REPL and you get one either way, which is the difference
between a busy port being an inconvenience and being a failed startup.
Start the browser for a REPL session and hand the prompt straight back. What `lein browser` calls, and the only thing `project.clj` names. Port from `VAELII_WEB_PORT`, else 3000; loopback only. A port already in use is **reported, not thrown** — you asked for a REPL and you get one either way, which is the difference between a busy port being an inconvenience and being a failed startup.
(dev-stop)Stop the server dev-repl started. No !: it takes down a socket, not knowledge —
the KB is untouched and still at the prompt.
Stop the server `dev-repl` started. No `!`: it takes down a socket, not knowledge — the KB is untouched and still at the prompt.
(find-page {:keys [kb] :as view} q)Term search over the KB's vocabulary: list every term whose name matches q, each
linking to its term page. q reads as re-find does — a bare dog finds every term
containing it, ^parent anchors — and it filters the index's term roster, so the cost
is the number of distinct terms rather than the number of sentexes.
A pattern that resolves to a single term jumps straight to that term's page —
either because it is the only match, or because the query names a term exactly
(so parentOf jumps even though it is a substring of grandparentOf). The jump
renders the term page and sets HX-Push-Url so the address bar reflects it. An
unusable pattern or an empty query reports gently.
Term search over the KB's vocabulary: list every term whose name matches `q`, each linking to its term page. `q` reads as `re-find` does — a bare `dog` finds every term containing it, `^parent` anchors — and it filters the index's term roster, so the cost is the number of distinct terms rather than the number of sentexes. **A pattern that resolves to a single term jumps straight to that term's page** — either because it is the only match, or because the query names a term *exactly* (so `parentOf` jumps even though it is a substring of `grandparentOf`). The jump renders the term page and sets `HX-Push-Url` so the address bar reflects it. An unusable pattern or an empty query reports gently.
(find-rows-page {:keys [kb] :as view} q offset)One more page of search hits — what the result list's continuation sentinel fetches.
One more page of search hits — what the result list's continuation sentinel fetches.
(fresh-starter-kb!)(fresh-starter-kb! opts)A KB freshly loaded with the starter ontology. Flushes the record + index
stores first, so a repeated run (or one over data from an earlier code version)
starts from a clean, deterministic state rather than re-asserting over stale
handles. For a persistent KB, construct one and call core/recover instead.
A KB freshly loaded with the starter ontology. Flushes the record + index stores first, so a repeated run (or one over data from an earlier code version) starts from a clean, deterministic state rather than re-asserting over stale handles. For a persistent KB, construct one and call `core/recover` instead.
(front-rows-page view section offset)One more page of a front-page list.
One more page of a front-page list.
(justification-page {:keys [kb] :as view} jid)(kbs-load id params)Start loading source id with the options the form submitted.
Start loading source `id` with the options the form submitted.
(kbs-page view)(kbs-page view note)The knowledge bases page: what is loaded, and what can be. note is what the catalog
said about the action that led here — a refusal is a state to show, not an error
status, since the page is still the right answer.
The knowledge bases page: what is loaded, and what can be. `note` is what the catalog said about the action that led here — a refusal is a state to show, not an error status, since the page is still the right answer.
(kbs-post act make-view)Perform a catalog action and answer with the page it changed.
The view is built after the action, not before: activating changes which KB the page reads, and rendering the one it was reading a moment ago would show the switch as not having happened. What the catalog refuses — a second concurrent load, a source already loaded, an entry whose loader has not yet stopped — comes back as a note on the page.
Perform a catalog action and answer with the page it changed. The view is built **after** the action, not before: activating changes which KB the page reads, and rendering the one it was reading a moment ago would show the switch as not having happened. What the catalog refuses — a second concurrent load, a source already loaded, an entry whose loader has not yet stopped — comes back as a note on the page.
(levels-page {:keys [kb] :as view} goal ctx)The lookup-to-query stack over a goal: what each of the eight levels answers, so the level at which results first appear is the mechanism the answer depends on. With no goal, the stack itself.
A vector goal is the conjunctive query prove takes, and the levels do not take
one — they answer about a literal. So a conjunction gets the join plan and stops
there, rather than being rendered through eight sections that cannot address it.
The lookup-to-query stack over a goal: what each of the eight levels answers, so the level at which results first appear is the mechanism the answer depends on. With no goal, the stack itself. A **vector** goal is the conjunctive query `prove` takes, and the levels do not take one — they answer about a literal. So a conjunction gets the join plan and stops there, rather than being rendered through eight sections that cannot address it.
(levels-rows-page view goal ctx lvl offset)One more page of results for a single level — what a level's continuation sentinel fetches.
One more page of results for a single level — what a level's continuation sentinel fetches.
(network-page {:keys [kb] :as view} ctx calc)The constraint network a calculus computes over one context: which terms it relates, what still holds of every pair, whether the believed facts are satisfiable at all, and one concrete arrangement consistent with them.
Every calculus is offered whether or not its prover is registered — a network is a
property of the stored facts, and add-prover only decides whether ask consults it.
The constraint network a calculus computes over one context: which terms it relates, what still holds of every pair, whether the believed facts are satisfiable at all, and one concrete arrangement consistent with them. Every calculus is offered whether or not its prover is registered — a network is a property of the stored facts, and `add-prover` only decides whether `ask` consults it.
(propose-apply-post {:keys [kb] :as view} lines)Store the accepted lines — the panel's one write, and the only one on this path.
Everything up to here proposes; this applies, and it applies the way the editor does:
check-edit over the whole batch first, and v/edit once so the adds land in one
settle rather than settling per line. A batch with any problem stores nothing, since a
partial commit of a reviewed set is the outcome nobody chose.
Store the accepted lines — the panel's one write, and the only one on this path. Everything up to here proposes; this applies, and it applies the way the editor does: `check-edit` over the whole batch first, and **`v/edit` once** so the adds land in one settle rather than settling per line. A batch with any problem stores nothing, since a partial commit of a reviewed set is the outcome nobody chose.
(propose-level-post {:keys [kb] :as view} froms ctxs level)The same proposal, re-read at another density.
The originals ride the list's own hidden fields, so this re-derives every verdict from
the KB and renders the rows again — without another turn. That is the whole claim
of the level control: a reader who opens guided, works out what a refusal meant and
drops to dense has asked the model exactly once.
The same proposal, re-read at another density. The originals ride the list's own hidden fields, so this re-derives every verdict from the KB and renders the rows again — **without another turn**. That is the whole claim of the level control: a reader who opens `guided`, works out what a refusal meant and drops to `dense` has asked the model exactly once.
(propose-line-post {:keys [kb] :as view} from ctx i n level)Re-render one row on shape n. What arrives is the original sentence and a
number; the shape itself is re-derived here from correct, which is a pure function of
the KB and what the model wrote — so a sentence cannot be smuggled into the row by
editing the request, and the chips the reader ends up committing against were computed
from the KB rather than sent to it.
Re-render one row on shape `n`. What arrives is the **original** sentence and a number; the shape itself is re-derived here from `correct`, which is a pure function of the KB and what the model wrote — so a sentence cannot be smuggled into the row by editing the request, and the chips the reader ends up committing against were computed from the KB rather than sent to it.
(propose-post {:keys [kb] :as view} term ctx message level)Run one proposal turn for a term and render what came back.
Every bound the panel places on the model is here: the token cap, the transport deadline, and the session's own turn budget. A throw out of the provider is caught and rendered — a browser panel is not the place to surface a stack trace, and a model backend is the one dependency that fails by not answering rather than by erroring.
Run one proposal turn for a term and render what came back. Every bound the panel places on the model is here: the token cap, the transport deadline, and the session's own turn budget. A throw out of the provider is caught and rendered — a browser panel is not the place to surface a stack trace, and a model backend is the one dependency that fails by *not answering* rather than by erroring.
(propose-preview-post {:keys [kb] :as view} lines)What the accepted lines would do, without doing it.
The same payload the commit button posts, read through v/preview instead of
v/edit — so the panel a reader decides from is computed from the very batch that
would land, rather than from a reconstruction of it. A read: preview hands the KB
back at the same handles, which is why this can run on every change of the accepted
set instead of once behind a confirmation.
A report-only line is held back rather than previewed: the commit refuses it
(report-only-problems), so previewing it would promise a consequence the button will
not deliver — and it would ask the engine about the very sentence the correction was
warning about.
What the accepted lines would do, without doing it. The same payload the commit button posts, read through `v/preview` instead of `v/edit` — so the panel a reader decides from is computed from the very batch that would land, rather than from a reconstruction of it. A read: `preview` hands the KB back at the same handles, which is why this can run on every change of the accepted set instead of once behind a confirmation. A report-only line is held back rather than previewed: the commit refuses it (`report-only-problems`), so previewing it would promise a consequence the button will not deliver — and it would ask the engine about the very sentence the correction was warning about.
(reasoning-page {:keys [kb sandbox] :as view})The gallery. Every card is computed from the live KB on render; the ones with premises are computed from the sandbox once the reader has established them, and show a button until then.
The gallery. Every card is computed from the live KB on render; the ones with premises are computed from the sandbox once the reader has established them, and show a button until then.
(reasoning-run kb sandbox id)Establish one example's premises in the sandbox. A write, so a POST — and the
sandbox is opened first, exactly as the demo does: without its genlContext edge it
would see no shipped rule and the example would quietly derive nothing.
Establish one example's premises in the sandbox. A write, so a POST — and the sandbox is opened first, exactly as the demo does: without its `genlContext` edge it would see no shipped rule and the example would quietly derive nothing.
(retract-post {:keys [kb] :as view} handles-csv)Retract the selected handles through edit — one settle for the whole selection,
the same write path the editor's save takes. The answer deletes every row that is
actually gone out of band (the selection and whatever the dependency-directed sweep
took with it), so the page corrects itself instead of reloading.
Retract the selected handles through `edit` — one settle for the whole selection, the same write path the editor's save takes. The answer deletes every row that is actually gone out of band (the selection *and* whatever the dependency-directed sweep took with it), so the page corrects itself instead of reloading.
(sentex-page {:keys [kb] :as view} h)(start target {:keys [port host reload?] :or {port 3000 host loopback}})Start a Jetty server for target (a KB, an access value, or a catalog holder).
Returns the server (non-blocking). :host defaults to loopback; pass an address
("0.0.0.0") to bind publicly. :reload? serves through reloading-handler, so a
namespace reload reaches the running server — what lein browser starts with.
Start a Jetty server for `target` (a KB, an access value, or a catalog holder). Returns the server (non-blocking). `:host` defaults to loopback; pass an address (`"0.0.0.0"`) to bind publicly. `:reload?` serves through `reloading-handler`, so a namespace reload reaches the running server — what `lein browser` starts with.
(stats-page view)(stats-page view note)(stats-page {:keys [kb types] :as view} note clashes?)KB-wide statistics: the headline counts (contexts, types, stored sentexes, and the reasoning-health tallies), what the last chaining run did and a control to run another, a contexts-by-size table, and — when non-empty — the actual contradictions, conflicts, and dropped-derivation violations.
clashes? asks the standing disjointness question, which is computed rather than
filed and so is not asked unless the reader asks for it.
note is what a just-finished forward-chaining run reported, shown above the
numbers it changed.
KB-wide statistics: the headline counts (contexts, types, stored sentexes, and the reasoning-health tallies), what the last chaining run did and a control to run another, a contexts-by-size table, and — when non-empty — the actual contradictions, conflicts, and dropped-derivation violations. `clashes?` asks the standing disjointness question, which is computed rather than filed and so is not asked unless the reader asks for it. `note` is what a just-finished forward-chaining run reported, shown above the numbers it changed.
(stats-rows-page {:keys [kb] :as view} section offset)One more page of a stats-page list — what its scroll sentinel fetches. Every section is recomputed rather than carried: each is a function of the KB, so a continuation asks the same question the page asked and gets the same order.
One more page of a stats-page list — what its scroll sentinel fetches. Every section is recomputed rather than carried: each is a function of the KB, so a continuation asks the same question the page asked and gets the same order.
The browser's stylesheet, on the classpath (resources/public/vaelii.css).
The browser's stylesheet, on the classpath (resources/public/vaelii.css).
(term-page {:keys [kb] :as view} term)(term-rows-page {:keys [kb] :as view} term g offset)One more page of rows for index group g of term — what a group's continuation
sentinel fetches. The groups are recomputed and indexed the same way the page built
them, so g names the same group it did then.
One more page of rows for index group `g` of `term` — what a group's continuation sentinel fetches. The groups are recomputed and indexed the same way the page built them, so `g` names the same group it did then.
(tree-rows-page view pred node offset)One node's children, as bare rows — what a disclosure fetches when it is opened, and
what its show more sentinel fetches to extend it.
One node's children, as bare rows — what a disclosure fetches when it is opened, and what its `show more` sentinel fetches to extend it.
(view kb req)What one request's rendering reads that does not vary row to row — built once per request and threaded through every render fn in place of a bare KB.
What one request's rendering reads that does not vary row to row — built once per request and threaded through every render fn in place of a bare KB.
(warm-model)Ask the configured backend to make itself ready, on a thread of its own.
Measured: the latency of a local turn is model load, not generation — three
identical page turns took 11.33 s, then 0.39 s, then 0.30 s. Warming at start moves
that eleven seconds off the first reader's question. It is fire-and-forget by
construction: it must not delay the server coming up, and a host that is down is the
ordinary case (provider/warm answers nil and the panel falls back to the stub).
Ask the configured backend to make itself ready, on a thread of its own. Measured: the latency of a local turn is model **load**, not generation — three identical page turns took 11.33 s, then 0.39 s, then 0.30 s. Warming at start moves that eleven seconds off the first reader's question. It is fire-and-forget by construction: it must not delay the server coming up, and a host that is down is the ordinary case (`provider/warm` answers nil and the panel falls back to the stub).
(why-page {:keys [kb] :as view} h)The whole proof tree for a handle — vaelii.core/why rendered, collapsible. Linked
from the sentex page, which shows only the first hop.
The whole proof tree for a handle — `vaelii.core/why` rendered, collapsible. Linked from the sentex page, which shows only the first hop.
cljdoc builds & hosts documentation for Clojure/Script libraries
| Ctrl+k | Jump to recent docs |
| ← | Move to previous article |
| → | Move to next article |
| Ctrl+/ | Jump to the search field |