Blog
- How compatible and how fast is LeanElpi? Test results against ELPI and Teyjus
· LeanElpi 0.3.0 against ELPI 1.18 and Teyjus: what ELPI's own test suite says about compatibility, and a benchmark that shows LeanElpi is about 30 times slower and hungry for memory. - Every ELPI performance program now runs on LeanElpi
· Nine language and library gaps kept eleven of ELPI's performance programs from loading. Closing them lets the benchmark cover all of them: LeanElpi is 2.4 times slower than ELPI by geometric mean, and 6.2 times at worst. - Types across the boundary
· LeanElpi can now share data types, functions and inductive declarations between Lean and λProlog in both directions. - What we took from ELPI's runtime to close the gap
· A second round of profiling found the rest of LeanElpi's gap with ELPI in allocation, not in algorithms. Doing at load time what ELPI does at load time, and fusing two term traversals into one, took the geometric-mean slowdown from 2.4 to 1.9 times and the worst case from 10.5 to 4.6. - Why LeanElpi was 30 times slower than ELPI, and what fixed it
· Profiling the LeanElpi engine found three specific costs, not a Lean limit. Fixing them took the geometric-mean slowdown against ELPI from 31 times to 3, and memory from gigabytes to about 100 MB. - How LeanElpi is built: architecture of a λProlog engine in Lean
· The layers of LeanElpi, from the term store and the abstract machine to solver tiers, the Lean bridge and the LF certificate pipeline. - Announcing LeanElpi 0.1
· The first release: an ELPI engine in Lean with constraints, Lean integration and kernel-checked LF proof search.