Add README, CONTRIBUTING, editorconfig, gitattributes, justfile

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

.editorconfig

@@ -0,0 +1,15 @@
+root = true
+
+[*]
+charset = utf-8
+end_of_line = lf
+indent_style = space
+indent_size = 2
+insert_final_newline = true
+trim_trailing_whitespace = true
+
+[*.md]
+trim_trailing_whitespace = false
+
+[Makefile]
+indent_style = tab

.gitattributes

@@ -0,0 +1,19 @@
+* text=auto eol=lf
+
+*.lean         text
+*.toml         text
+*.md           text
+*.m            text
+*.expected     text
+*.yml          text
+*.json         text
+*.js           text
+
+*.png          binary
+*.jpg          binary
+*.svg          text
+
+# Hide vendored & generated paths from diffs and language stats
+octave-upstream/  linguist-vendored linguist-generated
+.lake/            linguist-generated
+widget/js/        linguist-vendored

CONTRIBUTING.md

@@ -0,0 +1,53 @@
+# Contributing to octive-lean
+
+## Module map
+
+| Module | Purpose |
+| --- | --- |
+| `OctiveLean.AST` | Concrete + abstract syntax (statements, expressions, lvalues) |
+| `OctiveLean.Lexer` | Tokenizer — mirrors `octave-upstream/libinterp/parse-tree/lex.ll` |
+| `OctiveLean.Parser` | Parser — mirrors `octave-upstream/libinterp/parse-tree/oct-parse.yy` |
+| `OctiveLean.Value` | Runtime values: scalar, matrix, cell, struct, function handle |
+| `OctiveLean.Env` | Variable scopes, frames, builtin registry |
+| `OctiveLean.Eval` | Big-step evaluator over the AST |
+| `OctiveLean.Builtins` | Built-in functions (`sum`, `sin`, `printf`, …) |
+| `OctiveLean.REPL` | Interactive line reader |
+| `OctiveLean.PlotData`/`PlotSVG`/`PlotWidget` | Plotting backend |
+| `OctiveLean.BigStep`/`PureEval`/`ValueEquiv` | Semantic specs / proofs |
+| `OctiveLean.Corpus` | Driver behind `corpus-check` |
+
+The monad stack is `ExceptT OctaveError (StateT Env IO)` — putting `StateT` outermost preserves variable state through `break`/`continue` exceptions.
+
+## Adding a builtin
+
+1. Add the implementation in `OctiveLean/Builtins.lean`.
+2. Register it in `Env.builtinRegistry` (`OctiveLean/Env.lean`).
+3. Add a corpus test (next section) exercising it.
+4. `just test` to verify.
+
+## Adding a corpus test
+
+Drop a pair into `corpus/`:
+
+```
+corpus/NN_my_feature.m         # Octave source
+corpus/NN_my_feature.expected  # expected stdout
+```
+
+Generate the expected file with:
+
+```sh
+just update-corpus
+```
+
+Inspect the diff — if the output looks right, commit both files.
+
+## Reference: GNU Octave upstream
+
+`octave-upstream/` is a shallow clone (gitignored) used as a reference. Key paths:
+
+- `octave-upstream/libinterp/parse-tree/` — flex/bison sources for the original parser
+- `octave-upstream/libinterp/corefcn/` — built-in function implementations
+- `octave-upstream/libinterp/octave-value/` — value system
+
+When adding a feature, check upstream's behavior first so the semantics match.

README.md

@@ -1 +1,49 @@
-# octive-lean
+# octive-lean
+
+A Lean 4 reimplementation of [GNU Octave](https://www.gnu.org/software/octave/) — the MATLAB-compatible numerical language — aiming to be more versatile than upstream.
+
+## 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
+lake exe octive-lean
+
+# Run an .m script
+lake exe octive-lean path/to/script.m
+
+# Verify the corpus against expected outputs
+lake build corpus-check
+lake exe corpus-check
+```
+
+## Layout
+
+| Path | What's there |
+| --- | --- |
+| `OctiveLean/` | Library: `Lexer`, `Parser`, `AST`, `Eval`, `Builtins`, `REPL`, `BigStep`, `PlotSVG`, … |
+| `Main.lean` | Entry point — REPL or file runner |
+| `CorpusCheck.lean` | Test driver for `corpus/` |
+| `corpus/` | `.m` test cases paired with `.expected` outputs |
+| `NumericalTutorial.lean`, `RosettaStone.lean` | Lean-side tutorials and Octave⇄Lean translations |
+| `PlotDemo.lean`, `widget/` | Plotting via ProofWidgets + SVG |
+| `octave-upstream/` | Shallow clone of GNU Octave (gitignored, used as reference) |
+
+## Status
+
+Working interpreter: matrices, arithmetic, control flow, functions (incl. recursion, closures, anonymous `@(x)`), cell arrays, structs, `printf`-family, REPL, file execution. See `corpus/` for what's covered.
+
+## Tests
+
+```sh
+lake build && lake exe corpus-check
+```
+
+Pass `--update` to regenerate `.expected` files after intentional behavior changes.

justfile

@@ -0,0 +1,24 @@
+# Common project tasks. Run `just` to list.
+
+default:
+    @just --list
+
+build:
+    lake build
+
+repl:
+    lake exe octive-lean
+
+run script:
+    lake exe octive-lean {{script}}
+
+test:
+    lake build && lake exe corpus-check
+
+update-corpus:
+    lake build && lake exe corpus-check --update
+
+clean:
+    lake clean
+
+fresh: clean build