litexpy

Python runner for an interactive litex terminal session.

Links

• PyPI: https://pypi.org/project/litexpy/
• GitHub: https://github.com/litexlang/litexpy

Prerequisites

litexpy starts the local litex command in an interactive terminal session. It does not bundle the Litex executable, so install Litex first if litex is not already available in your terminal.

If you already have Litex

If litex -version works in your terminal, install only the Python package:

pip install litexpy

If you have not installed Litex

Install Litex first locally on your machine, then install litexpy.

Setup guide: https://litexlang.com/doc/Setup

Usage

Use a runner as a context manager so the underlying Litex process is closed automatically:

import litexpy

with litexpy.Runner() as runner:
    results = runner.run("1 = 1")

    print(results[0]["result"])
    print(results[0]["stmt"])

Runner() starts litex from your PATH by default. To use another command, pass an argument list:

runner = litexpy.Runner(command=["cargo", "run", "--quiet", "--"])

For local Litex development, set a default command so plain Runner() uses the checkout you choose:

export LITEXPY_LITEX_COMMAND='cargo run --quiet --manifest-path /path/to/golitex/Cargo.toml --'

If you already built a local binary, point directly at it:

export LITEXPY_LITEX_BIN=/path/to/golitex/target/debug/litex

An explicit Runner(command=...) always wins over these environment variables.

Run multiple lines or block-style Litex code in the same session:

with litexpy.Runner() as runner:
    results = runner.run("1 = 1\n0 = 0")

    block_results = runner.run(
        """forall x R:
    x = 2
    =>:
        x + 1 = 3
        x^2 = 4"""
    )

Facts accepted by run() stay in the interactive session until you call clear():

with litexpy.Runner() as runner:
    runner.run("have a R = 1")
    runner.run("a = 1")
    runner.clear()

Use sandbox_run() for candidate code that should see the current successful context but should not modify the main session:

with litexpy.Runner() as runner:
    runner.run("have a R = 1")
    trial = runner.sandbox_run("have b R = 2\na = 1")
    still_isolated = runner.run("b = 2")  # returns an error result

Pass commit=True to preflight in a sandbox first, then run the same code in the main session only if the sandbox succeeds:

with litexpy.Runner() as runner:
    committed = runner.sandbox_run("have b R = 2", commit=True)
    now_available = runner.run("b = 2")

commit=True is a preflight-then-run workflow in Python. It is not a single kernel-level transaction, so avoid relying on it for code that reads external files that may change between the preflight and the commit run.

If you do not use a with block, call runner.quit() or runner.close() when you are done. A live Runner owns a live Litex process; relying on Python garbage collection or interpreter shutdown is not the supported lifecycle.