Function kernel

tests/test_z3_compat.py:219–235

(example_lib)

@pytest.fixture(scope="module")
def kernel(example_lib) -> Kernel:
    k = Kernel(example_lib)
    import subprocess
    from pathlib import Path

    sp = (
        subprocess.check_output(
            ["lake", "env", "printenv", "LEAN_PATH"],
            cwd=str(Path(__file__).parent / "lean"),
        )
        .decode()
        .strip()
    )
    k.init_search(sp)
    k.load(["Init", "LeanPy.Z3"])
    set_kernel(k)
    return k


# ------------------------------------------------------------------