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

2.4 KiB

Raw Permalink Blame History

Typst documents tied to octive-lean

Typst sources for the m242 command-line diaries that demo octive-lean live outside this repo, in ~/.env/typst/m242/. The .m drivers in this repo's root produce the data each diary plots; the typst files compile to PDF and embed the plots, screenshots, and prose.

Typst file	PDF	Topic	Driver(s) in this repo
`~/.env/typst/m242/CLDiary.typ`	`CLDiary.pdf`	Polynomial interpolation: Runge phenomenon, least-squares fit, splines, Chebyshev nodes	`Lab7Interp.m`
`~/.env/typst/m242/CLDiary_Sym.typ`	`CLDiary_Sym.pdf`	Symbolic Math Toolbox walkthrough (28 cheat-sheet ops via SymPy bridge)	`SymToolboxDemo.m`
`~/.env/typst/m242/CLDiary_Sim.typ`	`CLDiary_Sim.pdf`	Simulink/Xcos: 4 dynamic systems with Xcos canvas screenshots + native fletcher diagrams + RK4 trajectories	`Sim_Gravity.m`, `Sim_VanDerPol.m`, `Sim_Lorenz.m`

Build

cd ~/.env/typst/m242
typst compile CLDiary.typ
typst compile CLDiary_Sym.typ
typst compile CLDiary_Sim.typ

Supporting assets (in `~/.env/typst/m242/`)

Path	What
`sim_data/*.csv`	Trajectories produced by `Sim_*.m`, loaded by `CLDiary_Sim.typ`
`screenshots/xcos_*.png`	Xcos canvas screenshots for `CLDiary_Sim.typ`
`xcos/*.zcos`	Scilab/Xcos diagram files (Lorenz, Bouncing_ball, gensin, pendulum, Inverted_pendulum, Colpitts, Boost_Converter)
`xcos/BUILD_DIAGRAMS.md`	How to build / screenshot each Xcos diagram

Regenerating sim_data

cd ~/.env/lean/octive-lean
lake exe octive-lean Sim_Gravity.m   | grep , > ~/.env/typst/m242/sim_data/gravity.csv
lake exe octive-lean Sim_VanDerPol.m | grep , > ~/.env/typst/m242/sim_data/vanderpol.csv
lake exe octive-lean Sim_Lorenz.m    | grep , > ~/.env/typst/m242/sim_data/lorenz.csv

Octive-lean features added for these diaries

polyfit, polyval, spline, linsolve — OctiveLean/Builtins.lean
OctiveLean/SymPyBridge.lean — persistent SymPy subprocess
25+ symbolic builtins (diff, int, subs, simplify, solve, taylor, dsolve, jacobian, hessian, laplacian, symsum, rewrite, resultant, series, isolate, lhs/rhs, latex, pretty, vpa, coeffs, collect, expand, factor, gradient, piecewise, symfun) — OctiveLean/Builtins.lean
Value.sym variant + binop overloading for symbolic operands — OctiveLean/Value.lean, OctiveLean/Eval.lean

2.4 KiB Raw Permalink Blame History