LeanElpi

λProlog inside Lean 4. Write tactics, commands and proof search as logic programs, share types and functions with Lean in both directions, and get proofs the Lean kernel checks.

LeanElpi is a clean-room, native Lean 4 implementation of the ELPI dialect of λProlog, the language behind Coq-Elpi. It embeds in Lean as a metaprogramming tool (commands, tactics, MetaM builtins), works as a pure library for ordinary Lean programs, ships a standalone lean-elpi binary, and adds an opt-in LF layer with kernel-checked proof terms.

Status: version 0.3: the engine, constraints, Lean integration, the LF layer and the Lean/ELPI type bridge are implemented. Documentation site and book: https://volland.github.io/lean-elpi/ (sources in site/, built into docs/ with python3 site/build.py).

Use it in your project

Add LeanElpi as a Lake dependency (Lean 4.35.0, no Mathlib needed):

-- lakefile.lean
require «lean-elpi» from git "https://github.com/Volland/lean-elpi" @ "v0.3.3"

or in lakefile.toml:

[[require]]
name = "lean-elpi"
git = "https://github.com/Volland/lean-elpi"
rev = "v0.3.3"

Then import Elpi:

import Elpi
open Elpi.Cmd

-- a Lean type, shared with ELPI
inductive Tree (α : Type) where
  | leaf
  | node (l : Tree α) (a : α) (r : Tree α)
  deriving Elpi

-- a Lean function, callable from ELPI
def twice (n : Nat) : Nat := 2 * n
elpi_extern twice

elpi_program demo
#elpi demo lp%{ twice 21 X }%     -- X = 42

From Python, Node.js and Rust

One native library serves three bindings: load a program once, extend it, query it many times.

pip install leanelpi        # Python
npm install @lean-elpi/leanelpi   # Node.js
cargo add leanelpi          # Rust (needs the native library, see the guide)

from leanelpi import Program
Program("pred n o:int.\nn 1.\nn 2.").solve("n X")   # two solutions: X = 1, X = 2

macOS and Linux, no Lean installation needed. Guide: From Python, Node.js and Rust; release steps: PUBLISHING.md.

What it does

• ELPI engine in Lean: typed clauses, pi/=>, higher-order pattern unification, modes, constraints and CHR, a command-line tool, and a lazy library API.
• Lean integration: {{ … }} quotations, tactics and commands written in λProlog, lean.* builtins over MetaM, a typed rule DSL.
• Type bridge (new in 0.2): deriving Elpi for parametric and recursive types, elpi_data (ELPI types to Lean inductives), elpi_extern (typed Lean functions as ELPI predicates), lean.env.indt / lean.add_inductive (read and create inductive types from ELPI).
• Bindings: Python, Node.js and Rust packages over a C interface, with the Lean runtime inside one shared library.
• LF layer: dependently typed signatures, recorded proof terms, export to Lean inductives, kernel-checked certificates.

Performance and compatibility

Measured against ELPI 1.18 on ELPI's own performance programs (tests/bench), all 24 of them run on release 0.3.3 (11 were rejected by 0.3.2). It is about 2.4 times slower by geometric mean over the 20 programs where ELPI takes more than 0.1 s, 6.2 times at worst, and faster than ELPI on cbv, on start-up and on the smallest programs; release 0.3.2 was 2.3 times slower on the programs it could read, and 0.3.0 was 31 times. It passes 52 of the 114 upstream ELPI tests that apply and 38 of 40 corpus programs. Memory is 50 to 200 MB, except map on lists (1.4 GB: nothing reclaims variables in a long run). Details, the known failures and how to reproduce: the blog posts compatibility and performance why it was slow and every performance program runs and what we took from ELPI's runtime.

See CHANGELOG.md for releases and CONTRIBUTING.md to help.

Where to read

The docs form a typed knowledge graph read with the tg CLI:

tg search "pattern unification"
tg section "decisions#Persistent store"
tg trace --gaps          # what is not implemented or verified yet
tg check && tg validate  # links, structure, typed edges

Build

lake build                        # library + lean-elpi executable (Lean 4.35.0)
tests/conformance/run.sh record   # store ELPI 1.18 oracle answers (needs opam elpi)
tests/conformance/run.sh          # compare lean-elpi against the oracle

License

Apache-2.0, clean-room: no upstream ELPI (LGPL-2.1) code is ported or vendored.