Set up Lean4 project scaffolding (Phase 0)

Establish the build system, project structure, test infrastructure,
and CI pipeline for the Lython Python interpreter.

Co-Authored-By: Claude Opus 4.6 (1M context) <noreply@anthropic.com>

Author: pirapira

.github/workflows/ci.yml

@@ -0,0 +1,13 @@
+name: CI
+on:
+  push:
+  pull_request:
+  workflow_dispatch:
+jobs:
+  build:
+    runs-on: ubuntu-latest
+    steps:
+      - uses: actions/checkout@v5
+      - uses: leanprover/lean-action@v1
+        with:
+          test: true

.gitignore

@@ -0,0 +1 @@
+/.lake

CLAUDE.md

@@ -0,0 +1,35 @@
+# Lython
+
+Python 3.12 interpreter in Lean4, targeting the leanSpec Ethereum consensus spec.
+
+## Build Commands
+
+- `lake build` — build the Lython library and executable
+- `lake test` — run tests (builds LythonTest driver; `#guard` failures = build errors)
+- `lake exe lython` — run the interpreter
+
+## Project Structure
+
+```
+Lython.lean          — umbrella import for the library
+Lython/
+  Lexer.lean         — tokenizer
+  Parser.lean        — PEG parser
+  AST.lean           — Python AST node types
+  Interpreter.lean   — tree-walking interpreter
+  Runtime.lean       — runtime support (types, exceptions, stdlib)
+Main.lean            — CLI entry point
+LythonTest.lean      — test driver root
+LythonTest/
+  Basic.lean         — smoke tests
+```
+
+## Code Style
+
+- `set_option autoImplicit false` at the top of every file
+- No trailing whitespace
+- Follow existing patterns in the codebase
+
+## Development Plan
+
+See `PLAN.md` for the full phased development plan.

Lython.lean

@@ -0,0 +1,5 @@
+import Lython.Lexer
+import Lython.Parser
+import Lython.AST
+import Lython.Interpreter
+import Lython.Runtime

Lython/AST.lean

@@ -0,0 +1,4 @@
+set_option autoImplicit false
+
+namespace Lython.AST
+end Lython.AST

Lython/Interpreter.lean

@@ -0,0 +1,4 @@
+set_option autoImplicit false
+
+namespace Lython.Interpreter
+end Lython.Interpreter

Lython/Lexer.lean

@@ -0,0 +1,4 @@
+set_option autoImplicit false
+
+namespace Lython.Lexer
+end Lython.Lexer

Lython/Parser.lean

@@ -0,0 +1,4 @@
+set_option autoImplicit false
+
+namespace Lython.Parser
+end Lython.Parser

Lython/Runtime.lean

@@ -0,0 +1,4 @@
+set_option autoImplicit false
+
+namespace Lython.Runtime
+end Lython.Runtime

LythonTest.lean

@@ -0,0 +1 @@
+import LythonTest.Basic