docs(context): stem order is a known evaluator defect, not a source contract; define refuses in every build (improvise-rnak)
Co-Authored-By: Claude Sonnet 5.5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01VdfEGXA7aJ6ftMsCc9PJze
This commit is contained in:
committed by
Edward Langley
parent
4b246f8108
commit
ed447c8dc9
@@ -457,7 +457,7 @@ change log, no stems. These are the readings taken.
|
|||||||
members; the view's hidden pairs go as `excluding`. `Eager::occupancy` lists every key to say the
|
members; the view's hidden pairs go as `excluding`. `Eager::occupancy` lists every key to say the
|
||||||
same thing.
|
same thing.
|
||||||
5. **`define(edit)` takes a formula or an aggregation edit and refreshes.** A cell edit is the source's:
|
5. **`define(edit)` takes a formula or an aggregation edit and refreshes.** A cell edit is the source's:
|
||||||
`Model::set_cell` refuses it in a debug build.
|
`define` refuses it with an `assert!` of its own in every build (`a_cell_edit_on_a_pushdown_is_refused`).
|
||||||
6. **What the differential proves, and what it does not.** `value`, `raw_fold`, `covered` and `total` are
|
6. **What the differential proves, and what it does not.** `value`, `raw_fold`, `covered` and `total` are
|
||||||
the same four functions for `Eager` and `Pushdown` (`reads.rs`; they were copies, and are shared now),
|
the same four functions for `Eager` and `Pushdown` (`reads.rs`; they were copies, and are shared now),
|
||||||
so a Pushdown-against-Eager differential cannot see a mistake in them. `Pushdown::members` repeats
|
so a Pushdown-against-Eager differential cannot see a mistake in them. `Pushdown::members` repeats
|
||||||
@@ -473,14 +473,17 @@ change log, no stems. These are the readings taken.
|
|||||||
that appears after the stem list was taken has no cell until the next refresh
|
that appears after the stem list was taken has no cell until the next refresh
|
||||||
(`a_stem_that_appears_between_the_stem_list_and_the_folds_waits_for_the_next_refresh`). A real source
|
(`a_stem_that_appears_between_the_stem_list_and_the_folds_waits_for_the_next_refresh`). A real source
|
||||||
should serve a refresh from one read transaction; nothing here can ask it to.
|
should serve a refresh from one read transaction; nothing here can ask it to.
|
||||||
8. **The order of the stems is part of the contract.** The passes of the fixed point visit stems in the
|
8. **Known evaluator defect: the result can depend on the order of the stems** (improvise-bw4p.30). The
|
||||||
order `distinct_without` lists them, and a document whose stems read each other settles in as many
|
passes of the fixed point update the cache in place, visiting stems in the order `distinct_without`
|
||||||
passes as its dependency chain runs against that order, with a bound of sixteen. A chain of
|
lists them, and stop at sixteen. A document whose stems read each other settles in one pass listed
|
||||||
eighteen stems settles in one pass listed along the chain and not at all listed against it
|
along its dependency chain and takes one pass per link listed against it, so an eighteen-link chain
|
||||||
(`the_order_stems_are_listed_in_decides_a_result_and_a_source_must_keep_it`). No fixture before it
|
is `circular` the second way. That is the evaluator's fault, not an obligation on a source: a SQL
|
||||||
had a result that depended on the order, and a source listing stems sorted passed everything.
|
source has no order to keep, and bw4p.30 is to make the fixed point independent of it. Until then
|
||||||
The first-seen order is `DataStore`'s insertion order; a source with no order of its own must
|
the first-seen order (`DataStore`'s insertion order) is what the oracle uses, and
|
||||||
fix one.
|
`the_order_stems_are_listed_in_decides_a_result_today` pins today's behaviour: along the chain 18,
|
||||||
|
sorted `circular`, and a source listing its stems sorted is a divergence. No fixture before it had a
|
||||||
|
result that depended on the order. When bw4p.30 lands the test's sorted half must change to expect
|
||||||
|
agreement, and this item goes.
|
||||||
9. **What is and is not proven.** The tests run against `Remote` (`tests/support/remote.rs`), a scanning
|
9. **What is and is not proven.** The tests run against `Remote` (`tests/support/remote.rs`), a scanning
|
||||||
in-memory table with counters, that shares no evaluator with `Eager` and answers queries over rows.
|
in-memory table with counters, that shares no evaluator with `Eager` and answers queries over rows.
|
||||||
Without a real SQL engine only the **contract** is proven: that a source answering these six
|
Without a real SQL engine only the **contract** is proven: that a source answering these six
|
||||||
|
|||||||
@@ -110,9 +110,11 @@ engine answers without sending rows (`COUNT(*) ... WHERE`, `SELECT DISTINCT`), a
|
|||||||
read that would have transferred every key: `Eager::occupancy` lists all keys, and
|
read that would have transferred every key: `Eager::occupancy` lists all keys, and
|
||||||
`recompute_formulas` walked every cell to find its stems. `recompute_formulas` now asks
|
`recompute_formulas` walked every cell to find its stems. `recompute_formulas` now asks
|
||||||
`distinct_without(target and None categories)` once per formula, and the order it returns is
|
`distinct_without(target and None categories)` once per formula, and the order it returns is
|
||||||
the order the cells were first seen in, so the stems are inserted in the order they always were
|
the order the cells were first seen in, so the stems are inserted in the order they always were.
|
||||||
(the passes of a fixed point visit stems in that order). A source with no order of its own must
|
That order is not a contract a source can be held to: the passes of the fixed point visit stems in
|
||||||
fix one, or the passes of a document whose stems read each other may differ between refreshes.
|
it and a chain of stems can settle or not by it. That is a known evaluator defect, improvise-bw4p.30
|
||||||
|
(`context/code/improvise-incremental.md`, step 7 item 8), and until it is fixed a source with no order
|
||||||
|
of its own should list stems in a stable one.
|
||||||
|
|
||||||
`Select::admits` is the predicate of a select over one key, for a source that must test keys itself
|
`Select::admits` is the predicate of a select over one key, for a source that must test keys itself
|
||||||
(`DataStore::count`). `TableSource` does not use it: its own `holds` is the independent second reading.
|
(`DataStore::count`). `TableSource` does not use it: its own `holds` is the independent second reading.
|
||||||
|
|||||||
@@ -925,10 +925,10 @@ The same for `ClearCell`.
|
|||||||
Review of #358: two backends over one feed; one write; `a.sync(); b.sync()`. The first sees it, the
|
Review of #358: two backends over one feed; one write; `a.sync(); b.sync()`. The first sees it, the
|
||||||
second does not. This pins the behaviour as documented rather than as a guarantee: a drain is destructive.
|
second does not. This pins the behaviour as documented rather than as a guarantee: a drain is destructive.
|
||||||
|
|
||||||
### the_order_stems_are_listed_in_decides_a_result_and_a_source_must_keep_it
|
### the_order_stems_are_listed_in_decides_a_result_today
|
||||||
|
|
||||||
Review of #360: stem order was invisible to every differential (a sorted `distinct_without` went
|
Review of #360: stem order was invisible to every differential (a sorted `distinct_without` went
|
||||||
uncaught). Eighteen products are stored in chain order with names that sort the other way, and one nested
|
uncaught). It pins today's behaviour of a known evaluator defect (improvise-bw4p.30), not a contract. Eighteen products are stored in chain order with names that sort the other way, and one nested
|
||||||
`IF` formula reads the product before it. Along the chain it settles in one pass (the last link is 18);
|
`IF` formula reads the product before it. Along the chain it settles in one pass (the last link is 18);
|
||||||
sorted it needs one pass per link and the bound of sixteen leaves it `circular`. The test asserts both
|
sorted it needs one pass per link and the bound of sixteen leaves it `circular`. The test asserts both
|
||||||
values, that a sound source passes the differential and that a source listing the stems sorted is a
|
values, that a sound source passes the differential and that a source listing the stems sorted is a
|
||||||
|
|||||||
@@ -232,7 +232,7 @@ fn chain() -> Model {
|
|||||||
}
|
}
|
||||||
|
|
||||||
#[test]
|
#[test]
|
||||||
fn the_order_stems_are_listed_in_decides_a_result_and_a_source_must_keep_it() {
|
fn the_order_stems_are_listed_in_decides_a_result_today() {
|
||||||
let model = chain();
|
let model = chain();
|
||||||
let last = CellKey::new(vec![
|
let last = CellKey::new(vec![
|
||||||
("Product".into(), "n82".into()),
|
("Product".into(), "n82".into()),
|
||||||
|
|||||||
Reference in New Issue
Block a user