From 23162fb93aae28466c78de17256602ff54f287f5 Mon Sep 17 00:00:00 2001 From: Maximus Gorog Date: Wed, 29 Apr 2026 09:44:24 -0600 Subject: [PATCH] Add README, CONTRIBUTING, editorconfig, gitattributes, justfile Co-Authored-By: Claude Opus 4.7 (1M context) --- .editorconfig | 15 ++++++++++++++ .gitattributes | 19 ++++++++++++++++++ CONTRIBUTING.md | 53 +++++++++++++++++++++++++++++++++++++++++++++++++ README.md | 50 +++++++++++++++++++++++++++++++++++++++++++++- justfile | 24 ++++++++++++++++++++++ 5 files changed, 160 insertions(+), 1 deletion(-) create mode 100644 .editorconfig create mode 100644 .gitattributes create mode 100644 CONTRIBUTING.md create mode 100644 justfile diff --git a/.editorconfig b/.editorconfig new file mode 100644 index 0000000..4250a32 --- /dev/null +++ b/.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 diff --git a/.gitattributes b/.gitattributes new file mode 100644 index 0000000..d18fe83 --- /dev/null +++ b/.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 diff --git a/CONTRIBUTING.md b/CONTRIBUTING.md new file mode 100644 index 0000000..75c54d0 --- /dev/null +++ b/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. diff --git a/README.md b/README.md index 74f7f60..4952429 100644 --- a/README.md +++ b/README.md @@ -1 +1,49 @@ -# octive-lean \ No newline at end of file +# 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. diff --git a/justfile b/justfile new file mode 100644 index 0000000..7735c82 --- /dev/null +++ b/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