Rename project from Lython to leanPython

Rename directories, files, namespaces, imports, and git remote URL.

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

Author: pirapira

CLAUDE.md

@@ -1,18 +1,18 @@
-# Lython
+# LeanPython
 
 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
+- `lake build` — build the LeanPython library and executable
+- `lake test` — run tests (builds LeanPythonTest driver; `#guard` failures = build errors)
+- `lake exe leanPython` — run the interpreter
 
 ## Project Structure
 
 ```
-Lython.lean          — umbrella import for the library
-Lython/
+LeanPython.lean          — umbrella import for the library
+LeanPython/
   Lexer.lean         — tokenizer entry point (imports sub-modules, exposes tokenize)
   Lexer/
     Types.lean       — SourcePos, SourceSpan, TokenKind, Token, LexError
@@ -46,8 +46,8 @@ Lython/
     Ops.lean         — Operator dispatch, truthiness, equality, comparison, iteration
     Builtins.lean    — Built-in function implementations (print, len, range, etc.)
 Main.lean            — CLI entry point (reads .py file, parses, interprets)
-LythonTest.lean      — test driver root
-LythonTest/
+LeanPythonTest.lean      — test driver root
+LeanPythonTest/
   Basic.lean         — lexer tests (keywords, operators, numbers, strings, indent)
   Parser.lean        — parser tests (expressions, statements, integration)
   Interpreter.lean   — interpreter tests (#eval-based, IO assertions)

LeanPython.lean

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

Lython/AST.lean LeanPython/AST.leanLython/AST.lean renamed to LeanPython/AST.lean

@@ -1,3 +1,3 @@
-import Lython.AST.Types
+import LeanPython.AST.Types
 
 set_option autoImplicit false

Lython/AST/Types.lean LeanPython/AST/Types.leanLython/AST/Types.lean renamed to LeanPython/AST/Types.lean

@@ -1,10 +1,10 @@
-import Lython.Lexer.Types
+import LeanPython.Lexer.Types
 
 set_option autoImplicit false
 
-namespace Lython.AST
+namespace LeanPython.AST
 
-open Lython.Lexer (SourceSpan)
+open LeanPython.Lexer (SourceSpan)
 
 /-- Binary operators for `Expr.binOp`. -/
 inductive BinOp where
@@ -384,4 +384,4 @@ end
 def dumpModule : Module → String
   | .module stmts => s!"Module({dumpList dumpStmt stmts})"
 
-end Lython.AST
+end LeanPython.AST

LeanPython/Interpreter.lean

@@ -0,0 +1,3 @@
+import LeanPython.Interpreter.Types
+import LeanPython.Interpreter.Eval
+import LeanPython.Interpreter.Core

Lython/Interpreter/Core.lean LeanPython/Interpreter/Core.leanLython/Interpreter/Core.lean renamed to LeanPython/Interpreter/Core.lean

@@ -1,14 +1,14 @@
-import Lython.Interpreter.Eval
-import Lython.Parser.Core
+import LeanPython.Interpreter.Eval
+import LeanPython.Parser.Core
 
 set_option autoImplicit false
 
-namespace Lython.Interpreter
+namespace LeanPython.Interpreter
 
-open Lython.AST (Module)
-open Lython.Runtime
-open Lython.Interpreter.Eval
-open Lython.Parser (parse)
+open LeanPython.AST (Module)
+open LeanPython.Runtime
+open LeanPython.Interpreter.Eval
+open LeanPython.Parser (parse)
 
 /-- Interpret a Python source string.
     Returns captured output lines on success, or an error message. -/
@@ -28,4 +28,4 @@ def interpret (source : String) : IO (Except String (List String)) := do
     | (.error (.control .continue_), _) =>
       return (.error "SyntaxError: 'continue' not properly in loop")
 
-end Lython.Interpreter
+end LeanPython.Interpreter

Lython/Interpreter/Eval.lean LeanPython/Interpreter/Eval.leanLython/Interpreter/Eval.lean renamed to LeanPython/Interpreter/Eval.lean

@@ -1,17 +1,17 @@
-import Lython.Runtime.Builtins
+import LeanPython.Runtime.Builtins
 import Std.Data.HashMap
 import Std.Data.HashSet
 
 set_option autoImplicit false
 
-namespace Lython.Interpreter.Eval
+namespace LeanPython.Interpreter.Eval
 
-open Lython.AST
-open Lython.Runtime
-open Lython.Runtime.Ops
-open Lython.Runtime.Builtins
-open Lython.Interpreter
-open Lython.Lexer (SourceSpan SourcePos)
+open LeanPython.AST
+open LeanPython.Runtime
+open LeanPython.Runtime.Ops
+open LeanPython.Runtime.Builtins
+open LeanPython.Interpreter
+open LeanPython.Lexer (SourceSpan SourcePos)
 
 -- ============================================================
 -- Helpers
@@ -1074,4 +1074,4 @@ partial def callSetMethod (ref : HeapRef) (method : String) (args : List Value)
 
 end
 
-end Lython.Interpreter.Eval
+end LeanPython.Interpreter.Eval

Lython/Interpreter/Types.lean LeanPython/Interpreter/Types.leanLython/Interpreter/Types.lean renamed to LeanPython/Interpreter/Types.lean

@@ -1,12 +1,12 @@
-import Lython.Runtime.Types
+import LeanPython.Runtime.Types
 import Std.Data.HashMap
 import Std.Data.HashSet
 
 set_option autoImplicit false
 
-namespace Lython.Interpreter
+namespace LeanPython.Interpreter
 
-open Lython.Runtime
+open LeanPython.Runtime
 
 -- ============================================================
 -- Control flow signals
@@ -318,4 +318,4 @@ def typeName : Value → String
   | .builtin _ => "builtin_function_or_method"
   | .ellipsis => "ellipsis"
 
-end Lython.Interpreter
+end LeanPython.Interpreter

LeanPython/Lexer.lean

@@ -0,0 +1,21 @@
+import LeanPython.Lexer.Types
+import LeanPython.Lexer.Keywords
+import LeanPython.Lexer.Operators
+import LeanPython.Lexer.State
+import LeanPython.Lexer.Char
+import LeanPython.Lexer.Indent
+import LeanPython.Lexer.Number
+import LeanPython.Lexer.StringLit
+import LeanPython.Lexer.Core
+
+set_option autoImplicit false
+
+namespace LeanPython.Lexer
+
+/-- Tokenize a Python source string into an array of tokens. -/
+def tokenize (source : String) : Except LexError (Array Token) :=
+  match lexAll.run (LexerState.initial source) with
+  | .ok (tokens, _) => .ok tokens
+  | .error err => .error err
+
+end LeanPython.Lexer

Lython/Lexer/Char.lean LeanPython/Lexer/Char.leanLython/Lexer/Char.lean renamed to LeanPython/Lexer/Char.lean

@@ -1,6 +1,6 @@
 set_option autoImplicit false
 
-namespace Lython.Lexer
+namespace LeanPython.Lexer
 
 /-- Is the character a valid Python identifier start? (ASCII subset) -/
 def isIdentStart (c : Char) : Bool :=
@@ -26,4 +26,4 @@ def isHexDigit (c : Char) : Bool :=
 def isHorizWhitespace (c : Char) : Bool :=
   c == ' ' || c == '\t' || c == '\x0C'
 
-end Lython.Lexer
+end LeanPython.Lexer