VeIR is a compiler infrastructure written in Lean that offers both an MLIR-style imperative design and (optional) ITP-level verification. VeIR connects with MLIR via the MLIR textual format, making it easy to combine MLIR and VeIR tooling.
| VeIR Features | Complete | Verified |
|---|---|---|
| MLIR core data structures (block, operation, region) | ✅ | 🔒 |
| define dialects | ✅ (basic) | |
| pass infrastructure | ✅ | |
| peephole rewriter | ✅ | |
| peephole rewriter (declarative) | ||
| interpreter framework | ✅ |
Our testing framework is split into two parts: unit tests written in Lean and
FileCheck tests for the
command line tool veir-opt.
Run the unit tests with:
lake testFileCheck tests require uv to be installed.
First, install dependencies:
uv syncThen run the tests:
uv run lit Test/ -vlake exe run-benchmarks add-fold-worklist