python-of-lean

A Lean 4 implementation of Python semantics based on the lambda-py (λπ) formalization.

Overview

This project implements a Python interpreter in Lean 4 using the lambda-py semantics. It uses Racket's lambda-py as a frontend (parser + desugarer) and Lean as the execution backend.

Python Source (.py)
       ↓
[Racket: parse + desugar]  → S-expression
       ↓
[Lean: Parse S-expr]       → Expr AST
       ↓
[Lean: Interpreter]        → Result

Prerequisites

• Lean 4 (see lean-toolchain for version)
• Racket with the lambda-py dependencies

Building

lake build

Usage

Run a Python file

lake exe python-of-lean --run <file.py>

Evaluate Python code directly

lake exe python-of-lean --eval "print(1 + 2)"

Parse and inspect

# Show the Expr AST for a Python file
lake exe python-of-lean --parse <file.py>

# Parse an S-expression file directly
lake exe python-of-lean --parse-sexp <file.sexp>

Running Tests

lake exe test-runner

This discovers all .py files in the Tests/ directory, runs them through the interpreter, and compares output against corresponding .expected files.

Project Structure

python-of-lean/
├── Main.lean                    # CLI entry point
├── PythonOfLean.lean            # Library root (imports all modules)
├── PythonOfLean/
│   ├── Syntax/
│   │   └── Expr.lean            # Core AST types (Expr, Val, MetaVal, etc.)
│   ├── Semantics/
│   │   ├── Store.lean           # Memory store, environment, and state
│   │   ├── Builtins.lean        # Built-in functions and types
│   │   ├── Interp.lean          # Big-step interpreter
│   │   ├── Step.lean            # Small-step semantics
│   │   ├── Subst.lean           # Substitution operations
│   │   └── Context.lean         # Evaluation contexts
│   ├── Parser/
│   │   ├── SExpr.lean           # S-expression parser
│   │   ├── SExprToExpr.lean     # S-expr to Expr conversion
│   │   ├── Racket.lean          # Racket integration (spawns lambda-py)
│   │   └── Tests.lean           # Parser tests
│   └── Examples/
│       ├── Basic.lean           # Example programs as Expr values
│       └── Utils.lean           # Result formatting utilities
├── Tests/
│   ├── Main.lean                # Test runner
│   ├── *.py                     # Python test files
│   └── *.expected               # Expected outputs
├── scripts/
│   └── python-to-sexp.rkt       # Racket script for parsing Python
└── lambda-py/                   # Lambda-py submodule (Racket)

Supported Features

• Arithmetic operations (+, -, *, /, %)
• Comparison operators (<, >, <=, >=, ==, !=)
• Boolean operations (and, or, not)
• Variables and assignment
• Control flow (if/else, while, break, continue)
• Functions (definition, calls, recursion, varargs)
• Print function
• Basic types: integers, strings, booleans, None, lists, tuples

Known Issues in Lambda-py

Short-circuit evaluation bug

Lambda-py has a bug in its desugaring of boolean operators (and, or) that causes the first operand to be evaluated twice when it determines the result.

Location: lambda-py/base/python-desugar.rkt, lines 24-29

The desugar-boolop function desugars a and b to (if a then b else a) and a or b to (if a then a else b). This duplicates the expression a in both the condition and a branch, causing any side effects in a to execute twice.

To reproduce:

Create a test file Tests/short_circuit.py:

def f():
    print("f called")
    return 0

result = f() or True
print(result)

Expected output (standard Python behavior):

f called
True

Actual output (both Lean and Racket interpreters):

f called
f called
True

Reproduce with Racket interpreter:

cd lambda-py && racket base/python-main.rkt --interp < ../Tests/short_circuit.py

Reproduce with Lean interpreter:

lake exe python-of-lean --run Tests/short_circuit.py

References

• An Executable Semantics for Python - The lambda-py paper
• brownplt/lambda-py - Lambda-py repository