A Lean (4) type checker written in (R)Python.

rpylean isn't complete yet.

Binaries are regardless currently built via GitHub Actions, so if you'd like you should be able to download and run one for your OS by visiting the latest CI run for the main branch.

You'll need to install PyPy (2) and also to have a checkout of PyPy which contains the RPython toolchain in order to work on rpylean.

Any RPython interpreter (program) can be run "untranslated" -- meaning as if it were a "normal" Python program on top of another Python interpreter -- or "translated", meaning as a standalone binary. The former is great because it allows use of any Python tool to work on the interpreter, and critically, any Python error handling is propagated as normal. And translated binaries are of course great because they're fast and self-contained, not depending on Python at all. So, the former is what you often use while developing, and the latter is what we build for actual use. The translated binary has a JIT inserted; pass --jit off at runtime to disable it (or --jit help to see other tunable parameters).

To run rpylean untranslated (i.e. on top of a Python interpreter) run:

PYTHONPATH=<pypy-checkout>/ pypy -m rpylean check <path/to/lean4export/file>

or

just rpylean <any CLI args>

(if you follow the section below on just).

The argument you pass should be a file exported via lean4export.

The ffi subcommand talks to a real Lean toolchain via FFI, skipping the lean4export round trip:

rpylean ffi check Init                     # type-check every constant in `Init`
rpylean ffi check --filter Nat.succ Init   # only specific declarations
rpylean ffi export Init                    # emit lean4export-format NDJSON
rpylean ffi repl Init                      # REPL with `Init` loaded

The Lean prefix is auto-detected from $LEAN_PREFIX or lean --print-prefix. Pass --prefix /path/to/lean to override.

To translate rpylean and build a binary run:

pypy <pypy-checkout>/rpython/bin/rpython --opt=jit targetrpylean.py

or

just translate

which will output a standalone rpylean-c binary usable with the same CLI as above. Pass --jit off at runtime to disable the JIT.

It's extremely important to write tests (in general) but certainly when working on RPython projects. Translating can take around 30 seconds, so doing so each time you make a change is unrealistic. Running the entire test suite however (as a normal Python program) takes less than a second.

There are some tests for rpylean which can be run via:

pypy <pypy-checkout>/pytest.py <rpylean-checkout>/tests

or

just test

There's a justfile alongside this README which can be used to perform all of the commands mentioned above. To use it, after installing just and cloning PyPy and lean4export, create a .env file containing:

PYPY_CHECKOUT=/path/to/pypy/checkout
LEAN4EXPORT_CHECKOUT=/path/to/lean4export/checkout

You can then run just rpylean, just translate and/or just test.

• Type Checking in Lean 4 by @ammkrn
• lean4export
• RPython's documentation