Node.refresh()

Bring this node and every node it reads up to date, and write the

Usage

Node.refresh(
    *,
    engine=None,
    audit=False,
    route="auto",
    unverified=False,
    reproducible=None
)

stored ones. engine runs the plans: "duckdb" (in memory, the default), "polars", "datafusion", "spark" or a Spark session. With audit, every batch is compared with recomputation before it is applied (AuditError).

A stored node’s sink commits each state once, by its epoch, so a rerun must reproduce its rows up to the sink’s reproducible (rows as a multiset, doubles within the plan’s bound and other values exact by default): a node whose result is not determined up to row order, or whose engine varies between runs more than that, is refused before anything runs (#444, D10, D20). Each node with a contract is refused unless its report is proved, or unverified=True (Report.run), or its transform says on_unproved="warn"; its proof is taken to engine by a route (sverify.routes.choose, D13), or the refresh is refused. StageRefresh.route records it.

Each node is refreshed once per call, upstream first, against each source’s latest version when the call starts, and every stored node is written once. The first refresh computes a node in full, or resumes a stored node from its table; later ones apply the changes to the sources with the delta plans Lean derives, or recompute and diff a node that has none (status says which).

Parameters

engine: Any = None: What runs the plans: "duckdb", "polars", "datafusion", "spark" or a Spark session. It may differ from one refresh to the next. Default None: DuckDB, in memory, the engine of the nodes’ state (as Report.run’s None is its connection’s).
audit: bool = False: Whether to compare every batch with recomputation before applying it. Default False.
route: RouteKind | Literal["auto"] = "auto": "auto" (the default) chooses a route for each node with a contract; "native", "translated", "transfer" or "recheck" takes that one or refuses ("reference" is a deprecated alias of "translated").
unverified: bool = False: Refresh nodes whose contract is not proved anyway; their route is "unverified", with what was not proved, and an UnverifiedRunWarning says so. Default False: such a node refuses the refresh, unless its transform says on_unproved="warn".
reproducible: Observation | None = None: What a rerun must reproduce for every node (sv.equivalent(...), D20), over each sink’s own. Default None: a stored node needs its sink’s, another node nothing.

Returns

Refresh

A Refresh: what was done to each node, upstream first.

print it for the full report, or log summary() for one line

per node.

Raises

sverify.errors.PreconditionError: A precondition on a source does not hold on its rows (checked in full on the first refresh, then on each batch).
sverify.errors.SchemaError: A source’s schema changed in a way the contract, proved against the old schema, cannot follow.
sverify.errors.AuditError: With audit, a batch disagrees with recomputation; nothing was applied.
sverify.errors.UnverifiedRunError: A node’s contract is not proved (a VerificationError and a RouteError); nothing was refreshed.
sverify.errors.RouteError: A stored node’s result is not determined up to row order, or no route takes a node’s proof to engine; nothing was refreshed.

Examples

With r from the Node example:

result = r.refresh(engine="polars")
print(result)  # one entry per node, upstream first
r.to_arrow().to_pylist()  # [{'id': 3, 'doubled': 100}]