commit 2173e196fed15aecccccc46d74c8a4175d0bfc95 Author: Maximus Gorog Date: Sun May 10 02:12:19 2026 -0600 Initial scaffold: Lean 4 reimplementation of Go. Mirrors the layout of octive-lean: lakefile, justfile, gitignored upstream clone, a top-level library module, and a Main entry point that switches between REPL and file execution. Module skeleton in GolangLean/: Token, AST — real ports of go/token and go/ast Scanner, Parser — stubs throwing notImpl, point at upstream Value, Env, Error — runtime data shapes Eval, Builtins, REPL — stubs that compile and run as a placeholder PureEval, BigStep, ValueEquiv — formal-semantics layer (mirroring octive-lean) where cross-language proof eventually lives. The proof layer is shaped identically to octive-lean's so that theorems about Go semantics will share their form with the Octave ones — that shared shape is the candidate for the future cross-language core. Upstream reference go-upstream/ (shallow clone of golang/go) is gitignored. diff --git a/.gitignore b/.gitignore new file mode 100644 index 0000000..871d475 --- /dev/null +++ b/.gitignore @@ -0,0 +1,2 @@ +/.lake +/go-upstream diff --git a/CorpusCheck.lean b/CorpusCheck.lean new file mode 100644 index 0000000..591a214 --- /dev/null +++ b/CorpusCheck.lean @@ -0,0 +1,9 @@ +import GolangLean + +/-! Corpus driver — runs every `.go` script under `corpus/` and compares +the captured stdout to the matching `.expected` file. Mirrors octive-lean's +`CorpusCheck`. Currently a no-op until the interpreter exists. -/ + +def main (_args : List String) : IO UInt32 := do + IO.println "golang-lean corpus-check: no corpus yet (interpreter is a scaffold)" + return 0 diff --git a/GolangLean.lean b/GolangLean.lean new file mode 100644 index 0000000..aaf57ef --- /dev/null +++ b/GolangLean.lean @@ -0,0 +1,13 @@ +import GolangLean.Error +import GolangLean.Token +import GolangLean.AST +import GolangLean.Value +import GolangLean.Env +import GolangLean.Scanner +import GolangLean.Parser +import GolangLean.Eval +import GolangLean.Builtins +import GolangLean.REPL +import GolangLean.PureEval +import GolangLean.BigStep +import GolangLean.ValueEquiv diff --git a/GolangLean/AST.lean b/GolangLean/AST.lean new file mode 100644 index 0000000..eb974d0 --- /dev/null +++ b/GolangLean/AST.lean @@ -0,0 +1,119 @@ +import GolangLean.Token + +namespace GolangLean + +/-! # Go AST — mirrors `go/ast/ast.go`. + +The Go reference parser produces nodes from three primary categories: +`Expr`, `Stmt`, `Decl`. We mirror that structure here. The point of mirroring +is that proofs and translations can refer to nodes by the same names that +Go programmers use, and so the eventual cross-language layer can compare +shapes apples-to-apples with octive-lean's `Expr/Stmt`. -/ + +/-! ## Operator categories (subsets of `Tok`) -/ + +inductive BinOp where + | add | sub | mul | quo | rem + | and | or | xor | shl | shr | andNot + | land | lor + | eql | neq | lss | leq | gtr | geq + deriving Repr, BEq, Inhabited + +inductive UnOp where + | plus | minus | not | xor | mul -- `*p` (deref) + | and -- `&v` (addr-of) + | arrow -- `<-ch` (recv) + deriving Repr, BEq, Inhabited + +/-! ## Channel direction (for `chan T`, `<-chan T`, `chan<- T`) -/ + +inductive ChanDir where + | send | recv | both + deriving Repr, BEq, Inhabited + +/-! ## AST nodes (mutually recursive: Expr ↔ Stmt ↔ Decl ↔ Type) -/ + +mutual + + /-- A Go expression. Types are also expressions in Go's grammar. -/ + inductive Expr where + | bad + | ident : String → Expr + | intLit : Int → Expr + | floatLit : Float → Expr + | stringLit : String → Expr + | charLit : Char → Expr + | imagLit : Float → Expr + | binOp : BinOp → Expr → Expr → Expr + | unOp : UnOp → Expr → Expr + | call : Expr → Array Expr → Bool → Expr -- f(args), variadic? + | selector : Expr → String → Expr -- x.Sel + | index : Expr → Expr → Expr -- x[i] + | slice : Expr → Option Expr → Option Expr → Option Expr → Expr -- x[lo:hi:max] + | typeAssert : Expr → Option Expr → Expr -- x.(T) (T = none for x.(type)) + | star : Expr → Expr -- *T or *p + | paren : Expr → Expr + | composite : Option Expr → Array Expr → Expr -- T{elts...} + | keyValue : Expr → Expr → Expr -- key: value (in composite) + | funcLit : FuncType → Array Stmt → Expr -- func(...) ... { ... } + | arrayType : Option Expr → Expr → Expr -- [N]T or [...]T (none = ...) + | sliceType : Expr → Expr -- []T + | mapType : Expr → Expr → Expr -- map[K]V + | chanType : ChanDir → Expr → Expr -- chan T / <-chan T / chan<- T + | structType : Array Field → Expr -- struct{ ... } + | interfaceType : Array Field → Expr -- interface{ ... } + | ellipsis : Option Expr → Expr -- ...T (variadic param / array len) + + /-- A struct field or method signature in an interface. -/ + inductive Field where + | mk : Array String → Expr → Option String → Field -- names, type, tag + + /-- A function-type expression: parameters and results. -/ + inductive FuncType where + | mk : Array Field → Array Field → FuncType -- params, results + + /-- A Go statement. -/ + inductive Stmt where + | bad + | declS : Decl → Stmt + | empty : Stmt + | labeled : String → Stmt → Stmt + | exprS : Expr → Stmt + | sendS : Expr → Expr → Stmt -- ch <- x + | incDec : Expr → Bool → Stmt -- x++ / x-- (true = inc) + | assignS : Array Expr → Tok → Array Expr → Stmt -- lhs op rhs (op ∈ {=, :=, +=, ...}) + | goS : Expr → Stmt -- go f(...) + | deferS : Expr → Stmt -- defer f(...) + | returnS : Array Expr → Stmt + | branchS : Tok → Option String → Stmt -- break/continue/goto/fallthrough + | block : Array Stmt → Stmt + | ifS : Option Stmt → Expr → Array Stmt → Option Stmt → Stmt + | switchS : Option Stmt → Option Expr → Array Stmt → Stmt + | typeSwitch : Option Stmt → Stmt → Array Stmt → Stmt + | caseClause : Array Expr → Array Stmt → Stmt + | selectS : Array Stmt → Stmt + | commClause : Option Stmt → Array Stmt → Stmt + | forS : Option Stmt → Option Expr → Option Stmt → Array Stmt → Stmt + | rangeS : Option Expr → Option Expr → Tok → Expr → Array Stmt → Stmt -- key,val := range x + + /-- A top-level or block-scoped declaration. -/ + inductive Decl where + | bad + | importD : Array (Option String × String) → Decl -- (alias, path) + | constD : Array (Array String × Option Expr × Array Expr) → Decl -- (names, type?, values) + | varD : Array (Array String × Option Expr × Array Expr) → Decl + | typeD : Array (String × Expr × Bool) → Decl -- (name, type, isAlias) + | funcD : Option Field → String → FuncType → Option (Array Stmt) → Decl + -- receiver?, name, signature, body? (none = forward decl in interface) + +end + +/-! ## File / Package -/ + +structure GoFile where + pkg : String + imports : Array (Option String × String) + decls : Array Decl + deriving Inhabited + +end GolangLean diff --git a/GolangLean/BigStep.lean b/GolangLean/BigStep.lean new file mode 100644 index 0000000..c5a132d --- /dev/null +++ b/GolangLean/BigStep.lean @@ -0,0 +1,21 @@ +import GolangLean.PureEval + +namespace GolangLean + +/-! # Big-step operational semantics. + +Mirror of octive-lean's `BigStep`. An inductive relation +`BigStepExpr : Env → Expr → Value → Env → Prop` that serves as the formal +specification of Go semantics, independent of the executable evaluator. + +This is the layer where cross-language proof becomes possible: theorems +stated about `BigStepExpr` for Go should look identical in shape to the +Octave version. The shared shape is the candidate for a language-generic +core. + +Stub. Constructors will be added one syntactic form at a time. -/ + +inductive BigStepExpr : Env → Expr → Value → Env → Prop where + | placeholder : BigStepExpr env e v env -- delete once real rules exist + +end GolangLean diff --git a/GolangLean/Builtins.lean b/GolangLean/Builtins.lean new file mode 100644 index 0000000..56fe2e2 --- /dev/null +++ b/GolangLean/Builtins.lean @@ -0,0 +1,18 @@ +import GolangLean.Value +import GolangLean.Env + +namespace GolangLean + +/-! # Built-in functions and the predeclared identifiers. + +Two layers in Go: + * Predeclared identifiers (`true`, `false`, `nil`, `iota`, basic types) — values. + * Built-in functions (`len`, `cap`, `make`, `new`, `append`, `copy`, `delete`, + `panic`, `recover`, `print`, `println`) — special forms in the spec. + * `fmt.*` and friends are *not* builtins; they live in package `fmt`. + +Stub for now. -/ + +def emptyBuiltinTable : List (String × (Array Value → IO (Except String Value))) := [] + +end GolangLean diff --git a/GolangLean/Env.lean b/GolangLean/Env.lean new file mode 100644 index 0000000..fb0d051 --- /dev/null +++ b/GolangLean/Env.lean @@ -0,0 +1,37 @@ +import GolangLean.Value + +namespace GolangLean + +/-! # Environment / heap. + +Distinct from octive-lean's flat `Env`: Go has lexically-nested scopes, +addressable variables (so a `&x` produces a stable heap index), and a +package-level namespace. This is a placeholder shape; flesh out as needed. -/ + +abbrev Frame := List (String × Value) + +structure Env where + frames : List Frame -- top of list = innermost scope + package : List (String × Value) -- package-level decls + heap : Array Value -- addressable cells (`&x` returns an index) + builtins : List (String × (Array Value → IO (Except String Value))) + deriving Inhabited + +namespace Env + +def empty : Env := + { frames := [[]], package := [], heap := #[], builtins := [] } + +/-- Look up a name: innermost frame first, then package, then builtins (later). -/ +def lookup (env : Env) (name : String) : Option Value := + let rec go : List Frame → Option Value + | [] => env.package.lookup name + | f :: fs => + match f.lookup name with + | some v => some v + | none => go fs + go env.frames + +end Env + +end GolangLean diff --git a/GolangLean/Error.lean b/GolangLean/Error.lean new file mode 100644 index 0000000..ba02c2c --- /dev/null +++ b/GolangLean/Error.lean @@ -0,0 +1,27 @@ +namespace GolangLean + +/-- Runtime / static errors produced anywhere in the Go toolchain. -/ +inductive GoError where + | scan (msg : String) (line col : Nat) -- lexical + | parse (msg : String) (line col : Nat) -- syntactic + | typeErr (msg : String) -- static type-check + | runtime (msg : String) -- panic / runtime + | nilDeref -- nil-pointer dereference + | indexOOB (i n : Int) -- index out of range + | divByZero + | notImpl (what : String) -- placeholder for stubs + deriving Repr, Inhabited + +def GoError.toString : GoError → String + | .scan m l c => s!"scan error: {m} ({l}:{c})" + | .parse m l c => s!"parse error: {m} ({l}:{c})" + | .typeErr m => s!"type error: {m}" + | .runtime m => s!"runtime error: {m}" + | .nilDeref => "runtime error: nil pointer dereference" + | .indexOOB i n => s!"runtime error: index out of range [{i}] with length {n}" + | .divByZero => "runtime error: integer divide by zero" + | .notImpl what => s!"not implemented: {what}" + +instance : ToString GoError := ⟨GoError.toString⟩ + +end GolangLean diff --git a/GolangLean/Eval.lean b/GolangLean/Eval.lean new file mode 100644 index 0000000..4cf36d6 --- /dev/null +++ b/GolangLean/Eval.lean @@ -0,0 +1,25 @@ +import GolangLean.AST +import GolangLean.Env +import GolangLean.Error + +namespace GolangLean + +/-! # Evaluator — operational big-step interpreter over the AST. + +Mirror of octive-lean's `Eval`. Monad stack `ExceptT GoError (StateT Env IO)`, +chosen for the same reason: state survives non-local control flow (defer, +panic, goroutine spawn) carried as exceptions. -/ + +abbrev EvalM := ExceptT GoError (StateT Env IO) + +partial def evalExpr (_e : Expr) : EvalM Value := + throw (.notImpl "Eval.evalExpr") + +partial def evalStmt (_s : Stmt) : EvalM Unit := + throw (.notImpl "Eval.evalStmt") + +def runFile (path : String) : IO UInt32 := do + IO.eprintln s!"golang-lean: would execute {path} (interpreter not yet implemented)" + return 1 + +end GolangLean diff --git a/GolangLean/Parser.lean b/GolangLean/Parser.lean new file mode 100644 index 0000000..7c57d11 --- /dev/null +++ b/GolangLean/Parser.lean @@ -0,0 +1,16 @@ +import GolangLean.Scanner +import GolangLean.AST + +namespace GolangLean + +/-! # Parser — port of `go/parser/parser.go`. + +Stub. Recursive-descent over the token stream. We mirror upstream: each +non-terminal in the Go spec corresponds to one `parseX` function, named +identically. -/ + +partial def parseFile (src : String) : Except GoError GoFile := do + let _toks ← scan src + .error (.notImpl "Parser.parseFile: see go-upstream/src/go/parser/parser.go") + +end GolangLean diff --git a/GolangLean/PureEval.lean b/GolangLean/PureEval.lean new file mode 100644 index 0000000..268d343 --- /dev/null +++ b/GolangLean/PureEval.lean @@ -0,0 +1,18 @@ +import GolangLean.AST +import GolangLean.Value +import GolangLean.Env + +namespace GolangLean + +/-! # Pure (non-IO) evaluator. + +Mirror of octive-lean's `PureEval`. Strips IO so that the evaluator becomes +a `def` (not `partial def`) over a finite fuel parameter, suitable for +reasoning. The relationship to `Eval.evalExpr` is captured by `ValueEquiv`. + +Stub for now — fill in once `Eval` is non-trivial. -/ + +def evalExprP (_fuel : Nat) (_env : Env) (_e : Expr) : Option (Value × Env) := + none + +end GolangLean diff --git a/GolangLean/REPL.lean b/GolangLean/REPL.lean new file mode 100644 index 0000000..9f33ea8 --- /dev/null +++ b/GolangLean/REPL.lean @@ -0,0 +1,24 @@ +import GolangLean.Eval + +namespace GolangLean + +/-! # REPL — placeholder. + +Go has no official REPL, but `gore` and `yaegi` show it is feasible: each +input is wrapped into a fresh `func main()` body or evaluated as a statement +sequence inside a persistent package-scope. We follow the latter approach. -/ + +partial def runREPL : IO Unit := do + IO.println "golang-lean v0.1 — interpreter scaffold (REPL not yet implemented)" + IO.println "Type Ctrl-D to exit." + let stdin ← IO.getStdin + let rec loop : IO Unit := do + IO.print "go> " + (← IO.getStdout).flush + let line ← stdin.getLine + if line.isEmpty then return () + IO.println s!" parsed: {line.trimAscii} (stub)" + loop + loop + +end GolangLean diff --git a/GolangLean/Scanner.lean b/GolangLean/Scanner.lean new file mode 100644 index 0000000..30a916a --- /dev/null +++ b/GolangLean/Scanner.lean @@ -0,0 +1,18 @@ +import GolangLean.Token +import GolangLean.Error + +namespace GolangLean + +/-! # Scanner — port of `go/scanner/scanner.go`. + +Stub. The real implementation is a hand-written DFA over UTF-8 byte input, +faithful to the upstream Go scanner. We start with a `notImpl` sentinel so +the project compiles, then fill in token-by-token alongside the parser. -/ + +partial def scan (src : String) : Except GoError (Array Token) := do + if src.isEmpty then + return #[⟨.eof, ⟨1, 1, 0⟩⟩] + else + .error (.notImpl "Scanner.scan: see go-upstream/src/go/scanner/scanner.go") + +end GolangLean diff --git a/GolangLean/Token.lean b/GolangLean/Token.lean new file mode 100644 index 0000000..eefefdb --- /dev/null +++ b/GolangLean/Token.lean @@ -0,0 +1,82 @@ +namespace GolangLean + +/-! # Token kinds — mirrors `go/token/token.go`. + +This is a faithful Lean port of the Go reference scanner's token enumeration. +Comments next to each constructor cite the Go name where it differs in casing +or spelling. Source: `go-upstream/src/go/token/token.go`. -/ + +inductive Tok where + -- Special + | illegal + | eof + | comment + -- Literals (carry their lexeme) + | ident (s : String) + | intLit (s : String) + | floatLit (s : String) + | imagLit (s : String) + | charLit (s : String) + | stringLit (s : String) + -- Operators & punctuation + | add | sub | mul | quo | rem + | and | or | xor | shl | shr | andNot + | addAssign | subAssign | mulAssign | quoAssign | remAssign + | andAssign | orAssign | xorAssign | shlAssign | shrAssign | andNotAssign + | landTok | lorTok | arrow | inc | dec + | eql | lss | gtr | assign | not + | neq | leq | geq | define | ellipsis + | lparen | lbrack | lbrace | comma | period + | rparen | rbrack | rbrace | semicolon | colon + -- Keywords + | breakK | caseK | chanK | constK | continueK + | defaultK | deferK | elseK | fallthroughK | forK + | funcK | goK | gotoK | ifK | importK + | interfaceK | mapK | packageK | rangeK | returnK + | selectK | structK | switchK | typeK | varK + -- Tilde introduced for generics (Go 1.18) + | tilde + deriving Repr, BEq, Inhabited + +/-- Source-position metadata attached to a token. -/ +structure Pos where + line : Nat + col : Nat + off : Nat + deriving Repr, BEq, Inhabited + +structure Token where + tok : Tok + pos : Pos + deriving Repr, Inhabited + +/-- Map a keyword spelling to its token, or `none` if it is just an identifier. -/ +def keyword? : String → Option Tok + | "break" => some .breakK + | "case" => some .caseK + | "chan" => some .chanK + | "const" => some .constK + | "continue" => some .continueK + | "default" => some .defaultK + | "defer" => some .deferK + | "else" => some .elseK + | "fallthrough" => some .fallthroughK + | "for" => some .forK + | "func" => some .funcK + | "go" => some .goK + | "goto" => some .gotoK + | "if" => some .ifK + | "import" => some .importK + | "interface" => some .interfaceK + | "map" => some .mapK + | "package" => some .packageK + | "range" => some .rangeK + | "return" => some .returnK + | "select" => some .selectK + | "struct" => some .structK + | "switch" => some .switchK + | "type" => some .typeK + | "var" => some .varK + | _ => none + +end GolangLean diff --git a/GolangLean/Value.lean b/GolangLean/Value.lean new file mode 100644 index 0000000..b76789b --- /dev/null +++ b/GolangLean/Value.lean @@ -0,0 +1,34 @@ +import GolangLean.AST + +namespace GolangLean + +/-! # Runtime values. + +Go is statically typed, so a faithful runtime keeps a `GoType` alongside each +value. For the first cut we keep things untyped (a tagged union) and recover +type safety later by adding a static type-checker pass on the AST. The shape +mirrors octive-lean's `Value`. -/ + +mutual + + inductive Value where + | nil + | boolV : Bool → Value + | intV : Int → Value + | floatV : Float → Value + | stringV : String → Value + | sliceV : Array Value → Value + | mapV : Array (Value × Value) → Value -- ordered list, equality via key + | structV : Array (String × Value) → Value + | ptrV : Nat → Value -- index into heap + | funcV : Closure → Value + | chanV : Nat → Value -- index into channel table + | tupleV : Array Value → Value -- multi-return packs + + /-- A function closure: signature + body + captured environment. -/ + inductive Closure where + | mk : FuncType → Array Stmt → List (String × Value) → Closure + +end + +end GolangLean diff --git a/GolangLean/ValueEquiv.lean b/GolangLean/ValueEquiv.lean new file mode 100644 index 0000000..40e1841 --- /dev/null +++ b/GolangLean/ValueEquiv.lean @@ -0,0 +1,17 @@ +import GolangLean.PureEval +import GolangLean.BigStep + +namespace GolangLean + +/-! # Equivalence between evaluators. + +Mirror of octive-lean's `ValueEquiv`. The theorem to prove is: + + `evalExprP fuel env e = some (v, env') ↔ BigStepExpr env e v env'` + (modulo fuel being large enough) + +This bridge is what lets us *use* the executable evaluator inside proofs: +once `evalExprP` is shown to compute the same relation as `BigStepExpr`, +running the interpreter is itself a proof. Stub. -/ + +end GolangLean diff --git a/Main.lean b/Main.lean new file mode 100644 index 0000000..b23b434 --- /dev/null +++ b/Main.lean @@ -0,0 +1,10 @@ +import GolangLean + +open GolangLean in +def main (args : List String) : IO UInt32 := do + match args with + | [] => runREPL; return 0 + | [path] => runFile path + | _ => + IO.eprintln "Usage: golang-lean [script.go]" + return 1 diff --git a/README.md b/README.md new file mode 100644 index 0000000..9464fe7 --- /dev/null +++ b/README.md @@ -0,0 +1,64 @@ +# golang-lean + +A Lean 4 reimplementation of the [Go programming language](https://go.dev/) — using the upstream reference compiler/parser as the source of truth, the way `octive-lean` uses GNU Octave. + +Built parallel to `octive-lean`. Goals: + +1. **Working Go interpreter** for a useful subset (start: pure Go, no goroutines). +2. **Formal semantics** layered on top: `BigStep` / `PureEval` / `ValueEquiv` so proofs about Go programs are first-class. +3. **Cross-language layer** — once both this and `octive-lean` have a real evaluator and big-step semantics, factor a shared core out of two concrete points rather than guessing the abstraction in advance. + +## Build + +```sh +lake build +``` + +Requires the Lean toolchain pinned in [`lean-toolchain`](lean-toolchain). [`elan`](https://github.com/leanprover/elan) will pick it up automatically. + +## Run + +```sh +# REPL stub +lake exe golang-lean + +# Run a .go script (not yet implemented) +lake exe golang-lean path/to/script.go + +# Verify the corpus against expected outputs +lake build corpus-check +lake exe corpus-check +``` + +## Layout + +| Path | What's there | +| --- | --- | +| `GolangLean/` | Library: `Token`, `Scanner`, `AST`, `Parser`, `Value`, `Env`, `Eval`, `Builtins`, `REPL`, `BigStep`, `PureEval`, `ValueEquiv`, `Error` | +| `Main.lean` | Entry point — REPL or file runner | +| `CorpusCheck.lean` | Test driver for `corpus/` | +| `corpus/` | `.go` test cases paired with `.expected` outputs | +| `go-upstream/` | Shallow clone of `golang/go` (gitignored, used as reference) | + +## Status + +**Scaffold.** Module skeleton in place. `Token` and `AST` are real ports of `go/token` and `go/ast`. Scanner / Parser / Eval are stubs that throw `notImpl` so the project compiles. + +Next: +1. Implement `Scanner.scan` against `go-upstream/src/go/scanner/scanner.go`. +2. Implement `Parser.parseFile` recursive-descent against `go-upstream/src/go/parser/parser.go`. +3. Implement `Eval` for the pure subset (no goroutines, no defer, no panic/recover). +4. Mirror octive-lean's `BigStep` / `ValueEquiv` triple. + +## Reference + +`go-upstream/` is a shallow clone of `https://github.com/golang/go`. Key paths: + +| Path | What's there | +| --- | --- | +| `go-upstream/src/go/token/` | Token kinds, position tracking | +| `go-upstream/src/go/scanner/` | Lexer | +| `go-upstream/src/go/ast/` | AST node types | +| `go-upstream/src/go/parser/` | Recursive-descent parser | +| `go-upstream/src/go/types/` | Type-checker (later) | +| `go-upstream/src/runtime/` | Runtime / scheduler / GC (much later) | diff --git a/corpus/.gitkeep b/corpus/.gitkeep new file mode 100644 index 0000000..e69de29 diff --git a/justfile b/justfile new file mode 100644 index 0000000..fc876e7 --- /dev/null +++ b/justfile @@ -0,0 +1,24 @@ +# Common project tasks. Run `just` to list. + +default: + @just --list + +build: + lake build + +repl: + lake exe golang-lean + +run script: + lake exe golang-lean {{script}} + +test: + lake build && lake exe corpus-check + +update-corpus: + lake build && lake exe corpus-check --update + +clean: + lake clean + +fresh: clean build diff --git a/lake-manifest.json b/lake-manifest.json new file mode 100644 index 0000000..ce3ab12 --- /dev/null +++ b/lake-manifest.json @@ -0,0 +1,6 @@ +{"version": "1.2.0", + "packagesDir": ".lake/packages", + "packages": [], + "name": "«golang-lean»", + "lakeDir": ".lake", + "fixedToolchain": false} diff --git a/lakefile.toml b/lakefile.toml new file mode 100644 index 0000000..412895e --- /dev/null +++ b/lakefile.toml @@ -0,0 +1,14 @@ +name = "golang-lean" +version = "0.1.0" +defaultTargets = ["golang-lean"] + +[[lean_lib]] +name = "GolangLean" + +[[lean_exe]] +name = "golang-lean" +root = "Main" + +[[lean_exe]] +name = "corpus-check" +root = "CorpusCheck" diff --git a/lean-toolchain b/lean-toolchain new file mode 100644 index 0000000..6c7e31f --- /dev/null +++ b/lean-toolchain @@ -0,0 +1 @@ +leanprover/lean4:v4.30.0-rc2