Skip to main content

engines.run()

Run a plan in Lean’s written form on engine (default: the

Usage

Source

engines.run(con: Connection, plan_json: str, engine: Engine | Any = None, keep: Literal[False] = False, finite: bool = True) -> pa.Table
 
engines.run(con: Connection, plan_json: str, engine: Engine | Any = None, keep: bool, finite: bool = True) -> pa.Table | Resident

connection’s), over the tables of con. DataFusion runs it as datafusion_plan writes it; "spark" runs it on the local Spark session (sverify.spark_engine.session), and a Spark session as engine runs it there.

DuckDB runs the SQL sverify.engines.to_sql writes for the plan, Polars a translation to a lazy frame, Spark the Spark SQL sverify.engines.to_sql writes in the SPARK dialect; each gives the result Rel.eval gives. This is sverify.engines.run.

Parameters

con: Connection

The connection whose tables the plan reads.

plan_json: str

A plan in Lean’s written form (a node’s plan, or sverify.engines.written_plan’s output).

engine: Engine | Any = None

"duckdb", "polars", "datafusion", "spark", or a Spark session. Default: the connection’s engine.

keep: bool = False

On DuckDB, leave the result in DuckDB, as a Resident table. Other engines ignore it. Default: False.

finite: bool = True
On DuckDB and Polars, check that no operation on finite doubles gives ±∞ (Issue.infinite, #575), the reference’s precondition. Default: True; Report.run passes False for a plan verified with semantics="duckdb", which allows ±∞.

Returns

pa.Table | Resident

The result as an Arrow table, with the plan’s output names; with

keep on DuckDB, a Resident table.

Raises

ValueError

engine is unknown, or the checker rejects the plan.

ImportError

The engine is an extra that is not installed.

sverify.engines.Unsupported
The plan uses something the engine’s SQL dialect cannot express (DuckDB, Spark). Polars refuses what its translation does not cover with a ValueError of its own.

Examples

The plan of a transform, on every engine:

import ibis
import pyarrow as pa
import sverify as sv
from sverify.engines import ENGINES, run
from sverify.io import StaticSource

orders = StaticSource(pa.table({"id": [1, 2], "amount": [30, 5]}), name="orders")


@sv.transform()
def big_orders(orders):
    return orders.filter(orders.amount > 10)


plan = big_orders(orders).internal_plan  # the plan the checker proved

con = sv.connect()
con.create("orders", ibis.schema({"id": "int64", "amount": "int64"}), [(1, 30), (2, 5)])
for engine in ENGINES:
    assert run(con, plan, engine).to_pylist() == [{"id": 1, "amount": 30}]