## engines.run()


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


Usage

``` python
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](engines.to_sql.md#sverify.engines.to_sql) writes for the plan, Polars a translation to a lazy frame, Spark the Spark SQL [sverify.engines.to_sql](engines.to_sql.md#sverify.engines.to_sql) writes in the [SPARK](engines.SPARK.md#sverify.engines.SPARK) dialect; each gives the result `Rel.eval` gives. This is [sverify.engines.run](engines.run.md#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](Node.plan.md#sverify.Node.plan), or [sverify.engines.written_plan](engines.written_plan.md#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](Report.run.md#sverify.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:

``` python
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}]
```