The dropped-conclusion ledger: what the derivation path refused to store, kept as a value a caller can read afterwards instead of thrown at whoever happened to be writing.
A namespace of its own because of who writes it. Two paths file entries and they
sit on opposite sides of the engine: the forward chainer
(vaelii.impl.chain) files a conclusion it dropped, and the prover registry
(vaelii.impl.provers) files an aggregate's numeric error — and the chainer is built
on the registry, so the registry cannot name it. The ledger reads nothing from
either, only (:violations kb) and (:chain-stats kb), so it sits below both and the
edge runs the one direction the layering allows.
Why a ledger rather than a throw: an entry is recorded from inside the semi-naive
fixpoint and from inside a relabel, and neither may abort — a definitional check that
aborted mid-fixpoint would leave belief half-computed, which is the failure the value-
first checks (vaelii.impl.checks) exist to avoid. So a violation is reported, and
the run continues without the conclusion.
It reads the record store for one thing only: an entry names the rule that concluded
the dropped sentence by handle, and a handle is not something an operator reading
a log can look up. So at :debug the drop is followed by the rule itself.
The dropped-conclusion ledger: what the derivation path refused to store, kept as a value a caller can read afterwards instead of thrown at whoever happened to be writing. A namespace of its own because of **who writes it**. Two paths file entries and they sit on opposite sides of the engine: the forward chainer (`vaelii.impl.chain`) files a conclusion it dropped, and the prover registry (`vaelii.impl.provers`) files an aggregate's numeric error — and the chainer is built *on* the registry, so the registry cannot name it. The ledger reads nothing from either, only `(:violations kb)` and `(:chain-stats kb)`, so it sits below both and the edge runs the one direction the layering allows. Why a ledger rather than a throw: an entry is recorded from inside the semi-naive fixpoint and from inside a relabel, and neither may abort — a definitional check that aborted mid-fixpoint would leave belief half-computed, which is the failure the value- first checks (`vaelii.impl.checks`) exist to avoid. So a violation is *reported*, and the run continues without the conclusion. It reads the record store for one thing only: an entry names the rule that concluded the dropped sentence by **handle**, and a handle is not something an operator reading a log can look up. So at `:debug` the drop is followed by the rule itself.
(report kb entries)Append dropped-conclusion entries to the accumulating ledger, stamped with the chaining run that dropped them, and log each at :warn — a drop must be visible even to a caller who never reads the ledger (a bulk load polls nothing).
The :warn line carries the entry as filed, which names the rule by handle. At
:debug each drop that blames a rule is followed by that rule's own sentence: the
handle is what the ledger stores and the sentence is what the operator was going to go
looking for, and the lookup rides inside Trove's payload delay, so a run at :warn
pays for none of it.
No !: this accumulates a report and destroys nothing, and the ledger it appends to is
emptied only by vaelii.core/clear-violations!, which does.
Append dropped-conclusion entries to the accumulating ledger, stamped with the chaining run that dropped them, and log each at :warn — a drop must be visible even to a caller who never reads the ledger (a bulk load polls nothing). The `:warn` line carries the entry as filed, which names the rule by handle. At `:debug` each drop that blames a rule is followed by that rule's own sentence: the handle is what the ledger stores and the sentence is what the operator was going to go looking for, and the lookup rides inside Trove's payload delay, so a run at `:warn` pays for none of it. No `!`: this accumulates a report and destroys nothing, and the ledger it appends to is emptied only by `vaelii.core/clear-violations!`, which does.
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 |