2173e196fe
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.
64 lines
2.5 KiB
Markdown
64 lines
2.5 KiB
Markdown
# 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) |
|