max/crosslang
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions
crosslang/octive-lean
History
Exact
Maximus Gorog 6592cd058d Add 'octive-lean/' from commit '4b6fcec565a170d7029d4ccba21be2ecd0512d13' 
git-subtree-dir: octive-lean
git-subtree-mainline: fd3d42ae33
git-subtree-split: 4b6fcec565
2026-05-12 02:59:14 -06:00
..
.github/workflows Add 'octive-lean/' from commit '4b6fcec565a170d7029d4ccba21be2ecd0512d13' 2026-05-12 02:59:14 -06:00
corpus Add 'octive-lean/' from commit '4b6fcec565a170d7029d4ccba21be2ecd0512d13' 2026-05-12 02:59:14 -06:00
docs Add 'octive-lean/' from commit '4b6fcec565a170d7029d4ccba21be2ecd0512d13' 2026-05-12 02:59:14 -06:00
OctiveLean Add 'octive-lean/' from commit '4b6fcec565a170d7029d4ccba21be2ecd0512d13' 2026-05-12 02:59:14 -06:00
widget/js Add 'octive-lean/' from commit '4b6fcec565a170d7029d4ccba21be2ecd0512d13' 2026-05-12 02:59:14 -06:00
.editorconfig Add 'octive-lean/' from commit '4b6fcec565a170d7029d4ccba21be2ecd0512d13' 2026-05-12 02:59:14 -06:00
.gitattributes Add 'octive-lean/' from commit '4b6fcec565a170d7029d4ccba21be2ecd0512d13' 2026-05-12 02:59:14 -06:00
.gitignore Add 'octive-lean/' from commit '4b6fcec565a170d7029d4ccba21be2ecd0512d13' 2026-05-12 02:59:14 -06:00
CONTRIBUTING.md Add 'octive-lean/' from commit '4b6fcec565a170d7029d4ccba21be2ecd0512d13' 2026-05-12 02:59:14 -06:00
CorpusCheck.lean Add 'octive-lean/' from commit '4b6fcec565a170d7029d4ccba21be2ecd0512d13' 2026-05-12 02:59:14 -06:00
justfile Add 'octive-lean/' from commit '4b6fcec565a170d7029d4ccba21be2ecd0512d13' 2026-05-12 02:59:14 -06:00
Lab7Interp.m Add 'octive-lean/' from commit '4b6fcec565a170d7029d4ccba21be2ecd0512d13' 2026-05-12 02:59:14 -06:00
lake-manifest.json Add 'octive-lean/' from commit '4b6fcec565a170d7029d4ccba21be2ecd0512d13' 2026-05-12 02:59:14 -06:00
lakefile.toml Add 'octive-lean/' from commit '4b6fcec565a170d7029d4ccba21be2ecd0512d13' 2026-05-12 02:59:14 -06:00
lean-toolchain Add 'octive-lean/' from commit '4b6fcec565a170d7029d4ccba21be2ecd0512d13' 2026-05-12 02:59:14 -06:00
Main.lean Add 'octive-lean/' from commit '4b6fcec565a170d7029d4ccba21be2ecd0512d13' 2026-05-12 02:59:14 -06:00
NumericalTutorial.lean Add 'octive-lean/' from commit '4b6fcec565a170d7029d4ccba21be2ecd0512d13' 2026-05-12 02:59:14 -06:00
OctiveLean.lean Add 'octive-lean/' from commit '4b6fcec565a170d7029d4ccba21be2ecd0512d13' 2026-05-12 02:59:14 -06:00
PlotDemo.lean Add 'octive-lean/' from commit '4b6fcec565a170d7029d4ccba21be2ecd0512d13' 2026-05-12 02:59:14 -06:00
README.md Add 'octive-lean/' from commit '4b6fcec565a170d7029d4ccba21be2ecd0512d13' 2026-05-12 02:59:14 -06:00
RosettaStone.lean Add 'octive-lean/' from commit '4b6fcec565a170d7029d4ccba21be2ecd0512d13' 2026-05-12 02:59:14 -06:00
Sim_Gravity.m Add 'octive-lean/' from commit '4b6fcec565a170d7029d4ccba21be2ecd0512d13' 2026-05-12 02:59:14 -06:00
Sim_Lorenz.m Add 'octive-lean/' from commit '4b6fcec565a170d7029d4ccba21be2ecd0512d13' 2026-05-12 02:59:14 -06:00
Sim_VanDerPol.m Add 'octive-lean/' from commit '4b6fcec565a170d7029d4ccba21be2ecd0512d13' 2026-05-12 02:59:14 -06:00
SymToolboxDemo.m Add 'octive-lean/' from commit '4b6fcec565a170d7029d4ccba21be2ecd0512d13' 2026-05-12 02:59:14 -06:00
tutorial.m Add 'octive-lean/' from commit '4b6fcec565a170d7029d4ccba21be2ecd0512d13' 2026-05-12 02:59:14 -06:00

README.md

octive-lean

A Lean 4 reimplementation of GNU Octave — the MATLAB-compatible numerical language — aiming to be more versatile than upstream.

Build

lake build

Requires the Lean toolchain pinned in lean-toolchain. elan will pick it up automatically.

Run

# 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

lake build && lake exe corpus-check

Pass --update to regenerate .expected files after intentional behavior changes.