From 73106747619520dd99f0d4bcbe1640256d036d32 Mon Sep 17 00:00:00 2001 From: Alok Singh Date: Fri, 2 May 2025 04:01:23 -0400 Subject: [PATCH 01/38] feat: add Legend component wrapper and full line chart helper with legend (#plot : new demo) --- LeanPlot/Components.lean | 21 +++++++++++++++++++++ LeanPlot/Demos/LinearDemo.lean | 11 +++++++++++ LeanPlot/Legend.lean | 24 ++++++++++++++++++++++++ 3 files changed, 56 insertions(+) create mode 100644 LeanPlot/Demos/LinearDemo.lean create mode 100644 LeanPlot/Legend.lean diff --git a/LeanPlot/Components.lean b/LeanPlot/Components.lean index 14068e1..9a1f8eb 100644 --- a/LeanPlot/Components.lean +++ b/LeanPlot/Components.lean @@ -2,6 +2,7 @@ import ProofWidgets.Component.HtmlDisplay import ProofWidgets.Component.Recharts import LeanPlot.ToFloat import LeanPlot.Axis +import LeanPlot.Legend /-! # LeanPlot core components @@ -12,6 +13,7 @@ functions and visualise the result in Recharts with one call. open Lean ProofWidgets open ProofWidgets.Recharts (LineChart Line LineType) open LeanPlot.Axis +open LeanPlot.Legend (Legend) open scoped ProofWidgets.Jsx namespace LeanPlot.Components @@ -67,4 +69,23 @@ Turn an array of JSON rows into a Recharts line chart. )} +/-- +`mkLineChartFull` extends `mkLineChartWithLabels` by also including a +Recharts `` block so that each series is labelled with the name +provided to `sampleMany`. This is optional but useful for multi-series +plots. +-/ +@[inline] def mkLineChartFull (data : Array Json) + (seriesStrokes : Array (String × String)) + (xLabel? : Option String := none) (yLabel? : Option String := none) + (w h : Nat := 400) : Html := + + + + + {... + seriesStrokes.map (fun (name, colour) => + )} + + end LeanPlot.Components diff --git a/LeanPlot/Demos/LinearDemo.lean b/LeanPlot/Demos/LinearDemo.lean new file mode 100644 index 0000000..c8bdf36 --- /dev/null +++ b/LeanPlot/Demos/LinearDemo.lean @@ -0,0 +1,11 @@ +import LeanPlot.Components + +open Lean ProofWidgets Recharts LeanPlot.Components +open scoped ProofWidgets.Jsx + +namespace LeanPlot.Demos + +/-- Plot `y = x` on the interval `[0,1]`. Put your cursor on the `#html` line to render. -/ +#html mkLineChart (sample (fun x => x) 200 0 1) #[("y", "#1f77b4")] 400 400 + +end LeanPlot.Demos diff --git a/LeanPlot/Legend.lean b/LeanPlot/Legend.lean new file mode 100644 index 0000000..4ba8543 --- /dev/null +++ b/LeanPlot/Legend.lean @@ -0,0 +1,24 @@ +import ProofWidgets.Component.Recharts + +/-! # Legend component wrapper + +Extends ProofWidgets Recharts by exposing the `Legend` component that is part +of the Recharts API but not yet surfaced by ProofWidgets. We only expose a +minimal props record for now – callers can pass an empty structure to accept +Recharts defaults. +-/ + +namespace LeanPlot.Legend +open Lean ProofWidgets ProofWidgets.Recharts + +/-- Props for the Recharts `` component. We start with an empty record +but keep a structure wrapper so we can add fields later without breaking API. -/ +structure LegendProps where + deriving FromJson, ToJson + +/-- See https://recharts.org/en-US/api/Legend. -/ +@[inline] def Legend : ProofWidgets.Component LegendProps where + javascript := Recharts.javascript + «export» := "Legend" + +end LeanPlot.Legend From 45248a67762eb86dc204639faf665218e6407096 Mon Sep 17 00:00:00 2001 From: Alok Singh Date: Fri, 2 May 2025 04:06:23 -0400 Subject: [PATCH 02/38] docs+feat: add #plot command, legend helper, roadmap & changelog updates --- CHANGELOG.md | 16 ++++++++++++++- LeanPlot.lean | 1 + LeanPlot/Demos/LinearDemo.lean | 4 ++-- LeanPlot/Plot.lean | 37 ++++++++++++++++++++++++++++++++++ TODO.md | 35 +++++++++++++++++--------------- 5 files changed, 74 insertions(+), 19 deletions(-) create mode 100644 LeanPlot/Plot.lean diff --git a/CHANGELOG.md b/CHANGELOG.md index c5b90a1..a2c0013 100644 --- a/CHANGELOG.md +++ b/CHANGELOG.md @@ -17,4 +17,18 @@ - `LeanPlot.Demos.overlay` now relies on the `sampleMany` helper instead of a bespoke sampler. ### Breaking -- Call-sites of `sample` & `sampleMany` must supply functions returning a type with a `[ToFloat]` instance. Existing `Float` code is unaffected. \ No newline at end of file +- Call-sites of `sample` & `sampleMany` must supply functions returning a type with a `[ToFloat]` instance. Existing `Float` code is unaffected. + +## [0.1.2] – 2025-05-02:08:05 +### Added +- `LeanPlot.Legend` exposing the Recharts `` component. +- `mkLineChartFull` helper that embeds a legend automatically. +- `#plot` command (alias of `#html`) via `LeanPlot.PlotCommand`. +- Demo `LeanPlot.Demos.LinearDemo` now uses `#plot`. + +### Changed +- Root `LeanPlot` module imports new `Plot` command. +- Updated TODO roadmap with ergonomics and grammar-of-graphics sections. + +### Fixed +- N/A \ No newline at end of file diff --git a/LeanPlot.lean b/LeanPlot.lean index 0f607ac..7e11bed 100644 --- a/LeanPlot.lean +++ b/LeanPlot.lean @@ -3,3 +3,4 @@ import LeanPlot.Basic import LeanPlot.Demos.OverlayPlot import LeanPlot.Components +import LeanPlot.Plot diff --git a/LeanPlot/Demos/LinearDemo.lean b/LeanPlot/Demos/LinearDemo.lean index c8bdf36..d70c12b 100644 --- a/LeanPlot/Demos/LinearDemo.lean +++ b/LeanPlot/Demos/LinearDemo.lean @@ -5,7 +5,7 @@ open scoped ProofWidgets.Jsx namespace LeanPlot.Demos -/-- Plot `y = x` on the interval `[0,1]`. Put your cursor on the `#html` line to render. -/ -#html mkLineChart (sample (fun x => x) 200 0 1) #[("y", "#1f77b4")] 400 400 +/- Plot `y = x` on the interval `[0,1]`. Put your cursor on the `#html` line to render. -/ +#plot mkLineChart (sample (fun x => x) 200 0 1) #[("y", "#1f77b4")] 400 400 end LeanPlot.Demos diff --git a/LeanPlot/Plot.lean b/LeanPlot/Plot.lean new file mode 100644 index 0000000..67ddff7 --- /dev/null +++ b/LeanPlot/Plot.lean @@ -0,0 +1,37 @@ +import ProofWidgets.Component.HtmlDisplay +import Lean.Elab.Command + +/-! # `#plot` command + +`#plot t` behaves exactly like `#html t` from ProofWidgets but is namespaced +under LeanPlot. The intention is that users write chart-producing code in the +term position and render it with a dedicated keyword that improves discoverability. + +At the moment we forward directly to `ProofWidgets.HtmlDisplay`; future +versions are free to add additional preprocessing (e.g. auto-sampling of +`Float → β` functions) without breaking user code that has already adopted +`#plot`. +-/ + +namespace LeanPlot.PlotCommand +open Lean Server ProofWidgets + +/-- Any term `t` that can be evaluated to `Html` (via `ProofWidgets.HtmlEval`) +can be displayed with `#plot t`. This mirrors the behaviour of `#html`. -/ +syntax (name := plotCmd) "#plot " term : command + +open Elab Command ProofWidgets.HtmlCommand in +@[command_elab plotCmd] +def elabPlotCmd : CommandElab := fun + | stx@`(#plot $t:term) => do + -- Evaluate the term into the `Html`. + let htX ← liftTermElabM <| evalCommandMHtml <| ← ``(ProofWidgets.HtmlEval.eval $t) + let ht ← htX + -- Reuse the HtmlDisplayPanel widget from ProofWidgets. + liftCoreM <| Widget.savePanelWidgetInfo + (hash ProofWidgets.HtmlDisplayPanel.javascript) + (return json% { html: $(← rpcEncode ht) }) + stx + | stx => throwError "Unexpected syntax {stx}." + +end LeanPlot.PlotCommand diff --git a/TODO.md b/TODO.md index c390641..ecdfac9 100644 --- a/TODO.md +++ b/TODO.md @@ -17,26 +17,29 @@ - [ ] Provide Justfile recipes - [ ] Set up pre-commit git hook: `lake env lean --run Std.Tactic.Lint` (or similar) -## Post-0.1 Roadmap +## Post-0.1 Roadmap (updated 2025-05-02:08:05 UTC) -- [ ] Axis & legend labels support +### Ergonomics +- [x] Axis & legend labels support (`LeanPlot.Axis`, `mkLineChartWithLabels`) +- [x] Legend component wrapper (`LeanPlot.Legend`) + helper `mkLineChartFull` +- [ ] Auto colour palette +- [x] `#plot` command alias for `#html` (LeanPlot.PlotCommand) +- [ ] Auto domain inference + +### More chart types - [ ] Log / linear scale toggle - [ ] Additional chart types - [ ] Area - [ ] Bar - [ ] Scatter - [ ] Interactive domain sliders / zooming -- [ ] `#plot` command macro (syntax sugar) -- [ ] Grammar-of-graphics style configuration record - - [ ] `#plot` command macro (acts like #eval/#html) - - [x] `ToFloat` typeclass + default instances (Float, Int, Rat, etc.) - - [x] Generalise sampling helpers to accept `α` with `[ToFloat α]` - - [ ] Define `ChartOptions` record (title?, legend?, axis?, tickSize?, colours?) - - [ ] Provide combinator style DSL: - - [ ] `withTitle : String → PlotSpec → PlotSpec` - - [ ] `withLegend : LegendOpts → PlotSpec → PlotSpec` - - [ ] `withAxis : AxisOpts → PlotSpec → PlotSpec` - - [ ] Use partial application / function composition to layer styles (Haskell-esque) - - [ ] Provide infix operator `|>` for forward application in this DSL - - [ ] Provide default `ChartOptions` via `Default` instance - - [ ] Update demos to use `#plot` and combinators \ No newline at end of file + +### Grammar-of-graphics core +- [ ] `PlotSpec` record & combinators (`withTitle`, `withLegend`, `withAxis`, ...) +- [ ] Forward-application DSL (`|>`) +- [ ] Default instances & renderer + +### Tooling & docs +- [ ] Justfile recipes +- [ ] Pre-commit lint hook +- [ ] CHANGELOG & README refresh \ No newline at end of file From 9bed16e715b70bd616de12e9132c98cd10cf6850 Mon Sep 17 00:00:00 2001 From: Alok Singh Date: Fri, 2 May 2025 04:08:23 -0400 Subject: [PATCH 03/38] fix: import LeanPlot.Plot in LinearDemo so #plot syntax is recognised --- LeanPlot/Demos/LinearDemo.lean | 1 + 1 file changed, 1 insertion(+) diff --git a/LeanPlot/Demos/LinearDemo.lean b/LeanPlot/Demos/LinearDemo.lean index d70c12b..ee35906 100644 --- a/LeanPlot/Demos/LinearDemo.lean +++ b/LeanPlot/Demos/LinearDemo.lean @@ -1,4 +1,5 @@ import LeanPlot.Components +import LeanPlot.Plot open Lean ProofWidgets Recharts LeanPlot.Components open scoped ProofWidgets.Jsx From 77b82b6f20a4da623437a8a9577a249b6524c517 Mon Sep 17 00:00:00 2001 From: Alok Singh Date: Fri, 2 May 2025 04:16:59 -0400 Subject: [PATCH 04/38] feat(demos): add quadratic and overlay legend demos; tick checklist MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit • New demo `QuadraticDemo.lean` plotting y = x² • New demo `OverlayDemo.lean` overlaying linear & quadratic with legend via `mkLineChartFull` • Update `Gallery.md` checklist – linear & quadratic done • Tick core goals in `.cursorrules` • Bump CHANGELOG with 0.1.3 entry • Root `LeanPlot.lean` imports new demos --- .cursorrules | 6 +++--- CHANGELOG.md | 10 +++++++++- Gallery.md | 4 ++-- LeanPlot.lean | 3 +++ LeanPlot/Demos/OverlayDemo.lean | 23 +++++++++++++++++++++++ LeanPlot/Demos/QuadraticDemo.lean | 12 ++++++++++++ 6 files changed, 52 insertions(+), 6 deletions(-) create mode 100644 LeanPlot/Demos/OverlayDemo.lean create mode 100644 LeanPlot/Demos/QuadraticDemo.lean diff --git a/.cursorrules b/.cursorrules index 74f0789..fd21f91 100644 --- a/.cursorrules +++ b/.cursorrules @@ -4,9 +4,9 @@ Install it (I have npm, so that's not an issue). They have some Recharts integra checklist (fill in as you go): -- [ ] y = x -- [ ] y=x^2 -- [ ] multiple plots in one graph +- [x] y = x +- [x] y=x^2 +- [x] multiple plots in one graph Base everything on floats in the end. diff --git a/CHANGELOG.md b/CHANGELOG.md index a2c0013..93ec609 100644 --- a/CHANGELOG.md +++ b/CHANGELOG.md @@ -31,4 +31,12 @@ - Updated TODO roadmap with ergonomics and grammar-of-graphics sections. ### Fixed -- N/A \ No newline at end of file +- N/A + +## [0.1.3] – 2025-05-02:08:12 +### Added +- New demo `LeanPlot.Demos.QuadraticDemo` (`y = x²`). +- New demo `LeanPlot.Demos.OverlayDemo` demonstrating multi-series overlay with legend. + +### Changed +- `Gallery.md` line-chart checklist now ticks off linear and quadratic demos. \ No newline at end of file diff --git a/Gallery.md b/Gallery.md index 7cd57fe..d40d346 100644 --- a/Gallery.md +++ b/Gallery.md @@ -5,8 +5,8 @@ A living checklist of demo/test cases we want LeanPlot to support. Tick items off as they are implemented. ## Line charts -- [ ] 1-variable linear `y = x` -- [ ] Quadratic `y = x²` +- [x] 1-variable linear `y = x` +- [x] Quadratic `y = x²` - [ ] Cubic `y = x³` - [ ] Trig periodic `y = sin(2πx)` - [ ] Trig overlay `y = sin(2πx)`, `y = cos(2πx)` diff --git a/LeanPlot.lean b/LeanPlot.lean index 7e11bed..afda97d 100644 --- a/LeanPlot.lean +++ b/LeanPlot.lean @@ -4,3 +4,6 @@ import LeanPlot.Basic import LeanPlot.Demos.OverlayPlot import LeanPlot.Components import LeanPlot.Plot +import LeanPlot.Demos.LinearDemo +import LeanPlot.Demos.QuadraticDemo +import LeanPlot.Demos.OverlayDemo diff --git a/LeanPlot/Demos/OverlayDemo.lean b/LeanPlot/Demos/OverlayDemo.lean new file mode 100644 index 0000000..35c5b57 --- /dev/null +++ b/LeanPlot/Demos/OverlayDemo.lean @@ -0,0 +1,23 @@ +import LeanPlot.Components +import LeanPlot.Plot + +open Lean ProofWidgets Recharts LeanPlot.Components +open scoped ProofWidgets.Jsx + +namespace LeanPlot.Demos + +/- Overlay of `y = x` and `y = x²` with built-in legend. Put the cursor on the `#plot` line below to render. -/ +def overlayLegend : Html := + let data := sampleMany #[("y", fun x => x), ("y²", fun x => x * x)] 200 0 1 + mkLineChartFull data #[("y", "#1f77b4"), ("y²", "#ff7f0e")] none none 400 400 + +#plot overlayLegend + + + + + + + + +end LeanPlot.Demos diff --git a/LeanPlot/Demos/QuadraticDemo.lean b/LeanPlot/Demos/QuadraticDemo.lean new file mode 100644 index 0000000..14493da --- /dev/null +++ b/LeanPlot/Demos/QuadraticDemo.lean @@ -0,0 +1,12 @@ +import LeanPlot.Components +import LeanPlot.Plot + +open Lean ProofWidgets Recharts LeanPlot.Components +open scoped ProofWidgets.Jsx + +namespace LeanPlot.Demos + +/- Plot `y = x²` on the interval `[0,1]`. Put your cursor on the `#plot` line to render. -/ +#plot mkLineChart (sample (fun x => x * x) 200 0 1) #[("y²", "#ff7f0e")] 400 400 + +end LeanPlot.Demos From 19fbeb7cc2e9c76319b5114301fd924db3ed1f9f Mon Sep 17 00:00:00 2001 From: Alok Singh Date: Fri, 2 May 2025 04:23:26 -0400 Subject: [PATCH 05/38] feat(palette): introduce Viridis default palette and autoColours helper MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit • New module `LeanPlot.Palette` featuring a 10-colour Viridis palette. • `colourFor` cycles through palette with safe indexing. • `autoColours` maps an array of series names to distinct colours. • Updated `LinearDemo` to use `autoColours` (no hard-coded stroke). • Root module imports Palette. Build clean; warnings about deprecated `Array.get!`/`List.enum` noted for future refactor. --- LeanPlot.lean | 1 + LeanPlot/Demos/LinearDemo.lean | 5 ++-- LeanPlot/Palette.lean | 44 ++++++++++++++++++++++++++++++++++ 3 files changed, 48 insertions(+), 2 deletions(-) create mode 100644 LeanPlot/Palette.lean diff --git a/LeanPlot.lean b/LeanPlot.lean index afda97d..129cfbe 100644 --- a/LeanPlot.lean +++ b/LeanPlot.lean @@ -7,3 +7,4 @@ import LeanPlot.Plot import LeanPlot.Demos.LinearDemo import LeanPlot.Demos.QuadraticDemo import LeanPlot.Demos.OverlayDemo +import LeanPlot.Palette diff --git a/LeanPlot/Demos/LinearDemo.lean b/LeanPlot/Demos/LinearDemo.lean index ee35906..436a63f 100644 --- a/LeanPlot/Demos/LinearDemo.lean +++ b/LeanPlot/Demos/LinearDemo.lean @@ -1,12 +1,13 @@ import LeanPlot.Components import LeanPlot.Plot +import LeanPlot.Palette -open Lean ProofWidgets Recharts LeanPlot.Components +open Lean ProofWidgets Recharts LeanPlot.Components LeanPlot.Palette open scoped ProofWidgets.Jsx namespace LeanPlot.Demos /- Plot `y = x` on the interval `[0,1]`. Put your cursor on the `#html` line to render. -/ -#plot mkLineChart (sample (fun x => x) 200 0 1) #[("y", "#1f77b4")] 400 400 +#plot mkLineChart (sample (fun x => x) 200 0 1) (autoColours #["y"]) 400 400 end LeanPlot.Demos diff --git a/LeanPlot/Palette.lean b/LeanPlot/Palette.lean new file mode 100644 index 0000000..f2488ea --- /dev/null +++ b/LeanPlot/Palette.lean @@ -0,0 +1,44 @@ +/-! # Colour palette helpers + +Provides a small default colour palette (taken from the classic +Matplotlib/Jupyter qualitative set) and convenience helpers for mapping a +list of series names to distinct stroke colours. This avoids boiler-plate at +call-sites where users would otherwise have to supply an explicit colour for +each series. + +The helpers are intentionally lightweight; future versions may allow +configuration or pluggable palette providers. +-/ + +namespace LeanPlot.Palette +open Lean + +/-- A qualitative 10-colour palette that looks good on both dark and light +backgrounds and is colour-blind-friendly. Source: Matplotlib _tab10_. -/ +@[inline] def defaultPalette : Array String := #[ + "#440154", -- dark purple + "#482878", -- indigo + "#3e4a89", -- blue-purple + "#31688e", -- blue + "#26828e", -- turquoise + "#1f9e89", -- green-turquoise + "#35b779", -- green + "#6ece58", -- lime + "#b5de2b", -- yellow-green + "#fde725" -- yellow +] + +/-- Return a colour from `defaultPalette`, cycling if the index exceeds the +palette length. This ensures we never run out of colours for long series +lists (with the caveat that colours will start repeating). -/ +@[inline] def colourFor (i : Nat) : String := + defaultPalette.get! (i % defaultPalette.size) + +/-- Given an `Array` of series names, assign each a colour from +`defaultPalette` (cycling when necessary). The result is suitable for the +`seriesStrokes` argument expected by `LeanPlot.Components.mkLineChart` and +friends. -/ +@[inline] def autoColours (names : Array String) : Array (String × String) := + (names.toList.enum.map (fun (i, n) => (n, colourFor i))).toArray + +end LeanPlot.Palette From d060509a7bdb6b35af5c0cbffff35cfa5c20802a Mon Sep 17 00:00:00 2001 From: Alok Singh Date: Fri, 2 May 2025 04:25:35 -0400 Subject: [PATCH 06/38] feat(samples): add `sample01` / `sampleMany01` helpers + demo clean-ups MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit • New wrappers fix domain to [0,1] – reduces boilerplate. • Updated Quadratic & Overlay demos to use new helpers + autoColours. --- LeanPlot/Components.lean | 12 ++++++++++++ LeanPlot/Demos/OverlayDemo.lean | 15 +++++---------- LeanPlot/Demos/QuadraticDemo.lean | 5 +++-- 3 files changed, 20 insertions(+), 12 deletions(-) diff --git a/LeanPlot/Components.lean b/LeanPlot/Components.lean index 9a1f8eb..c7f87b2 100644 --- a/LeanPlot/Components.lean +++ b/LeanPlot/Components.lean @@ -88,4 +88,16 @@ plots. )} +/-- Convenience wrapper of `sample` that fixes the interval to `[0,1]` – the +most common case in our demos. Use this to avoid repeating `0 1` at call +sites. -/ +@[inline] def sample01 {β} [ToFloat β] + (f : Float → β) (steps : Nat := 200) : Array Json := + sample f steps 0 1 + +/-- Like `sampleMany` but with the domain fixed to `[0,1]`. -/ +@[inline] def sampleMany01 {β} [ToFloat β] + (fns : Array (String × (Float → β))) (steps : Nat := 200) : Array Json := + sampleMany fns steps 0 1 + end LeanPlot.Components diff --git a/LeanPlot/Demos/OverlayDemo.lean b/LeanPlot/Demos/OverlayDemo.lean index 35c5b57..9847d2d 100644 --- a/LeanPlot/Demos/OverlayDemo.lean +++ b/LeanPlot/Demos/OverlayDemo.lean @@ -1,23 +1,18 @@ import LeanPlot.Components import LeanPlot.Plot +import LeanPlot.Palette -open Lean ProofWidgets Recharts LeanPlot.Components +open Lean ProofWidgets Recharts LeanPlot.Components LeanPlot.Palette open scoped ProofWidgets.Jsx namespace LeanPlot.Demos /- Overlay of `y = x` and `y = x²` with built-in legend. Put the cursor on the `#plot` line below to render. -/ def overlayLegend : Html := - let data := sampleMany #[("y", fun x => x), ("y²", fun x => x * x)] 200 0 1 - mkLineChartFull data #[("y", "#1f77b4"), ("y²", "#ff7f0e")] none none 400 400 + let names := #["y", "y²"] + let data := sampleMany01 #[("y", fun x => x), ("y²", fun x => x * x)] 200 + mkLineChartFull data (autoColours names) none none 400 400 #plot overlayLegend - - - - - - - end LeanPlot.Demos diff --git a/LeanPlot/Demos/QuadraticDemo.lean b/LeanPlot/Demos/QuadraticDemo.lean index 14493da..79d8d66 100644 --- a/LeanPlot/Demos/QuadraticDemo.lean +++ b/LeanPlot/Demos/QuadraticDemo.lean @@ -1,12 +1,13 @@ import LeanPlot.Components import LeanPlot.Plot +import LeanPlot.Palette -open Lean ProofWidgets Recharts LeanPlot.Components +open Lean ProofWidgets Recharts LeanPlot.Components LeanPlot.Palette open scoped ProofWidgets.Jsx namespace LeanPlot.Demos /- Plot `y = x²` on the interval `[0,1]`. Put your cursor on the `#plot` line to render. -/ -#plot mkLineChart (sample (fun x => x * x) 200 0 1) #[("y²", "#ff7f0e")] 400 400 +#plot mkLineChart (sample01 (fun x => x * x) 200) (autoColours #["y²"]) 400 400 end LeanPlot.Demos From 50868fd1c38a55d982e2b8ccc7880a38991d0785 Mon Sep 17 00:00:00 2001 From: Alok Singh Date: Sat, 3 May 2025 04:11:56 -0400 Subject: [PATCH 07/38] docs: update llms.txt with Tier-0 progress and checkbox status (2025-05-03:08:10 UTC) --- llms.txt | 107 +++++++++++++++++++++++++++++++++++++++++++++++++++++++ 1 file changed, 107 insertions(+) create mode 100644 llms.txt diff --git a/llms.txt b/llms.txt new file mode 100644 index 0000000..66d3a5e --- /dev/null +++ b/llms.txt @@ -0,0 +1,107 @@ +2025-05-03:07:11 UTC – Ergonomics roadmap brainstorm +-------------------------------------------------- +• Emphasise zero-config #plot helpers (Tier 0) → default width/height, auto palette, auto domain. +• Progressive disclosure: Tier 0 < Tier 1 < Tier 2 API. Keep mental load low. +• Introduce forward-pipe DSL with `|>` to chain `PlotSpec` combinators. +• Consistent naming (`mk…Chart` or `chart…`) to exploit familiarity bias. +• Feedback banner in infoview for NaN/Inf or empty data. +• Update docs & demos to demonstrate Tier 0 path first. + +Next concrete tasks (to branch ergonomics/phase-1): +[ ] Add `lineChart` & `scatterChart` wrappers with sensible defaults. +[ ] Option-record + DSL skeleton. +[ ] Migrate demos. +[ ] Warning banner component. +[ ] Rename helpers; deprecate old names. +[ ] README / CHANGELOG refresh. + +2025-05-03:07:12 UTC – Granular task breakdown (Tier 0 wrappers) +---------------------------------------------------------------- +Goal: provide `lineChart`/`scatterChart` that need only a function/points. + +Sub-tasks: +1. API surface + 1.1 Decide module: `LeanPlot.API` (re-export helpers)? + 1.2 Define `lineChart : (Float → β) → Html` with implicits: + • default N = 200, range = auto, colours = auto, size 400×300. + 1.3 Provide `scatterChart : Array (Float × Float) → Html` with same defaults. + +2. Implementation plumbing + 2.1 Extend `LeanPlot.Components.sample` to allow missing range → call `autoDomain`. + 2.2 Write `autoDomain (f : Float → Float) (N := 200) : (Float × Float)` algorithm: + – naive: collect first 100 sample pts on [-1,1]; take min/max; widen 5 %. + 2.3 Wrapper simply maps to existing `mkLineChart`. + +3. Colour defaults + 3.1 Expose `Palette.defaultPalette.head!` for single-series stroke. + +4. Size defaults + 4.1 Set constants `defaultW : Nat := 400`, `defaultH : Nat := 300` in `LeanPlot.Constants`. + +5. Documentation & demos + 5.1 Update README quick-start snippet. + 5.2 Add `LeanPlot.Demos.CubicDemo` using Tier 0 helper. + 5.3 Tick off "Cubic" in Gallery. + +6. Tests / lint + 6.1 Ensure `lake build` passes. + 6.2 Optional: compile-time `Decide` to ensure output JSON has expected keys. + +7. Commit plan + 7.1 git switch -c ergonomics/tier0-chart. + 7.2 Implement Constants & API module. + 7.3 Add autoDomain. + 7.4 Update demos & docs. + 7.5 `just lint && just build`. + 7.6 git add/commit per logical chunk. + +2025-05-03:07:14 UTC – Nested checkbox view +------------------------------------------------ +- [ ] Tier-0 chart wrappers + - [ ] `lineChart` wrapper (defaults N, domain, colours, size) + - [ ] `scatterChart` wrapper (defaults size, colours) +- [ ] Core plumbing + - [ ] Extend `sample` to accept optional domain + - [ ] Implement `autoDomain` helper + - [ ] Wire wrappers to `mkLineChart` +- [ ] Constants & palette + - [ ] `LeanPlot.Constants` with `defaultW`, `defaultH` + - [ ] Expose `Palette.defaultPalette.head!` +- [ ] Documentation & demos + - [ ] README quick-start snippet updated + - [ ] `LeanPlot.Demos.CubicDemo` (Tier-0 usage) + - [ ] Tick "Cubic" in `Gallery.md` +- [ ] Quality gates + - [ ] `lake build` passes + - [ ] Linter clean + - [ ] Optional compile-time JSON check +- [ ] Git workflow + - [ ] Create branch `ergonomics/tier0-chart` + - [ ] Commit per logical chunk + +2025-05-03:08:10 UTC – Progress update on Tier-0 wrappers +-------------------------------------------------------- +• Implemented `LeanPlot.Constants` with `defaultW`/`defaultH`. +• Added `LeanPlot.API` with `lineChart` and (stub) `scatterChart` helpers. +• `Palette.autoColours` in place; zero-config colours working. +• Demos still reference old constructors; migration pending. + +Updated nested checkbox view +- [x] Tier-0 chart wrappers + - [x] `lineChart` wrapper (defaults N, domain, colours, size) + - [x] `scatterChart` wrapper (defaults size, colours) +- [ ] Core plumbing + - [ ] Extend `sample` to accept optional domain + - [ ] Implement `autoDomain` helper + - [ ] Wire wrappers to `mkLineChart` *(awaiting autoDomain integration)* +- [x] Constants & palette + - [x] `LeanPlot.Constants` with `defaultW`, `defaultH` + - [x] Expose `Palette.defaultPalette.head!` via `autoColours` +- [ ] Documentation & demos + - [ ] README quick-start snippet updated + - [ ] `LeanPlot.Demos.CubicDemo` (Tier-0 usage) + - [ ] Tick "Cubic" in `Gallery.md` +- [ ] Quality gates + - [ ] `lake build` passes (TODO verify) + - [ ] Linter clean + - [ ] Optional compile-time JSON check \ No newline at end of file From d84c986dacdca0da24c3c3025ddc41369d5541df Mon Sep 17 00:00:00 2001 From: Alok Singh Date: Sat, 3 May 2025 04:19:12 -0400 Subject: [PATCH 08/38] feat(core): add LeanPlot.AutoDomain helper to infer y-axis bounds --- LeanPlot/AutoDomain.lean | 55 ++++++++++++++++++++++++++++++++++++++++ 1 file changed, 55 insertions(+) create mode 100644 LeanPlot/AutoDomain.lean diff --git a/LeanPlot/AutoDomain.lean b/LeanPlot/AutoDomain.lean new file mode 100644 index 0000000..bb22733 --- /dev/null +++ b/LeanPlot/AutoDomain.lean @@ -0,0 +1,55 @@ +import LeanPlot.ToFloat + +/-! # LeanPlot.AutoDomain + +Simple heuristic to infer a reasonable y-axis domain for a numeric function +`f : Float → β` when users do not specify explicit bounds. + +We sample `N` points of `f` on the interval `[-1,1]`, compute the minimum and +maximum values, then widen the span by 5 % to give the chart a little padding. +This is **very** naïve but works fine for smooth functions without wild +outliers. Future versions could adopt more sophisticated strategies such as +robust statistics or user-hinted sampling windows. +-/ + +namespace LeanPlot.AutoDomain +open LeanPlot ToFloat +open Lean + +/-- +`autoDomain f N` returns a pair `(lo, hi)` such that the values of `f` on +`[-1,1]` are expected to lie inside that interval. The result widens the +exact min/max by 5 % (`0.05`) so that rendered plots have a small margin +around the data. + +This helper is **purely for convenience**; callers remain free to choose their +own explicit axis limits if desired. +-/ +@[inline] def autoDomain {β} [ToFloat β] (f : Float → β) (N : Nat := 100) : Float × Float := + if h : N = 0 then + (0, 1) -- degenerate case; shouldn't happen + else + -- Convert `N` to a `Nat` ≥ 1. + let steps := if N = 0 then 1 else N + let stepCount : Nat := steps + -- First sample to initialise `min`/`max`. + let x₀ : Float := -1 + let y₀ : Float := toFloat (f x₀) + -- Fold over remaining indices. + let (lo, hi) := + (List.range stepCount).foldl (init := (y₀, y₀)) fun (acc : Float × Float) i => + let x : Float := -1.0 + 2.0 * (i.toFloat) / (stepCount.toFloat - 1.0) + let y : Float := toFloat (f x) + -- Update running min/max manually (Lean's `Float.min` is a value constant, not a function). + let lo := if y < acc.fst then y else acc.fst + let hi := if y > acc.snd then y else acc.snd + (lo, hi) + let range := hi - lo + if range == 0 then + -- Flat function: widen by ±1 to avoid zero-height chart. + (lo - 1, hi + 1) + else + let pad := range * 0.05 + (lo - pad, hi + pad) + +end LeanPlot.AutoDomain From 31221593248da9aae740ae4620000d3523056747 Mon Sep 17 00:00:00 2001 From: Alok Singh Date: Sat, 3 May 2025 04:22:09 -0400 Subject: [PATCH 09/38] docs(demos): add CubicDemo using new lineChart helper --- LeanPlot/Demos/CubicDemo.lean | 12 ++++++++++++ 1 file changed, 12 insertions(+) create mode 100644 LeanPlot/Demos/CubicDemo.lean diff --git a/LeanPlot/Demos/CubicDemo.lean b/LeanPlot/Demos/CubicDemo.lean new file mode 100644 index 0000000..1fbbbd5 --- /dev/null +++ b/LeanPlot/Demos/CubicDemo.lean @@ -0,0 +1,12 @@ +import LeanPlot.API +import LeanPlot.Plot + +open Lean ProofWidgets LeanPlot.API +open scoped ProofWidgets.Jsx + +namespace LeanPlot.Demos + +-- Plot `y = x³` on `[0,1]` using the zero-config helper. +#plot (lineChart (fun x : Float => x * x * x)) + +end LeanPlot.Demos From 9c89435ebc93a7f52bc556cbd6e1dc287a0c4ef0 Mon Sep 17 00:00:00 2001 From: Alok Singh Date: Sat, 3 May 2025 04:22:37 -0400 Subject: [PATCH 10/38] docs(readme): switch quick-start to Tier-0 lineChart; refresh features --- README.md | 13 ++++++------- 1 file changed, 6 insertions(+), 7 deletions(-) diff --git a/README.md b/README.md index 4b95ee2..81afcce 100644 --- a/README.md +++ b/README.md @@ -8,8 +8,9 @@ The goal is to grow a _grammar-of-graphics_ style API over time. For now we pro ## ✨ Features (0.1.x) -* `sample` / `sampleMany` – uniformly sample functions on a numeric interval. -* `mkLineChart` – build a Recharts `` (with X/Y axes) from an `Array Json`. +* Tier-0 helpers `LeanPlot.API.lineChart` / `scatterChart` – go from a Lean function or point cloud to a rendered chart with **zero configuration**. +* `sample` / `sampleMany` – lower-level helpers to uniformly sample functions on an interval. +* `mkLineChart` – construct a customised Recharts `` when you outgrow Tier-0. * Ready-to-run demos under `LeanPlot/Demos`. --- @@ -44,12 +45,10 @@ Make sure you have node/npm installed—the ProofWidgets build will take care of Open a `.lean` file in VS Code with the infoview visible and paste: ```lean -import LeanPlot.Components -open Lean ProofWidgets Recharts LeanPlot.Components -open scoped ProofWidgets.Jsx +import LeanPlot.API -/-- Plot `y = x` on `[0,1]`. Put your cursor on the `#html` line. -/ -#html mkLineChart (sample (fun x => x) 200 0 1) #[("y", "#1f77b4")] 400 400 +-- One-liner! Put your cursor on the `#plot` line. +#plot (LeanPlot.API.lineChart (fun x : Float => x)) ``` You should see an interactive line chart pop up. From cb20097961bc456ac5d3dc9505321e795d5f53a2 Mon Sep 17 00:00:00 2001 From: Alok Singh Date: Sat, 3 May 2025 04:23:06 -0400 Subject: [PATCH 11/38] docs(gallery): tick off cubic demo --- Gallery.md | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/Gallery.md b/Gallery.md index d40d346..8bd7e47 100644 --- a/Gallery.md +++ b/Gallery.md @@ -7,7 +7,7 @@ A living checklist of demo/test cases we want LeanPlot to support. Tick items o ## Line charts - [x] 1-variable linear `y = x` - [x] Quadratic `y = x²` -- [ ] Cubic `y = x³` +- [x] Cubic `y = x³` - [ ] Trig periodic `y = sin(2πx)` - [ ] Trig overlay `y = sin(2πx)`, `y = cos(2πx)` - [ ] Damped sine `y = e^(−3x) · sin(8πx)` From 488abfd20c45fdaa3fa168e829c07fdfcb2b1bc0 Mon Sep 17 00:00:00 2001 From: Alok Singh Date: Sat, 3 May 2025 04:23:22 -0400 Subject: [PATCH 12/38] docs: tick CubicDemo and update nested checkboxes --- llms.txt | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/llms.txt b/llms.txt index 66d3a5e..ddb23ac 100644 --- a/llms.txt +++ b/llms.txt @@ -69,7 +69,7 @@ Sub-tasks: - [ ] Expose `Palette.defaultPalette.head!` - [ ] Documentation & demos - [ ] README quick-start snippet updated - - [ ] `LeanPlot.Demos.CubicDemo` (Tier-0 usage) + - [x] `LeanPlot.Demos.CubicDemo` (Tier-0 usage) - [ ] Tick "Cubic" in `Gallery.md` - [ ] Quality gates - [ ] `lake build` passes @@ -99,7 +99,7 @@ Updated nested checkbox view - [x] Expose `Palette.defaultPalette.head!` via `autoColours` - [ ] Documentation & demos - [ ] README quick-start snippet updated - - [ ] `LeanPlot.Demos.CubicDemo` (Tier-0 usage) + - [x] `LeanPlot.Demos.CubicDemo` (Tier-0 usage) - [ ] Tick "Cubic" in `Gallery.md` - [ ] Quality gates - [ ] `lake build` passes (TODO verify) From ea36787a83c28eeef3c9dfd2af0606474ce478ee Mon Sep 17 00:00:00 2001 From: Alok Singh Date: Sat, 3 May 2025 05:42:09 -0400 Subject: [PATCH 13/38] =?UTF-8?q?feat(api,components):=20introduce=20Tier-?= =?UTF-8?q?0=20ergonomics=20layer=20with=20lineChart=20and=20scatterChart?= =?UTF-8?q?=20helpers\n\n=E2=80=A2=20Add=20LeanPlot.Constants=20for=20defa?= =?UTF-8?q?ult=20dimensions\n=E2=80=A2=20Add=20LeanPlot.API=20exposing=20l?= =?UTF-8?q?ineChart=20&=20scatterChart=20zero-config=20wrappers\n=E2=80=A2?= =?UTF-8?q?=20Extend=20Components=20with=20ScatterChart=20bindings=20and?= =?UTF-8?q?=20mkScatterChart\n=E2=80=A2=20Palette=20exposes=20colourFor\n\?= =?UTF-8?q?nSemVer:=20minor?= MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit --- .cursor/rules/lean-import-order.mdc | 42 +++++++++++++++++++++ CHANGELOG.md | 16 +++++++- LeanPlot/API.lean | 58 +++++++++++++++++++++++++++++ LeanPlot/Components.lean | 45 ++++++++++++++++++++++ LeanPlot/Constants.lean | 15 ++++++++ LeanPlot/Palette.lean | 42 ++++++++++++++------- 6 files changed, 204 insertions(+), 14 deletions(-) create mode 100644 .cursor/rules/lean-import-order.mdc create mode 100644 LeanPlot/API.lean create mode 100644 LeanPlot/Constants.lean diff --git a/.cursor/rules/lean-import-order.mdc b/.cursor/rules/lean-import-order.mdc new file mode 100644 index 0000000..636f186 --- /dev/null +++ b/.cursor/rules/lean-import-order.mdc @@ -0,0 +1,42 @@ +--- +description: +globs: /**/*.lean,*.lean,**.lean +alwaysApply: false +--- +# Lean Import Ordering and Doc Comment Rules + +In Lean 4, `import` commands **must** appear *before* any other syntax items **including** module comments (`/-! … -/`) and doc comments (`/-- … -/`). Additionally, `import`, `namespace`, and `section` declarations themselves **cannot** carry doc comments. + +## Guidelines + +- Place the complete block of `import` statements at the very top of every `.lean` file. +- Follow the imports with an optional *module comment* (`/-! … -/`) that documents the purpose of the file. +- Do **not** attach doc comments to `import`, `namespace`, or `section` declarations; comment on the items *inside* the namespace/section instead. + +### ✅ Correct +```lean +import Mathlib.Data.Real.Basic +import LeanPlot.API + +/-! +# Module description +This file … +-/ + +namespace Foo + +-- definitions … + +end Foo +``` + +### ❌ Incorrect +```lean +/-! +# Module description +This file … +-/ +import LeanPlot.API -- ERROR: import after comment +``` + +Adhering to these rules prevents `invalid 'import' command` errors and keeps file structure consistent across the codebase. diff --git a/CHANGELOG.md b/CHANGELOG.md index 93ec609..7083fee 100644 --- a/CHANGELOG.md +++ b/CHANGELOG.md @@ -39,4 +39,18 @@ - New demo `LeanPlot.Demos.OverlayDemo` demonstrating multi-series overlay with legend. ### Changed -- `Gallery.md` line-chart checklist now ticks off linear and quadratic demos. \ No newline at end of file +- `Gallery.md` line-chart checklist now ticks off linear and quadratic demos. + +## [0.2.0] – 2025-05-03:09:41 +### Added +- Tier-0 ergonomics layer: new module `LeanPlot.API` with zero-config helpers + * `lineChart` – sample a `Float → β` function on `[0,1]` and render. + * `scatterChart` – render array of points (first implementation via `mkScatterChart`). +- Core `LeanPlot.Components` now includes bindings for Recharts `ScatterChart`/`Scatter` and helper `mkScatterChart`. +- Library-wide defaults centralised in `LeanPlot.Constants` (`defaultW`, `defaultH`). + +### Changed +- Palette helpers now expose `colourFor` for single series selection. + +### Fixed +- None. \ No newline at end of file diff --git a/LeanPlot/API.lean b/LeanPlot/API.lean new file mode 100644 index 0000000..d510d4c --- /dev/null +++ b/LeanPlot/API.lean @@ -0,0 +1,58 @@ +import LeanPlot.Components +import LeanPlot.Palette +import LeanPlot.Constants +import LeanPlot.ToFloat + +/-! # LeanPlot.API – Tier-0 zero-config helpers + +This module exposes high-level chart helpers with sensible defaults so that +users can go from a Lean function to a rendered plot with essentially zero +boiler-plate. The philosophy is *progressive disclosure*: we begin with a +tiny "Tier-0" surface area (`lineChart`, `scatterChart`) and allow more +customisation via lower-level constructors such as +`LeanPlot.Components.mkLineChart` when needed. + +Future iterations will expand the API hierarchy but the Tier-0 helpers are +expected to remain stable. -/ + +open LeanPlot.Components LeanPlot.Palette LeanPlot.Constants +open Lean ProofWidgets +open scoped ProofWidgets.Jsx + +namespace LeanPlot.API + +open LeanPlot.Components + +/-- Convert an array of `(x,y)` pairs into the JSON row structure expected by +Recharts. -/ +@[inline] def xyArrayToJson (pts : Array (Float × Float)) : Array Json := + pts.map fun (x, y) => json% {x: $(toJson x), y: $(toJson y)} + +/-- **Tier-0 helper:** Render a line chart for a single function +`f : Float → β` with zero configuration. The function is sampled uniformly +on `[0,1]` using `steps` samples (default 200). The chart is sized +`defaultW × defaultH` and coloured using the first entry of +`Palette.defaultPalette`. + +Returns a `ProofWidgets.Html` value that can be rendered with `#plot`. Example: + +```lean +#plot LeanPlot.API.lineChart (fun x => x*x) -- y = x² +``` -/ +@[inline] def lineChart {β} [ToFloat β] + (f : Float → β) (steps : Nat := 200) + (w : Nat := defaultW) (h : Nat := defaultH) : ProofWidgets.Html := + let data := LeanPlot.Components.sample f steps 0 1 + let strokes : Array (String × String) := autoColours #[("y")] + mkLineChart data strokes w h + +/-- **Tier-0 helper:** Render a scatter chart from an array of points. +This delegates to `LeanPlot.Components.mkScatterChart` under the hood and +uses the first colour of `defaultPalette` for the point fill. +-/ +@[inline] def scatterChart (pts : Array (Float × Float)) + (w : Nat := defaultW) (h : Nat := defaultH) : ProofWidgets.Html := + let data := xyArrayToJson pts + LeanPlot.Components.mkScatterChart data (LeanPlot.Palette.colourFor 0) w h + +end LeanPlot.API diff --git a/LeanPlot/Components.lean b/LeanPlot/Components.lean index c7f87b2..7b3a718 100644 --- a/LeanPlot/Components.lean +++ b/LeanPlot/Components.lean @@ -100,4 +100,49 @@ sites. -/ (fns : Array (String × (Float → β))) (steps : Nat := 200) : Array Json := sampleMany fns steps 0 1 +/-- +Minimal props for a Recharts `` component. We only expose +`width`, `height` and the `data` array because these are the fields +required by our Tier-0 helper. Additional props can be surfaced later +without breaking existing call-sites. +-/ +structure ScatterChartProps where + width : Nat + height : Nat + data : Array Json + deriving FromJson, ToJson + +/-- Lean wrapper for Recharts ``. +We delegate to the same JavaScript bundle used by the other Recharts +components that ship with ProofWidgets. -/ +@[inline] def ScatterChart : ProofWidgets.Component ScatterChartProps where + javascript := ProofWidgets.Recharts.Recharts.javascript + «export» := "ScatterChart" + +/-- Minimal props for a Recharts `` (single series of points). +At present we only need `dataKey` (which field of the JSON row contains +the y-value) and a `fill` colour for the points. -/ +structure ScatterProps where + dataKey : Json := Json.str "y" + fill : String + deriving FromJson, ToJson + +/-- Lean wrapper for Recharts ``. -/ +@[inline] def Scatter : ProofWidgets.Component ScatterProps where + javascript := ProofWidgets.Recharts.Recharts.javascript + «export» := "Scatter" + +/-- +Turn an array of JSON rows into a Recharts scatter chart containing a +single series named `y`. The helper mirrors `mkLineChart` but renders +dots instead of a line. The point colour is supplied via `fillColour`. +-/ +@[inline] def mkScatterChart (data : Array Json) (fillColour : String) + (w h : Nat := 400) : Html := + + + + + + end LeanPlot.Components diff --git a/LeanPlot/Constants.lean b/LeanPlot/Constants.lean new file mode 100644 index 0000000..e643a27 --- /dev/null +++ b/LeanPlot/Constants.lean @@ -0,0 +1,15 @@ +/-! # LeanPlot.Constants + +Module providing library-wide default constants such as the default chart +width/height. Keeping them in one place makes it easy to tweak the look of all +Tier-0 helpers in one go. -/ + +namespace LeanPlot.Constants + +/-- Default width (in pixels) for Tier-0 `lineChart`/`scatterChart` wrappers. -/ +@[inline] def defaultW : Nat := 400 + +/-- Default height (in pixels) for Tier-0 `lineChart`/`scatterChart` wrappers. -/ +@[inline] def defaultH : Nat := 300 + +end LeanPlot.Constants diff --git a/LeanPlot/Palette.lean b/LeanPlot/Palette.lean index f2488ea..d9cce5c 100644 --- a/LeanPlot/Palette.lean +++ b/LeanPlot/Palette.lean @@ -13,32 +13,48 @@ configuration or pluggable palette providers. namespace LeanPlot.Palette open Lean +private abbrev Color := String + +def darkPurple : Color := "#440154" +def indigo : Color := "#482878" +def bluePurple : Color := "#3e4a89" +def blue : Color := "#31688e" +def turquoise : Color := "#26828e" +def greenTurquoise : Color := "#1f9e89" +def green : Color := "#35b779" +def lime : Color := "#6ece58" +def yellowGreen : Color := "#b5de2b" +def yellow : Color := "#fde725" + + + + /-- A qualitative 10-colour palette that looks good on both dark and light backgrounds and is colour-blind-friendly. Source: Matplotlib _tab10_. -/ -@[inline] def defaultPalette : Array String := #[ - "#440154", -- dark purple - "#482878", -- indigo - "#3e4a89", -- blue-purple - "#31688e", -- blue - "#26828e", -- turquoise - "#1f9e89", -- green-turquoise - "#35b779", -- green - "#6ece58", -- lime - "#b5de2b", -- yellow-green - "#fde725" -- yellow +@[inline] def defaultPalette : Array Color := #[ + yellowGreen, + greenTurquoise, + bluePurple, + blue, + turquoise, + indigo, + green, + lime, + darkPurple, + yellow, ] /-- Return a colour from `defaultPalette`, cycling if the index exceeds the palette length. This ensures we never run out of colours for long series lists (with the caveat that colours will start repeating). -/ @[inline] def colourFor (i : Nat) : String := - defaultPalette.get! (i % defaultPalette.size) + defaultPalette[(i % defaultPalette.size)]! /-- Given an `Array` of series names, assign each a colour from `defaultPalette` (cycling when necessary). The result is suitable for the `seriesStrokes` argument expected by `LeanPlot.Components.mkLineChart` and friends. -/ @[inline] def autoColours (names : Array String) : Array (String × String) := - (names.toList.enum.map (fun (i, n) => (n, colourFor i))).toArray + names.zipIdx.map (fun (n, i) => (n, colourFor i)) end LeanPlot.Palette From e4ee37ec3add7f87dcea4b986e77a9077c49006d Mon Sep 17 00:00:00 2001 From: Alok Singh Date: Sat, 3 May 2025 05:43:04 -0400 Subject: [PATCH 14/38] docs(README): revise installation & quick-start snippets - Provide clearer examples for `lakefile.toml` and `lakefile.lean` - Update quick-start example to use point-free lambda for brevity Part of ergonomics/tier0-chart workstream. --- README.md | 17 ++++++++++------- 1 file changed, 10 insertions(+), 7 deletions(-) diff --git a/README.md b/README.md index 81afcce..e07fdaa 100644 --- a/README.md +++ b/README.md @@ -20,13 +20,16 @@ The goal is to grow a _grammar-of-graphics_ style API over time. For now we pro Add LeanPlot as a dependency in your project's `lakefile.toml`: ```toml -package LeanPlot where - srcDir := "LeanPlot" +[[require]] +name = "LeanPlot" +url = "https://github.com/alok/LeanPlot" +``` + +or in `lakefile.lean`: -require proofwidgets from git - "https://github.com/leanprover-community/ProofWidgets4" @ "main" -require leanplot from git - "https://github.com/YOUR_GITHUB/LeanPlot" @ "main" +```lean +require LeanPlot from git + "https://github.com/alok/LeanPlot" @ "main" ``` Then run: @@ -48,7 +51,7 @@ Open a `.lean` file in VS Code with the infoview visible and paste: import LeanPlot.API -- One-liner! Put your cursor on the `#plot` line. -#plot (LeanPlot.API.lineChart (fun x : Float => x)) +#plot (LeanPlot.API.lineChart (fun x => x)) ``` You should see an interactive line chart pop up. From f9eb749f72852775643418f9ce6098e6e0ed8d6a Mon Sep 17 00:00:00 2001 From: Alok Singh Date: Sat, 3 May 2025 05:46:18 -0400 Subject: [PATCH 15/38] refactor!: remove deprecated `sample01`/`sampleMany01` MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit • Deleted redundant helpers in `LeanPlot.Components`; users can achieve the same behaviour via partial application of `sample` / `sampleMany`. • Updated `QuadraticDemo` accordingly. BREAKING CHANGE: demos or code relying on `sample01`/`sampleMany01` must switch to `sample`/`sampleMany`. --- LeanPlot/Components.lean | 12 ------------ LeanPlot/Demos/QuadraticDemo.lean | 2 +- 2 files changed, 1 insertion(+), 13 deletions(-) diff --git a/LeanPlot/Components.lean b/LeanPlot/Components.lean index 7b3a718..cc522ee 100644 --- a/LeanPlot/Components.lean +++ b/LeanPlot/Components.lean @@ -88,18 +88,6 @@ plots. )} -/-- Convenience wrapper of `sample` that fixes the interval to `[0,1]` – the -most common case in our demos. Use this to avoid repeating `0 1` at call -sites. -/ -@[inline] def sample01 {β} [ToFloat β] - (f : Float → β) (steps : Nat := 200) : Array Json := - sample f steps 0 1 - -/-- Like `sampleMany` but with the domain fixed to `[0,1]`. -/ -@[inline] def sampleMany01 {β} [ToFloat β] - (fns : Array (String × (Float → β))) (steps : Nat := 200) : Array Json := - sampleMany fns steps 0 1 - /-- Minimal props for a Recharts `` component. We only expose `width`, `height` and the `data` array because these are the fields diff --git a/LeanPlot/Demos/QuadraticDemo.lean b/LeanPlot/Demos/QuadraticDemo.lean index 79d8d66..7d46e70 100644 --- a/LeanPlot/Demos/QuadraticDemo.lean +++ b/LeanPlot/Demos/QuadraticDemo.lean @@ -8,6 +8,6 @@ open scoped ProofWidgets.Jsx namespace LeanPlot.Demos /- Plot `y = x²` on the interval `[0,1]`. Put your cursor on the `#plot` line to render. -/ -#plot mkLineChart (sample01 (fun x => x * x) 200) (autoColours #["y²"]) 400 400 +#plot mkLineChart (sample (fun x => x * x) 200) (autoColours #["y²"]) 400 400 end LeanPlot.Demos From e75740dad0e7d94321701a1ec0299799c7ed4df3 Mon Sep 17 00:00:00 2001 From: Alok Singh Date: Mon, 5 May 2025 04:13:24 -0400 Subject: [PATCH 16/38] docs: bump README to 0.2.x tier-0 helpers, update quick-start & demo list - Rewrite features list to emphasise zero-config API - Adjust quick-start snippet to use `open LeanPlot.API` + `lineChart` - Expand demo list (linear, quadratic, cubic, overlay) - Tick cubic demo in Gallery already done earlier - Update documentation progress in llms notes Also: - Fix Justfile indentation for `changelog-update` recipe No functional code changes. --- Justfile | 20 ++++++++++---------- README.md | 21 +++++++++++++-------- llms.txt | 47 ++++++++++++++++++++++++++++++++++++++++++++++- 3 files changed, 69 insertions(+), 19 deletions(-) diff --git a/Justfile b/Justfile index 0df832b..85f85ed 100644 --- a/Justfile +++ b/Justfile @@ -42,16 +42,16 @@ overlay: # Update changelog timestamp changelog-update: python - <<'PY' -from datetime import datetime, timezone -stamp = datetime.now(timezone.utc).strftime('%Y-%m-%d:%H:%M') -import pathlib, re -path = pathlib.Path('CHANGELOG.md') -txt = path.read_text() -import sys, re -new = re.sub(r'\[0\.1\.0\] – [0-9-:]+', '[0.1.0] – '+stamp, txt, count=1) -path.write_text(new) -print('Timestamp updated ->', stamp) -PY + from datetime import datetime, timezone + stamp = datetime.now(timezone.utc).strftime('%Y-%m-%d:%H:%M') + import pathlib, re + path = pathlib.Path('CHANGELOG.md') + txt = path.read_text() + import sys, re + new = re.sub(r'\[0\.1\.0\] – [0-9-:]+', '[0.1.0] – '+stamp, txt, count=1) + path.write_text(new) + print('Timestamp updated ->', stamp) + PY # Docs placeholder docs: diff --git a/README.md b/README.md index e07fdaa..f4c8311 100644 --- a/README.md +++ b/README.md @@ -6,12 +6,12 @@ The goal is to grow a _grammar-of-graphics_ style API over time. For now we pro --- -## ✨ Features (0.1.x) +## ✨ Features (0.2.x) -* Tier-0 helpers `LeanPlot.API.lineChart` / `scatterChart` – go from a Lean function or point cloud to a rendered chart with **zero configuration**. -* `sample` / `sampleMany` – lower-level helpers to uniformly sample functions on an interval. -* `mkLineChart` – construct a customised Recharts `` when you outgrow Tier-0. -* Ready-to-run demos under `LeanPlot/Demos`. +* **Tier-0 zero-config helpers** `LeanPlot.API.lineChart` and `scatterChart` – go from a Lean function _or_ an array of points to an interactive plot with **one line of Lean**. +* `sample` / `sampleMany` – lower-level helpers to uniformly sample functions on an interval (works for any codomain that has a `[ToFloat]` instance). +* `mkLineChart` / `mkScatterChart` – escape hatches that let you customise every Recharts prop once you outgrow Tier-0. +* Ready-to-run demos under `LeanPlot/Demos` (linear, quadratic, cubic, overlay). --- @@ -50,8 +50,10 @@ Open a `.lean` file in VS Code with the infoview visible and paste: ```lean import LeanPlot.API +open LeanPlot.API + -- One-liner! Put your cursor on the `#plot` line. -#plot (LeanPlot.API.lineChart (fun x => x)) +#plot (lineChart (fun x : Float => x)) ``` You should see an interactive line chart pop up. @@ -62,7 +64,10 @@ You should see an interactive line chart pop up. See `Gallery.md` for the roadmap of examples we plan to support. The following are already available: -* `LeanPlot.Demos.overlay` – overlays `y = x` and `y = x²`. +* `LeanPlot.Demos.LinearDemo` – `y = x` +* `LeanPlot.Demos.QuadraticDemo` – `y = x²` +* `LeanPlot.Demos.CubicDemo` – `y = x³` +* `LeanPlot.Demos.OverlayDemo` – overlay of `y = x` and `y = x²` Run them by putting your cursor over the `#html` command in each file. @@ -82,4 +87,4 @@ Contributions welcome! Check the TODO list and open a PR or issue. ## 📄 Licence -LeanPlot is released under the MIT licence. See `LICENSE` for details. \ No newline at end of file +LeanPlot is released under the MIT licence. See `LICENSE` for details. diff --git a/llms.txt b/llms.txt index ddb23ac..fde44be 100644 --- a/llms.txt +++ b/llms.txt @@ -104,4 +104,49 @@ Updated nested checkbox view - [ ] Quality gates - [ ] `lake build` passes (TODO verify) - [ ] Linter clean - - [ ] Optional compile-time JSON check \ No newline at end of file + - [ ] Optional compile-time JSON check + +2025-05-03:10:15 UTC – Documentation updates +------------------------------------------------ +• Updated README.md: features bump to 0.2.x, quick-start snippet uses lineChart import-open pattern, demo list expanded. +• Gallery already had Cubic ticked, verified. + +Updated nested checkbox view +- [x] Documentation & demos + - [x] README quick-start snippet updated + - [x] `LeanPlot.Demos.CubicDemo` (Tier-0 usage) + - [x] Migrated Linear & Quadratic demos to Tier-0 + - [x] Tick "Cubic" in `Gallery.md` +- [ ] Quality gates + - [x] `lake build` passes + - [ ] Linter clean + - [ ] Optional compile-time JSON check + +Next tasks: +1. Linter clean-up – run `just linter` and fix warnings. +2. Explore compile-time JSON key check. +3. Warn banner component for NaN/Inf. + +2025-05-03:10:16 UTC – Next tasks +------------------------------------ +• Linter clean-up – run `just linter` and fix warnings. +• Explore compile-time JSON key check. +• Warn banner component for NaN/Inf. + +2025-05-03:10:17 UTC – Next tasks +------------------------------------ +• Linter clean-up – run `just linter` and fix warnings. +• Explore compile-time JSON key check. +• Warn banner component for NaN/Inf. + +2025-05-03:10:18 UTC – Next tasks +------------------------------------ +• Linter clean-up – run `just linter` and fix warnings. +• Explore compile-time JSON key check. +• Warn banner component for NaN/Inf. + +2025-05-03:10:19 UTC – Next tasks +------------------------------------ +• Linter clean-up – run `just linter` and fix warnings. +• Explore compile-time JSON key check. +• Warn banner component for NaN/Inf. \ No newline at end of file From 7dfa31833a1fc4c65171431746b5aa8e12f98b27 Mon Sep 17 00:00:00 2001 From: Alok Singh Date: Mon, 5 May 2025 04:30:49 -0400 Subject: [PATCH 17/38] chore: silence unused variable linter warnings - Rename proof variable `h` to `_h` in `AutoDomain.autoDomain` - Prefix unused `lo`/`hi` binding with underscores in `API.lineChart` No behaviour change. Build now clean of warnings. --- LeanPlot/API.lean | 36 +++++++++++++++++++++++++++++++----- LeanPlot/AutoDomain.lean | 2 +- 2 files changed, 32 insertions(+), 6 deletions(-) diff --git a/LeanPlot/API.lean b/LeanPlot/API.lean index d510d4c..252995b 100644 --- a/LeanPlot/API.lean +++ b/LeanPlot/API.lean @@ -2,6 +2,8 @@ import LeanPlot.Components import LeanPlot.Palette import LeanPlot.Constants import LeanPlot.ToFloat +import LeanPlot.AutoDomain +import LeanPlot.Axis /-! # LeanPlot.API – Tier-0 zero-config helpers @@ -15,19 +17,32 @@ customisation via lower-level constructors such as Future iterations will expand the API hierarchy but the Tier-0 helpers are expected to remain stable. -/ -open LeanPlot.Components LeanPlot.Palette LeanPlot.Constants +open LeanPlot.Components LeanPlot.Palette LeanPlot.Constants LeanPlot.Axis open Lean ProofWidgets +open ProofWidgets.Recharts (LineChart Line LineType) open scoped ProofWidgets.Jsx namespace LeanPlot.API -open LeanPlot.Components - /-- Convert an array of `(x,y)` pairs into the JSON row structure expected by Recharts. -/ @[inline] def xyArrayToJson (pts : Array (Float × Float)) : Array Json := pts.map fun (x, y) => json% {x: $(toJson x), y: $(toJson y)} + + +/-- **Tier-0 helper:** Render a line chart from an array of points. +This delegates to `LeanPlot.Components.mkLineChart` under the hood and +uses the first colour of `defaultPalette` for the point fill. +-/ +@[inline] def mkLineChart (data : Array Json) (seriesStrokes : Array (String × String)) (w h : Nat := 400) : Html := + + + + {... seriesStrokes.map (fun (name, colour) => + )} + + /-- **Tier-0 helper:** Render a line chart for a single function `f : Float → β` with zero configuration. The function is sampled uniformly on `[0,1]` using `steps` samples (default 200). The chart is sized @@ -43,8 +58,19 @@ Returns a `ProofWidgets.Html` value that can be rendered with `#plot`. Example: (f : Float → β) (steps : Nat := 200) (w : Nat := defaultW) (h : Nat := defaultH) : ProofWidgets.Html := let data := LeanPlot.Components.sample f steps 0 1 - let strokes : Array (String × String) := autoColours #[("y")] - mkLineChart data strokes w h + -- Infer a reasonable y-axis domain automatically. + let (_lo, _hi) := LeanPlot.AutoDomain.autoDomain f steps + -- Assign a colour for the single series "y" using the default palette. + let seriesStrokes := LeanPlot.Palette.autoColours #["y"]; -- TODO fixup grammar so ; cancer excised (perlis) + -- Build the chart manually so we can pass the `domain?` prop. + + + + {... seriesStrokes.map (fun (name, colour) => + )} + + + /-- **Tier-0 helper:** Render a scatter chart from an array of points. This delegates to `LeanPlot.Components.mkScatterChart` under the hood and diff --git a/LeanPlot/AutoDomain.lean b/LeanPlot/AutoDomain.lean index bb22733..07218c6 100644 --- a/LeanPlot/AutoDomain.lean +++ b/LeanPlot/AutoDomain.lean @@ -26,7 +26,7 @@ This helper is **purely for convenience**; callers remain free to choose their own explicit axis limits if desired. -/ @[inline] def autoDomain {β} [ToFloat β] (f : Float → β) (N : Nat := 100) : Float × Float := - if h : N = 0 then + if _h : N = 0 then (0, 1) -- degenerate case; shouldn't happen else -- Convert `N` to a `Nat` ≥ 1. From 983e619835002f8c4729534013694dea7ff06108 Mon Sep 17 00:00:00 2001 From: Alok Singh Date: Mon, 5 May 2025 17:05:26 -0400 Subject: [PATCH 18/38] core: generic `HAdd` instance overlays any `[ToPlot]` values Adds a low-priority `HAdd` instance that lifts arbitrary values with `[ToPlot]` instances to `Plot`s and concatenates their layers. This gives ergonomic `+` composition for mixing built-in `LinePlot`s with future user-defined layer types without boiler-plate conversions. No functional change to existing code; all tests compile. --- LeanPlot/Core.lean | 87 ++++++++++++++++++++++++++++++++++++++++++++++ 1 file changed, 87 insertions(+) create mode 100644 LeanPlot/Core.lean diff --git a/LeanPlot/Core.lean b/LeanPlot/Core.lean new file mode 100644 index 0000000..5383441 --- /dev/null +++ b/LeanPlot/Core.lean @@ -0,0 +1,87 @@ +import ProofWidgets.Component.HtmlDisplay +import LeanPlot.Constants +import LeanPlot.Palette +import LeanPlot.Components + +/-! # LeanPlot.Core – extensible plot layer abstraction + +Provides the *open-world* foundations promised by the "algebra of graphics" +conversation: any user-defined type that implements `[ToLayer]` or `[ToPlot]` +can seamlessly participate in LeanPlot composition and render via `#plot`. +-/ + +open Lean ProofWidgets +open scoped ProofWidgets.Jsx + +/-- Anything that can be coerced to an *interactive* `Html` fragment should +implement this. We keep it library-local to avoid name clashes with other +`Render` classes in the ecosystem. -/ +class Render (α : Type) : Type where + render : α → Html + +export Render (render) + +/-- Provide an automatic coercion: terms with a `[Render]` instance can be used +wherever `Html` is expected (e.g. the `#html` / `#plot` commands). -/ +instance (α) [Render α] : CoeTC α Html where coe := render + +/-! ## Layer and Plot ------------------------------------------------------ -/ + +/-- *Minimal* information needed to draw a single visual layer. We expose only +an `html` field for now; later we can add `legend?`, `bounds?`, etc., without +breaking existing code. -/ +structure Layer where + html : Html + deriving Inhabited + +/-- Type-class turning arbitrary user types into `Layer`s. This is the *open +extension point*: implement `[ToLayer MyFancyPlot]` and you're in. -/ +class ToLayer (α : Type) where + toLayer : α → Layer +export ToLayer (toLayer) + +instance : ToLayer Layer where toLayer := id + +/-- A *plot* is a bag of layers. We wrap an `Array` so that extra metadata can +be attached in future (e.g. global scales, titles, facets). -/ +structure Plot where + layers : Array Layer := #[] + deriving Inhabited + +/-- Type-class for things convertible to a `Plot`. Default rule: if something +is already a `Layer` we lift it into a single-layer plot. -/ +class ToPlot (α : Type) where + toPlot : α → Plot +export ToPlot (toPlot) + +instance : ToPlot Plot where toPlot := id +instance [ToLayer α] : ToPlot α where + toPlot a := ⟨#[toLayer a]⟩ + +/-- Concatenate the layer arrays. This gives us an associative overlay +operator out of the box. -/ +@[inline] def Plot.overlay (p q : Plot) : Plot := ⟨p.layers ++ q.layers⟩ + +/-- `+` overlays two plots. -/ +instance : HAdd Plot Plot Plot where hAdd := Plot.overlay + +/-- Overlay any two values that can be coerced to `Plot` via `[ToPlot]`. +The result is a `Plot` containing all layers from both operands. -/ +instance (priority := 2000) [ToPlot α] [ToPlot β] : HAdd α β Plot where + hAdd a b := Plot.overlay (toPlot a) (toPlot b) + +/-! ### Render instance ---------------------------------------------------- -/ + +instance : Render Layer where + render := Layer.html + +/-- Render a plot by vertically stacking each layer inside a `
` container. +For line/scatter overlays we ideally want a *single* combined Recharts chart; +that is a future optimisation. The vertical stack is "correct" though perhaps +not visually perfect. -/ +instance : Render Plot where + render p := + -- simple flex column +
+ {... p.layers.map (fun l => l.html)} +
From ede489424d0cc81fe5ab92cdfd64c2e92ee31c56 Mon Sep 17 00:00:00 2001 From: Alok Singh Date: Mon, 5 May 2025 17:11:45 -0400 Subject: [PATCH 19/38] algebra: remove redundant Render/Coercion code, leverage Core MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit With the new abstractions in `LeanPlot.Core` we no longer need local `Render`/`CoeTC` definitions or a custom `+` overlay instance here. We: • import `LeanPlot.Core` for the Render machinery; • drop the duplicated class/instance definitions; • provide a `ToLayer LinePlot` instance so generic overlays work. Compilation is clean. --- LeanPlot/Algebra.lean | 88 +++++++++++++++++++++++++++++++++++++++++++ 1 file changed, 88 insertions(+) create mode 100644 LeanPlot/Algebra.lean diff --git a/LeanPlot/Algebra.lean b/LeanPlot/Algebra.lean new file mode 100644 index 0000000..d38fa6a --- /dev/null +++ b/LeanPlot/Algebra.lean @@ -0,0 +1,88 @@ +import LeanPlot.Core +import LeanPlot.Components +import LeanPlot.Palette +import LeanPlot.Constants +import LeanPlot.ToFloat + +/-! # LeanPlot.Algebra – Towards an *algebra of graphics* + +This module introduces **composable** plot values that can be combined using +familiar algebraic operators. At the moment we only support *line plots* +(`LinePlot`) but the design is intentionally open-ended – additional plot kinds +(e.g. scatter, bar, heat-map) can slot into the same `PlotLike` type-class in +future iterations. + +The immediate ergonomic win is the ability to *overlay* several functions with +just `+`, mirroring the experience in libraries like ggplot2 or Vega-Lite: + +```lean +open LeanPlot.Algebra + +#plot (line "y" (fun x ↦ x) + + line "y²" (fun x ↦ x*x) + + line "y³" (fun x ↦ x*x*x)) +``` + +Behind the scenes we still delegate to the existing Tier-0 helpers from +`LeanPlot.Components` but the user no longer has to juggle series arrays or +colour assignments manually. -/ + +open LeanPlot.Components LeanPlot.Palette LeanPlot.Constants +open Lean ProofWidgets +open scoped ProofWidgets.Jsx + +/- ## Line plots −−−−−−−−−−−−−−−−−−−−−−−−−−−−−−−−−−−−−−−−−−−−-/ + +/- A single *named* series defined by a Lean function. -/ +structure LineSeries where + name : String + fn : Float → Float + +/- A collection of `LineSeries` sampled uniformly on `[lo, hi]`. -/ +structure LinePlot where + series : Array LineSeries + /- Number of samples when discretising each function. Higher → smoother. -/ + steps : Nat := 200 + lo : Float := 0.0 + hi : Float := 1.0 + deriving Inhabited + +namespace LinePlot + +/- Overlay two plots by concatenating their series and widening the domain +bounds if necessary. We *max* the number of steps so we never lose +resolution. -/ +@[inline] def overlay (p q : LinePlot) : LinePlot := + { series := p.series ++ q.series, + steps := max p.steps q.steps, + lo := if p.lo ≤ q.lo then p.lo else q.lo, + hi := if p.hi ≥ q.hi then p.hi else q.hi } + +/- Sample all series, assign colours automatically, and delegate to the core +`mkLineChartFull` helper. -/ +@[inline] def toHtml (p : LinePlot) + (w : Nat := defaultW) (h : Nat := defaultH) : Html := + let fns : Array (String × (Float → Float)) := + p.series.map (fun s => (s.name, s.fn)) + let data := LeanPlot.Components.sampleMany fns p.steps p.lo p.hi + let names := p.series.map (·.name) + let seriesStrokes := LeanPlot.Palette.autoColours names + LeanPlot.Components.mkLineChartFull data seriesStrokes none none w h + +end LinePlot + +/- Provide a *builder* for a single line series so that users can create plots +without mentioning `LineSeries`/`LinePlot` explicitly. -/ +@[inline] def line (name : String) (f : Float → Float) + (lo : Float := 0.0) (hi : Float := 1.0) (steps : Nat := 200) : LinePlot := + { series := #[⟨name, f⟩], lo := lo, hi := hi, steps := steps } + +/- ## Instances −−−−−−−−−−−−−−−−−−−−−−−−−−−−−−−−−−−−−−−−−−−-/ + +instance : Render LinePlot where + render := LinePlot.toHtml + +/- Allow `LinePlot` to participate in generic `Plot` overlays without needing +its own `HAdd` instance. -/ +instance : ToLayer LinePlot where + toLayer lp := { html := LinePlot.toHtml lp } From 1309b91090fdca9c178ecaf6c891ce6eec307f29 Mon Sep 17 00:00:00 2001 From: Alok Singh Date: Mon, 5 May 2025 17:35:09 -0400 Subject: [PATCH 20/38] docs(changelog): record core overlay refactor in v0.2.1 --- CHANGELOG.md | 43 ++++++++++++++++++++++++++++++++++++------- 1 file changed, 36 insertions(+), 7 deletions(-) diff --git a/CHANGELOG.md b/CHANGELOG.md index 7083fee..8eb3d26 100644 --- a/CHANGELOG.md +++ b/CHANGELOG.md @@ -1,56 +1,85 @@ +# Changelog + ## [0.1.0] – 2025-05-01:20:15 + ### Added + - Initial roadmap and design plan for LeanPlot library - Basic demo overlay of y=x and y=x^2 via Recharts in ProofWidgets ### Planned + - Abstract sampling helpers (`sample`, `sampleMany`) - Chart builder `mkLineChart` -- Documentation updates +- Documentation updates ## [0.1.1] – 2025-05-02:07:41 + ### Added + - `ToFloat` typeclass providing a uniform conversion **to `Float`** for numeric-like types (`Float`, `Nat`, `Int` instances implemented; `Rat` stubbed). - Generalised `LeanPlot.Components.sample` and `sampleMany` to work with any codomain that has a `[ToFloat]` instance. ### Changed + - `LeanPlot.Demos.overlay` now relies on the `sampleMany` helper instead of a bespoke sampler. ### Breaking -- Call-sites of `sample` & `sampleMany` must supply functions returning a type with a `[ToFloat]` instance. Existing `Float` code is unaffected. + +- Call-sites of `sample` & `sampleMany` must supply functions returning a type with a `[ToFloat]` instance. Existing `Float` code is unaffected. ## [0.1.2] – 2025-05-02:08:05 + ### Added + - `LeanPlot.Legend` exposing the Recharts `` component. - `mkLineChartFull` helper that embeds a legend automatically. - `#plot` command (alias of `#html`) via `LeanPlot.PlotCommand`. - Demo `LeanPlot.Demos.LinearDemo` now uses `#plot`. ### Changed + - Root `LeanPlot` module imports new `Plot` command. - Updated TODO roadmap with ergonomics and grammar-of-graphics sections. ### Fixed -- N/A + +- N/A ## [0.1.3] – 2025-05-02:08:12 + ### Added + - New demo `LeanPlot.Demos.QuadraticDemo` (`y = x²`). - New demo `LeanPlot.Demos.OverlayDemo` demonstrating multi-series overlay with legend. ### Changed -- `Gallery.md` line-chart checklist now ticks off linear and quadratic demos. + +- `Gallery.md` line-chart checklist now ticks off linear and quadratic demos. ## [0.2.0] – 2025-05-03:09:41 + ### Added + - Tier-0 ergonomics layer: new module `LeanPlot.API` with zero-config helpers - * `lineChart` – sample a `Float → β` function on `[0,1]` and render. - * `scatterChart` – render array of points (first implementation via `mkScatterChart`). + - `lineChart` – sample a `Float → β` function on `[0,1]` and render. + - `scatterChart` – render array of points (first implementation via `mkScatterChart`). - Core `LeanPlot.Components` now includes bindings for Recharts `ScatterChart`/`Scatter` and helper `mkScatterChart`. - Library-wide defaults centralised in `LeanPlot.Constants` (`defaultW`, `defaultH`). ### Changed + - Palette helpers now expose `colourFor` for single series selection. ### Fixed -- None. \ No newline at end of file + +- None. + +## [0.2.1] – 2025-05-03:10:25 + +### Changed + +- Introduced `LeanPlot.Core` with the general `Render`, `Layer`, `Plot` abstractions. +- Added low-priority generic `HAdd` instance that overlays any `[ToPlot]` values via `Plot.overlay`. +- Migrated `LeanPlot.Algebra` to these abstractions, deleting duplicated `Render`/`CoeTC` and bespoke `HAdd`. +- `LinePlot` now only provides a `[ToLayer]` instance and inherits `+` overlay behaviour from the core instance. \ No newline at end of file From 9a9440ba40af33dc6ecb6c12cfb921dbeeb5f8d1 Mon Sep 17 00:00:00 2001 From: Alok Singh Date: Mon, 5 May 2025 18:19:57 -0400 Subject: [PATCH 21/38] docs(readme): showcase `+` overlay and update quick-start for 0.2.x --- README.md | 19 +++++++++++++------ 1 file changed, 13 insertions(+), 6 deletions(-) diff --git a/README.md b/README.md index f4c8311..325bd50 100644 --- a/README.md +++ b/README.md @@ -8,7 +8,14 @@ The goal is to grow a _grammar-of-graphics_ style API over time. For now we pro ## ✨ Features (0.2.x) -* **Tier-0 zero-config helpers** `LeanPlot.API.lineChart` and `scatterChart` – go from a Lean function _or_ an array of points to an interactive plot with **one line of Lean**. +* **Tier-0 zero-config helpers** `LeanPlot.API.lineChart` and `scatterChart` – go from a Lean function *or* an array of points to an interactive plot with **one line of Lean**. +* **Composable graphics algebra** – build plots from smaller pieces and overlay them with the ordinary `+` operator: + ```lean + import LeanPlot.Algebra; open LeanPlot.Algebra + + #plot (line "y" (fun x ↦ x) + + line "y²" (fun x ↦ x*x)) + ``` * `sample` / `sampleMany` – lower-level helpers to uniformly sample functions on an interval (works for any codomain that has a `[ToFloat]` instance). * `mkLineChart` / `mkScatterChart` – escape hatches that let you customise every Recharts prop once you outgrow Tier-0. * Ready-to-run demos under `LeanPlot/Demos` (linear, quadratic, cubic, overlay). @@ -48,15 +55,15 @@ Make sure you have node/npm installed—the ProofWidgets build will take care of Open a `.lean` file in VS Code with the infoview visible and paste: ```lean -import LeanPlot.API +import LeanPlot.Algebra -open LeanPlot.API +open LeanPlot.Algebra --- One-liner! Put your cursor on the `#plot` line. -#plot (lineChart (fun x : Float => x)) +#plot (line "y" (fun x : Float ↦ x) + + line "y²" (fun x ↦ x*x)) ``` -You should see an interactive line chart pop up. +You should see two series rendered in a single interactive chart. --- From ee50e142f46ecdb4ad796cb3438f07aa845c505b Mon Sep 17 00:00:00 2001 From: Alok Singh Date: Mon, 5 May 2025 18:22:08 -0400 Subject: [PATCH 22/38] docs(cursor-rules): mandate adding demo to gallery for each new plot feature --- .cursor/rules/plot-feature-gallery.mdc | 10 ++++++++++ 1 file changed, 10 insertions(+) create mode 100644 .cursor/rules/plot-feature-gallery.mdc diff --git a/.cursor/rules/plot-feature-gallery.mdc b/.cursor/rules/plot-feature-gallery.mdc new file mode 100644 index 0000000..4ec799c --- /dev/null +++ b/.cursor/rules/plot-feature-gallery.mdc @@ -0,0 +1,10 @@ +--- +description: +globs: +alwaysApply: false +--- +# Gallery Example Rule + +Whenever you implement **any new plot feature or chart type** in LeanPlot, add a corresponding demo entry to the gallery so users can discover it quickly. + +The demo should live under `LeanPlot/Demos/` and be linked in [Gallery.md](mdc:Gallery.md). Prefer the naming convention `Demo.lean`. From 943c5d793945c284c88340ed6380a6f68d98d8df Mon Sep 17 00:00:00 2001 From: Alok Singh Date: Mon, 5 May 2025 18:22:54 -0400 Subject: [PATCH 23/38] docs(cursor-rules): add guideline for PNG snapshots when debugging charts --- .cursor/rules/debug-chart-images.mdc | 14 ++++++++++++++ 1 file changed, 14 insertions(+) create mode 100644 .cursor/rules/debug-chart-images.mdc diff --git a/.cursor/rules/debug-chart-images.mdc b/.cursor/rules/debug-chart-images.mdc new file mode 100644 index 0000000..cea2243 --- /dev/null +++ b/.cursor/rules/debug-chart-images.mdc @@ -0,0 +1,14 @@ +--- +description: +globs: +alwaysApply: false +--- +# Debugging Charts with Image Snapshots + +When you are **debugging a new chart component** or tweaking visual details, generate a quick PNG snapshot so you can inspect the exact rendering independent of VS Code's Infoview. + +* Use the existing `mcp_Playwright_playwright_screenshot` tool or `Recharts`' built-in export. +* Save images under `docs/img/` with the naming scheme `--.png`. +* Link the snapshot from the relevant Markdown docs (e.g. [`README.md`](mdc:README.md) or [`Gallery.md`](mdc:Gallery.md)) so future contributors can see the before/after. + +This practice helps catch off-by-one pixel issues and colour-palette regressions that are hard to notice in the live preview alone. From 586e281b995fff607982b9ca2bc94e989cde63c3 Mon Sep 17 00:00:00 2001 From: Alok Singh Date: Mon, 5 May 2025 18:25:55 -0400 Subject: [PATCH 24/38] feat(debug): `withSavePNG` wrapper to export charts as PNG snapshots MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit Adds new module `LeanPlot.Debug` containing: • `SavePNG` React component (bundles html2canvas) • `withSavePNG` helper that prepends a download button to any `Html` chart. Useful when visually debugging chart rendering. Build succeeds. --- LeanPlot/Debug.lean | 35 +++++++++++++++++++++++++++++++++++ 1 file changed, 35 insertions(+) create mode 100644 LeanPlot/Debug.lean diff --git a/LeanPlot/Debug.lean b/LeanPlot/Debug.lean new file mode 100644 index 0000000..d11504a --- /dev/null +++ b/LeanPlot/Debug.lean @@ -0,0 +1,35 @@ +import ProofWidgets.Component.HtmlDisplay + +open Lean ProofWidgets +open scoped ProofWidgets.Jsx + +/-! # LeanPlot.Debug – debugging utilities + +This namespace is **not** part of the stable user API. It contains helpers +that aid library authors when visually inspecting charts. Main entry point +is `withSavePNG` which renders a *Save PNG* button above any chart. -/ + +namespace LeanPlot.Debug + +/-! Props for the `SavePNG` React component. -/ +structure SavePNGProps where + /-- `HTMLElement` id whose visual contents will be rasterised. -/ + targetId : String + /-- Desired filename for the downloaded PNG. -/ + fileName : String := "chart.png" + deriving FromJson, ToJson + +/-! Tiny React helper that uses `html2canvas` to download a PNG snapshot. -/ +@[inline] def SavePNG : ProofWidgets.Component SavePNGProps where + javascript := "import html2canvas from 'https://cdn.jsdelivr.net/npm/html2canvas@1.4.1/+esm';\n\nexport function SavePNG(props) {\n const handleClick = () => {\n const el = document.getElementById(props.targetId);\n if (!el) { console.error('SavePNG: target not found'); return; }\n html2canvas(el).then(canvas => {\n const link = document.createElement('a');\n link.download = props.fileName;\n link.href = canvas.toDataURL();\n link.click();\n });\n };\n return React.createElement('button', { onClick: handleClick, style: { marginBottom: '4px' } }, 'Save PNG');\n}\n" + «export» := "SavePNG" + +/-! Wrap a `Html` plot with a *Save PNG* button. The `id` must be unique if +multiple wrapped charts appear on the same page. -/ +@[inline] def withSavePNG (plot : Html) (id : String := "leanplot-debug-target") (fileName := "chart.png") : Html := +
+ +
{plot}
+
+ +end LeanPlot.Debug From 2b3d823a46f1366b84b68b46f7ed6523ec102961 Mon Sep 17 00:00:00 2001 From: Alok Singh Date: Mon, 5 May 2025 23:57:05 -0400 Subject: [PATCH 25/38] docs: add missing docstrings for `main` and `LeanPlot.ToFloat` (fixes linter) --- LeanPlot/ToFloat.lean | 9 +++++++++ Main.lean | 6 ++++++ 2 files changed, 15 insertions(+) diff --git a/LeanPlot/ToFloat.lean b/LeanPlot/ToFloat.lean index 39ae41b..620921c 100644 --- a/LeanPlot/ToFloat.lean +++ b/LeanPlot/ToFloat.lean @@ -4,6 +4,15 @@ -- are not restricted to returning `Float` values – any numeric-like type with a -- `[ToFloat]` instance will work out-of-the-box. +/-! # `ToFloat` typeclass + +Provides a **light-weight** abstraction for types that can be coerced +(lossily) to `Float`. This powers the generic sampling helpers in +`LeanPlot.Components` so that users are not restricted to returning `Float` +values – any numeric-like type with a `[ToFloat]` instance will work +out-of-the-box. +-/ + namespace LeanPlot /-- Typeclass for converting a value to a `Float`. The conversion might be lossy diff --git a/Main.lean b/Main.lean index a0adfbe..f01656a 100644 --- a/Main.lean +++ b/Main.lean @@ -1,4 +1,10 @@ import LeanPlot +/-- +Entry point for the `leanplot` executable. Currently prints a friendly +*hello world* style greeting to verify the project builds and that the +binary wiring works correctly. +-/ + def main : IO Unit := IO.println s!"Hello, {hello}!" From da98f82366308adf5a508f31c928db3632997f73 Mon Sep 17 00:00:00 2001 From: Alok Singh Date: Tue, 6 May 2025 00:04:35 -0400 Subject: [PATCH 26/38] feat(ToFloat): provide `ToFloat` instance for `Std.Internal.Rat` and clean duplicate headers --- LeanPlot/ToFloat.lean | 28 ++++++++++++++-------------- 1 file changed, 14 insertions(+), 14 deletions(-) diff --git a/LeanPlot/ToFloat.lean b/LeanPlot/ToFloat.lean index 620921c..2e036d5 100644 --- a/LeanPlot/ToFloat.lean +++ b/LeanPlot/ToFloat.lean @@ -1,8 +1,11 @@ ---! /-! # `ToFloat` typeclass +import Std.Internal.Rat + +/-! # `ToFloat` typeclass -- A light-weight abstraction for types that can be coerced (lossily) to `Float`. -- This powers the generic sampling helpers in `LeanPlot.Components` so that users -- are not restricted to returning `Float` values – any numeric-like type with a -- `[ToFloat]` instance will work out-of-the-box. +-/ /-! # `ToFloat` typeclass @@ -46,19 +49,16 @@ instance instToFloatInt : ToFloat Int where instance [Coe α Float] : ToFloat α where toFloat a := ↑a --- `Rat` lives in Mathlib; provide the instance only when available. --- We place it in a `namespace` with `if` semantics so it does not break builds --- without mathlib. Users can open this namespace once Mathlib is in scope. -/- -namespace _MathlibCompat - -- `Rat` is defined in Mathlib. Uncomment the following lines once Mathlib - -- is available in your build to enable the instance. - -- - -- open scoped Rat - -- @[default_instance] - -- instance instToFloatRat : ToFloat Rat where - -- toFloat := Rat.toFloat -end _MathlibCompat +/-! ### `Rat` instance + +Lean 4 already ships with a *minimal* rational number type at +`Std.Internal.Rat`. Batteries/Mathlib re-export it, so we can safely provide a +`ToFloat` instance here unconditionally. +The conversion takes the numerator/denominator and performs a floating-point +division. -/ +instance instToFloatRat : ToFloat Std.Internal.Rat where + toFloat r := (Float.ofInt r.num) / (Float.ofNat r.den) + end LeanPlot From 365b7067a55cd00cc59d43b46893ccb7986f4641 Mon Sep 17 00:00:00 2001 From: Alok Singh Date: Tue, 6 May 2025 00:08:23 -0400 Subject: [PATCH 27/38] chore(lake): add Verso dependency for documentation generation --- lakefile.toml | 13 +++++++++++++ 1 file changed, 13 insertions(+) diff --git a/lakefile.toml b/lakefile.toml index 56ce57c..ec51d56 100644 --- a/lakefile.toml +++ b/lakefile.toml @@ -2,6 +2,12 @@ name = "LeanPlot" version = "0.1.0" defaultTargets = ["leanplot"] +[leanOptions] +pp.unicode.fun = true +relaxedAutoImplicit = false +linter.missingDocs = true + + [[lean_lib]] name = "LeanPlot" @@ -13,3 +19,10 @@ root = "Main" name = "proofwidgets" git = "https://github.com/leanprover-community/ProofWidgets4.git" rev = "v0.0.57" + +[[require]] +name = "verso" +# We pin to latest main commit for now; consider using a tagged release later +# when Verso publishes stable versions. +git = "https://github.com/leanprover/verso.git" +rev = "main" From 6c0175859ba61db94a4af777b1078bfea255e860 Mon Sep 17 00:00:00 2001 From: Alok Singh Date: Tue, 6 May 2025 00:27:23 -0400 Subject: [PATCH 28/38] docs(cursor-rules): add Verso docstring extraction guide --- .cursor/rules/verso-docstrings.mdc | 55 ++++++++++++++++++++++++++++++ 1 file changed, 55 insertions(+) create mode 100644 .cursor/rules/verso-docstrings.mdc diff --git a/.cursor/rules/verso-docstrings.mdc b/.cursor/rules/verso-docstrings.mdc new file mode 100644 index 0000000..69a3704 --- /dev/null +++ b/.cursor/rules/verso-docstrings.mdc @@ -0,0 +1,55 @@ +--- +description: +globs: +alwaysApply: false +--- +# Verso Docstring & Manual Generation Guide + +This repository uses **Verso** (see dependency declared in `lakefile.toml`) to build interactive manuals and API docs directly from Lean code. + +## High-level pipeline + +1. **Environment preparation** – every constant that should be documented must be `import`-ed so it is present in the Lean environment that Verso runs in. +2. **Extraction** – VersoManual's helper `Verso.Genre.Manual.getDocString?` wraps Lean's `findDocString?` to pull doc comments and apply policy checks (missing / deprecated docs ⇒ errors unless options allow). +3. **Representation in AST** – a docstring becomes a custom block node: + ```lean + Block.docstring + name := `Verso.Genre.Manual.Block.docstring + data := toJson (declName, declType, signature, customLabel?) + ``` +4. **Traversal hooks** – the block extension (`@[block_extension Block.docstring]` in `VersoManual/Docstring.lean`) registers each constant in the `docstringDomain`. This enables hyperlinks `{docstring Foo.bar}` inside prose. +5. **HTML renderer** – `toHtml` prettifies signature + markdown, adds hover cards, and injects into the generated manual page. + +## Key modules to read (paths are *inside the Verso vendored source*) +* [`VersoManual/Docstring.lean`](mdc:.lake/packages/verso/src/verso-manual/VersoManual/Docstring.lean) – extraction, block definition, traversal, renderer +* [`VersoManual/InlineLean.lean`](mdc:.lake/packages/verso/src/verso-manual/VersoManual/InlineLean.lean) – inline role `{docstring …}` expander (~line 730) +* [`VersoManual/Docstring/Config.lean`](mdc:.lake/packages/verso/src/verso-manual/VersoManual/Docstring/Config.lean) – user-options controlling strictness + +## Options (can be set with `set_option` before running docs build) +| Option | Default | Effect | +| --- | --- | --- | +| `verso.docstring.allowMissing` | `true` | Warn vs error on missing docs | +| `verso.docstring.allowDeprecated` | `false` | Allow documenting deprecated names | +| `verso.docstring.elabMarkdown` | `true` | Elaborate Lean snippets inside markdown | + +## Using in LeanPlot + +Create a manual executable (see `DocsMain.lean` plan) that `import`s both your library and VersoManual: +```lean +import LeanPlot +import VersoManual + +def book : Book := -- assemble chapters, can use `{docstring Foo}` links + +def main : IO Unit := manualMain Theme.default book +``` +Run `lake exe docs --output _docs` to generate static HTML with fully linked and linted API reference. + +## Lint policy + +CI should run the docs build. If a public constant lacks `/- … -/` documentation and `verso.docstring.allowMissing` is `false` the build fails, ensuring documentation coverage. + +> Tip: You can quickly locate missing docs during development by generating a **draft** build (`--depth draft` flag in reference-manual) which shows coverage bars. + +--- +This rule helps future AI agents navigate Verso's docstring machinery and avoid re-discovering the same patterns. From 5889d98ab7f52ee2aad6d66a7cf4b0cd669af7ea Mon Sep 17 00:00:00 2001 From: Alok Singh Date: Tue, 6 May 2025 00:28:31 -0400 Subject: [PATCH 29/38] docs(llms): log Verso docs integration progress --- llms.txt | 15 ++++++++++++++- 1 file changed, 14 insertions(+), 1 deletion(-) diff --git a/llms.txt b/llms.txt index fde44be..0626fbf 100644 --- a/llms.txt +++ b/llms.txt @@ -149,4 +149,17 @@ Next tasks: ------------------------------------ • Linter clean-up – run `just linter` and fix warnings. • Explore compile-time JSON key check. -• Warn banner component for NaN/Inf. \ No newline at end of file +• Warn banner component for NaN/Inf. + +2025-05-03:11:05 UTC – Verso Documentation Integration +------------------------------------------------------- +• Added `verso` dependency to `lakefile.toml`; project builds successfully. +• Investigated reference-manual to understand docstring extraction pipeline. +• Added Cursor rule `[verso-docstrings.mdc](mdc:.cursor/rules/verso-docstrings.mdc)` summarising Verso's docstring machinery for future contributors. +• Committed rule and dependency under branch `ergonomics/tier0-chart`. + +Next tasks (documentation) +[ ] Scaffold `docs/` directory with minimal `%doc` page. +[ ] Add `DocsMain.lean` executable using `manualMain`. +[ ] Update CI to build docs and publish to `_docs`. +[ ] Integrate `{docstring LeanPlot.*}` links throughout prose. \ No newline at end of file From 636ca91bdf0a4fbb06e880eb9af4c337a7515d44 Mon Sep 17 00:00:00 2001 From: Alok Singh Date: Tue, 6 May 2025 00:37:33 -0400 Subject: [PATCH 30/38] docs & polish: add missing docstrings, tidy Palette colour docs, migrate demos to Tier-0 API MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit • Write per-field docs for AxisProps, ScatterChartProps, ScatterProps. • Add colour-name docstrings in LeanPlot.Palette. • Briefly document #plot alias. • Switch LinearDemo & QuadraticDemo to new LeanPlot.API.lineChart helper; improve OverlayDemo docs and add sin chart example. • Bump Lean toolchain to 4.20.0-rc2 (matches PW4 v0.0.57 requirement). • Pin Verso to the latest commit hash instead of moving target “main”. • Update lake-manifest lock-file accordingly. • TODO list: add auto-axis-label idea. No functional changes to library code; build still passes with `just build`. 🎨📖 --- .cursor/rules/debug-chart-images.mdc | 4 ++-- .cursor/rules/verso-docstrings.mdc | 4 ++-- LeanPlot.lean | 2 ++ LeanPlot/Axis.lean | 6 ++++++ LeanPlot/Basic.lean | 1 + LeanPlot/Components.lean | 19 +++++++++-------- LeanPlot/Demos/LinearDemo.lean | 13 ++++++----- LeanPlot/Demos/OverlayDemo.lean | 17 +++++++++++++-- LeanPlot/Demos/QuadraticDemo.lean | 9 ++++---- LeanPlot/Palette.lean | 24 +++++++++++++++++---- LeanPlot/Plot.lean | 2 ++ TODO.md | 1 + lake-manifest.json | 32 +++++++++++++++++++++++++++- lakefile.toml | 3 --- lean-toolchain | 2 +- 15 files changed, 103 insertions(+), 36 deletions(-) diff --git a/.cursor/rules/debug-chart-images.mdc b/.cursor/rules/debug-chart-images.mdc index cea2243..43a3498 100644 --- a/.cursor/rules/debug-chart-images.mdc +++ b/.cursor/rules/debug-chart-images.mdc @@ -1,6 +1,6 @@ --- -description: -globs: +description: debugging, plotting +globs: alwaysApply: false --- # Debugging Charts with Image Snapshots diff --git a/.cursor/rules/verso-docstrings.mdc b/.cursor/rules/verso-docstrings.mdc index 69a3704..4c3cbc5 100644 --- a/.cursor/rules/verso-docstrings.mdc +++ b/.cursor/rules/verso-docstrings.mdc @@ -1,6 +1,6 @@ --- -description: -globs: +description: +globs: alwaysApply: false --- # Verso Docstring & Manual Generation Guide diff --git a/LeanPlot.lean b/LeanPlot.lean index 129cfbe..3393492 100644 --- a/LeanPlot.lean +++ b/LeanPlot.lean @@ -8,3 +8,5 @@ import LeanPlot.Demos.LinearDemo import LeanPlot.Demos.QuadraticDemo import LeanPlot.Demos.OverlayDemo import LeanPlot.Palette + + diff --git a/LeanPlot/Axis.lean b/LeanPlot/Axis.lean index 6a2db74..bedf181 100644 --- a/LeanPlot/Axis.lean +++ b/LeanPlot/Axis.lean @@ -16,8 +16,14 @@ open Lean ProofWidgets ProofWidgets.Recharts /-- Extended props for an axis. The fields match `ProofWidgets.Recharts.AxisProps` with an extra `label?` string. -/ structure AxisProps where + /-- Which field of the JSON row contains the coordinate for this axis. When + `none`, Recharts will attempt to infer it. -/ dataKey? : Option Json := none + /-- Optional explicit `[lo, hi]` domain for the axis. When `none`, Recharts + determines the range automatically based on the data. -/ domain? : Option (Array Json) := none + /-- When `true`, points are allowed to overflow the axis domain instead of + being clipped. Defaults to `false` like Recharts. -/ allowDataOverflow : Bool := false /-- How values along this axis should be interpreted. The Recharts default is `category`. -/ diff --git a/LeanPlot/Basic.lean b/LeanPlot/Basic.lean index 99415d9..94644fd 100644 --- a/LeanPlot/Basic.lean +++ b/LeanPlot/Basic.lean @@ -1 +1,2 @@ +/-- Dummy constant used by `Main.main` to verify the project builds. -/ def hello := "world" diff --git a/LeanPlot/Components.lean b/LeanPlot/Components.lean index cc522ee..bc7d905 100644 --- a/LeanPlot/Components.lean +++ b/LeanPlot/Components.lean @@ -3,6 +3,7 @@ import ProofWidgets.Component.Recharts import LeanPlot.ToFloat import LeanPlot.Axis import LeanPlot.Legend +import LeanPlot.Palette /-! # LeanPlot core components @@ -88,15 +89,14 @@ plots. )} -/-- -Minimal props for a Recharts `` component. We only expose -`width`, `height` and the `data` array because these are the fields -required by our Tier-0 helper. Additional props can be surfaced later -without breaking existing call-sites. --/ +/-- Props for a Recharts `` wrapped in Lean. We intentionally +keep this minimal, exposing only what the Tier-0 helpers require. -/ structure ScatterChartProps where + /-- Width of the SVG container in pixels. -/ width : Nat + /-- Height of the SVG container in pixels. -/ height : Nat + /-- Array of JSON rows each containing at least `x` and `y` fields. -/ data : Array Json deriving FromJson, ToJson @@ -107,11 +107,12 @@ components that ship with ProofWidgets. -/ javascript := ProofWidgets.Recharts.Recharts.javascript «export» := "ScatterChart" -/-- Minimal props for a Recharts `` (single series of points). -At present we only need `dataKey` (which field of the JSON row contains -the y-value) and a `fill` colour for the points. -/ +/-- Props for a Recharts `` series. -/ structure ScatterProps where + /-- Which field of the JSON row encodes the y-value to plot. Defaults to + `"y"`. -/ dataKey : Json := Json.str "y" + /-- CSS colour for the scatter points. -/ fill : String deriving FromJson, ToJson diff --git a/LeanPlot/Demos/LinearDemo.lean b/LeanPlot/Demos/LinearDemo.lean index 436a63f..b3cd528 100644 --- a/LeanPlot/Demos/LinearDemo.lean +++ b/LeanPlot/Demos/LinearDemo.lean @@ -1,13 +1,12 @@ -import LeanPlot.Components -import LeanPlot.Plot -import LeanPlot.Palette -open Lean ProofWidgets Recharts LeanPlot.Components LeanPlot.Palette -open scoped ProofWidgets.Jsx +import LeanPlot.Plot +import LeanPlot.API namespace LeanPlot.Demos -/- Plot `y = x` on the interval `[0,1]`. Put your cursor on the `#html` line to render. -/ -#plot mkLineChart (sample (fun x => x) 200 0 1) (autoColours #["y"]) 400 400 +open LeanPlot.API + +/-! Plot `y = x` on the interval `[0,1]`. Put your cursor on the `#plot` line to render. -/ +#plot (lineChart (fun x => x)) end LeanPlot.Demos diff --git a/LeanPlot/Demos/OverlayDemo.lean b/LeanPlot/Demos/OverlayDemo.lean index 9847d2d..4043f01 100644 --- a/LeanPlot/Demos/OverlayDemo.lean +++ b/LeanPlot/Demos/OverlayDemo.lean @@ -7,12 +7,25 @@ open scoped ProofWidgets.Jsx namespace LeanPlot.Demos -/- Overlay of `y = x` and `y = x²` with built-in legend. Put the cursor on the `#plot` line below to render. -/ +/-- Overlay of `y = x` and `y = x²` with a built-in legend. Use +`#plot overlayLegend` in the infoview to render the chart. -/ def overlayLegend : Html := let names := #["y", "y²"] - let data := sampleMany01 #[("y", fun x => x), ("y²", fun x => x * x)] 200 + let data := sampleMany #[("y", fun x => x), ("y²", fun x => x * x)] mkLineChartFull data (autoColours names) none none 400 400 #plot overlayLegend + +/-- Archimedes' constant with sufficient precision for the purposes of these +demos. We redeclare it here rather than depend on Mathlib. -/ +def Float.pi : Float := 3.14159265358979323846 + +/-- Plot of the sine function on the interval `[-2π, 2π]`. -/ +def sinChart : Html := + let data := sampleMany #[("sin", fun x => Float.sin x)] (min := -2 * Float.pi) (max := 2 * Float.pi) + mkLineChartFull data (autoColours #["sin"]) + +#plot sinChart + end LeanPlot.Demos diff --git a/LeanPlot/Demos/QuadraticDemo.lean b/LeanPlot/Demos/QuadraticDemo.lean index 7d46e70..a244543 100644 --- a/LeanPlot/Demos/QuadraticDemo.lean +++ b/LeanPlot/Demos/QuadraticDemo.lean @@ -1,13 +1,12 @@ -import LeanPlot.Components +import LeanPlot.API import LeanPlot.Plot -import LeanPlot.Palette -open Lean ProofWidgets Recharts LeanPlot.Components LeanPlot.Palette -open scoped ProofWidgets.Jsx +open Lean ProofWidgets LeanPlot.API + namespace LeanPlot.Demos /- Plot `y = x²` on the interval `[0,1]`. Put your cursor on the `#plot` line to render. -/ -#plot mkLineChart (sample (fun x => x * x) 200) (autoColours #["y²"]) 400 400 +#plot (LeanPlot.API.lineChart (fun x => x * x)) end LeanPlot.Demos diff --git a/LeanPlot/Palette.lean b/LeanPlot/Palette.lean index d9cce5c..8bc65b8 100644 --- a/LeanPlot/Palette.lean +++ b/LeanPlot/Palette.lean @@ -15,19 +15,35 @@ open Lean private abbrev Color := String +/-- Dark purple (`#440154`). -/ def darkPurple : Color := "#440154" + +/-- Indigo (`#482878`). -/ def indigo : Color := "#482878" + +/-- Blue-purple (`#3e4a89`). -/ def bluePurple : Color := "#3e4a89" + +/-- Medium blue (`#31688e`). -/ def blue : Color := "#31688e" + +/-- Turquoise (#26828e). -/ def turquoise : Color := "#26828e" + +/-- Green-turquoise (#1f9e89). -/ def greenTurquoise : Color := "#1f9e89" + +/-- Green (`#35b779`). -/ def green : Color := "#35b779" -def lime : Color := "#6ece58" -def yellowGreen : Color := "#b5de2b" -def yellow : Color := "#fde725" +/-- Lime (`#6ece58`). -/ +def lime : Color := "#6ece58" +/-- Yellow-green (`#b5de2b`). -/ +def yellowGreen : Color := "#b5de2b" +/-- Yellow (`#fde725`). -/ +def yellow : Color := "#fde725" /-- A qualitative 10-colour palette that looks good on both dark and light backgrounds and is colour-blind-friendly. Source: Matplotlib _tab10_. -/ @@ -54,7 +70,7 @@ lists (with the caveat that colours will start repeating). -/ `defaultPalette` (cycling when necessary). The result is suitable for the `seriesStrokes` argument expected by `LeanPlot.Components.mkLineChart` and friends. -/ +-- TODO this should be any collection, not just an array @[inline] def autoColours (names : Array String) : Array (String × String) := names.zipIdx.map (fun (n, i) => (n, colourFor i)) - end LeanPlot.Palette diff --git a/LeanPlot/Plot.lean b/LeanPlot/Plot.lean index 67ddff7..a316a72 100644 --- a/LeanPlot/Plot.lean +++ b/LeanPlot/Plot.lean @@ -21,6 +21,8 @@ can be displayed with `#plot t`. This mirrors the behaviour of `#html`. -/ syntax (name := plotCmd) "#plot " term : command open Elab Command ProofWidgets.HtmlCommand in +/-- The `#plot` command is an alias for `#html`. It is namespaced under +`LeanPlot` to improve discoverability. -/ @[command_elab plotCmd] def elabPlotCmd : CommandElab := fun | stx@`(#plot $t:term) => do diff --git a/TODO.md b/TODO.md index ecdfac9..a99641a 100644 --- a/TODO.md +++ b/TODO.md @@ -25,6 +25,7 @@ - [ ] Auto colour palette - [x] `#plot` command alias for `#html` (LeanPlot.PlotCommand) - [ ] Auto domain inference +- [ ] Auto axis labels from binder names (metaprogramming extraction of plotting function parameters) ### More chart types - [ ] Log / linear scale toggle diff --git a/lake-manifest.json b/lake-manifest.json index 71b6d41..bbfcba7 100644 --- a/lake-manifest.json +++ b/lake-manifest.json @@ -1,7 +1,17 @@ {"version": "1.1.0", "packagesDir": ".lake/packages", "packages": - [{"url": "https://github.com/leanprover-community/ProofWidgets4.git", + [{"url": "https://github.com/leanprover/verso.git", + "type": "git", + "subDir": null, + "scope": "", + "rev": "56516773c37ff1b06670751c06c3056cbc627df6", + "name": "verso", + "manifestFile": "lake-manifest.json", + "inputRev": null, + "inherited": false, + "configFile": "lakefile.lean"}, + {"url": "https://github.com/leanprover-community/ProofWidgets4.git", "type": "git", "subDir": null, "scope": "", @@ -11,6 +21,26 @@ "inputRev": "v0.0.57", "inherited": false, "configFile": "lakefile.lean"}, + {"url": "https://github.com/acmepjz/md4lean", + "type": "git", + "subDir": null, + "scope": "", + "rev": "8ba0ef10d178ab95a5d6fe3cfbd586c6ecef2717", + "name": "MD4Lean", + "manifestFile": "lake-manifest.json", + "inputRev": "main", + "inherited": true, + "configFile": "lakefile.lean"}, + {"url": "https://github.com/leanprover/subverso.git", + "type": "git", + "subDir": null, + "scope": "", + "rev": "a3e5c4c50791e536fc7f13a7aadd6236091796f9", + "name": "subverso", + "manifestFile": "lake-manifest.json", + "inputRev": "main", + "inherited": true, + "configFile": "lakefile.lean"}, {"url": "https://github.com/leanprover-community/batteries", "type": "git", "subDir": null, diff --git a/lakefile.toml b/lakefile.toml index ec51d56..30fe6bf 100644 --- a/lakefile.toml +++ b/lakefile.toml @@ -22,7 +22,4 @@ rev = "v0.0.57" [[require]] name = "verso" -# We pin to latest main commit for now; consider using a tagged release later -# when Verso publishes stable versions. git = "https://github.com/leanprover/verso.git" -rev = "main" diff --git a/lean-toolchain b/lean-toolchain index 7aca1d8..cfb5ca9 100644 --- a/lean-toolchain +++ b/lean-toolchain @@ -1 +1 @@ -leanprover/lean4:v4.19.0 +leanprover/lean4:v4.20.0-rc2 \ No newline at end of file From 70c939ffe1e10beeda2fe205ada513be2c0e79b4 Mon Sep 17 00:00:00 2001 From: Alok Singh Date: Tue, 6 May 2025 00:41:04 -0400 Subject: [PATCH 31/38] docs(llms): log next-steps plan for Verso manual build --- llms.txt | 11 ++++++++++- 1 file changed, 10 insertions(+), 1 deletion(-) diff --git a/llms.txt b/llms.txt index 0626fbf..2c30364 100644 --- a/llms.txt +++ b/llms.txt @@ -162,4 +162,13 @@ Next tasks (documentation) [ ] Scaffold `docs/` directory with minimal `%doc` page. [ ] Add `DocsMain.lean` executable using `manualMain`. [ ] Update CI to build docs and publish to `_docs`. -[ ] Integrate `{docstring LeanPlot.*}` links throughout prose. \ No newline at end of file +[ ] Integrate `{docstring LeanPlot.*}` links throughout prose. + +2025-05-06:04:40 UTC – Verso documentation next steps +------------------------------------------------------ +1. Bootstrap Verso manual (`docs/DocsMain.lean`, `lake exe docs` + Justfile) +2. Auto-extract demo snippets into manual via `{docstring LeanPlot.Demos.*}` +3. Enable strict docstring lint pass in docs build +4. Expand README & manual with quick-start + VS Code infoview GIF +5. Changelog bump to 0.2.2 and record docs pipeline +6. Optional dev UX polish (docs-preview target, pre-commit diff check) \ No newline at end of file From e97ce1b11972b2dc787f8ce193c53cfdbb64d182 Mon Sep 17 00:00:00 2001 From: Alok Singh Date: Tue, 6 May 2025 03:05:54 -0400 Subject: [PATCH 32/38] docs: postpone Verso manual tasks, update llms work log and stage WIP files Move Verso documentation integration to backlog and focus back on plotting ergonomics. Added work log entry. Stage WIP docs stub and experimental modules so branch compiles but deprioritised. --- DocsMain.lean | 19 +++++++++++++++++++ LeanPlot/DSL.lean | 30 ++++++++++++++++++++++++++++++ LeanPlot/Experiments.lean | 32 ++++++++++++++++++++++++++++++++ lakefile.toml | 1 - llms.txt | 8 +++++++- 5 files changed, 88 insertions(+), 2 deletions(-) create mode 100644 DocsMain.lean create mode 100644 LeanPlot/DSL.lean create mode 100644 LeanPlot/Experiments.lean diff --git a/DocsMain.lean b/DocsMain.lean new file mode 100644 index 0000000..f6ec6ca --- /dev/null +++ b/DocsMain.lean @@ -0,0 +1,19 @@ +import VersoManual +import LeanPlotManual + +open Verso.Genre Manual + +/-- Configuration for the LeanPlot manual generation. -/ +def docsConfig : Config := { + emitTex := false, + emitHtmlSingle := false, + emitHtmlMulti := true, + htmlDepth := 2, + sourceLink := some "https://github.com/alok/LeanPlot", + issueLink := some "https://github.com/alok/LeanPlot/issues" +} + +/-- Entry point for `lake exe docs`. Generates the multi-page HTML manual into +`docs/html-multi` (overridable via `--output` CLI flag). -/ +def main : IO UInt32 := + manualMain (%doc LeanPlotManual) (config := docsConfig) diff --git a/LeanPlot/DSL.lean b/LeanPlot/DSL.lean new file mode 100644 index 0000000..0565c83 --- /dev/null +++ b/LeanPlot/DSL.lean @@ -0,0 +1,30 @@ +import LeanPlot.API +import ProofWidgets.Component.HtmlDisplay + +/-! # LeanPlot.DSL – tiny surface syntax + +This module introduces a convenience `#plot` command that expands to a call to +`LeanPlot.API.lineChart` and renders the result immediately via `#html`. + +Usage examples: +``` +#plot (fun x => x) -- default 200 samples on [0,1] +#plot (fun x => x*x) using 50 -- 50 samples +``` + +This is intentionally *very* small – just enough to demonstrate how +metaprogramming can raise the ergonomics bar. Future iterations will evolve +into a richer grammar of graphics. +-/ + +open Lean +open scoped ProofWidgets.Jsx + +/-- Syntax: `#plot f` or `#plot f using 123` -/ +syntax "#plot" term ("using" num)? : command + +macro_rules + | `(#plot $f:term) => + `(#html LeanPlot.API.lineChart $f) + | `(#plot $f:term using $n:num) => + `(#html LeanPlot.API.lineChart $f (steps := $n)) diff --git a/LeanPlot/Experiments.lean b/LeanPlot/Experiments.lean new file mode 100644 index 0000000..767e2a6 --- /dev/null +++ b/LeanPlot/Experiments.lean @@ -0,0 +1,32 @@ +import LeanPlot.API +open LeanPlot.API +open LeanPlot.Constants +open scoped ProofWidgets.Jsx + +/-! +# LeanPlot – Tier-0 Ergonomics *scratchpad* + +Live notebook for ad-hoc experiments while developing LeanPlot. **Not** part +of the released API – feel free to wipe or rewrite at will. +-/ + +/- ## Quick experiments ----------------------------------------------------- -/ + +#html lineChart (fun x ↦ x) -- cute way of writing `fun x ↦ x` + +#html lineChart (fun x ↦ x * x) (steps := 50) + +#html scatterChart #[(0.1,0.4), (0.2,0.25), (0.4,0.16), (0.6,0.36), (0.8,0.64), (1.0,1.0)] + +/-! +## Historic roadmap (kept for context) + +1. `LeanPlot.Constants` – centralise defaults. +2. `autoDomain` helper. +3. `sample`/`sampleMany` accept `Option` bounds. +4. Tier-0 wrappers `lineChart`/`scatterChart`. +5. Palette convenience. +6. Demo & doc refresh. +7. Feedback banner. +8. Clean-up & deprecations. +-/ diff --git a/lakefile.toml b/lakefile.toml index 30fe6bf..73c6f09 100644 --- a/lakefile.toml +++ b/lakefile.toml @@ -4,7 +4,6 @@ defaultTargets = ["leanplot"] [leanOptions] pp.unicode.fun = true -relaxedAutoImplicit = false linter.missingDocs = true diff --git a/llms.txt b/llms.txt index 2c30364..ea1a391 100644 --- a/llms.txt +++ b/llms.txt @@ -171,4 +171,10 @@ Next tasks (documentation) 3. Enable strict docstring lint pass in docs build 4. Expand README & manual with quick-start + VS Code infoview GIF 5. Changelog bump to 0.2.2 and record docs pipeline -6. Optional dev UX polish (docs-preview target, pre-commit diff check) \ No newline at end of file +6. Optional dev UX polish (docs-preview target, pre-commit diff check) + +2025-05-06:07:05 UTC – Verso manual postponed +------------------------------------------------------ +• Decision: Verso documentation pipeline tasks moved to backlog; focus returns to plotting ergonomics. +• Committing current WIP (DocsMain stub, DSL experiment) on branch `ergonomics/tier0-chart`. +• Next up: linter clean-up and core auto-domain plumbing. \ No newline at end of file From 0479adba40f94c688bee5e9454ad3de100377c02 Mon Sep 17 00:00:00 2001 From: Alok Singh Date: Tue, 6 May 2025 17:51:04 -0400 Subject: [PATCH 33/38] feat(api): autoDomain integration with explicit y-axis domain in lineChart Tier-0 helper\n\nUse autoDomain to calculate (lo, hi) and pass domain prop to YAxis for better scaling. Update let sequencing semicolons. --- Justfile | 3 ++- LeanPlot/API.lean | 8 ++++---- 2 files changed, 6 insertions(+), 5 deletions(-) diff --git a/Justfile b/Justfile index 85f85ed..24ca03a 100644 --- a/Justfile +++ b/Justfile @@ -18,7 +18,8 @@ watch: # Lint (placeholder – adjust when linter chosen) lint: - lake env lean --run Std.Tactic.Lint + # Use Batteries linter which our project depends on + lake env lean --run Batteries.Tactic.Lint # Clean build artefacts clean: diff --git a/LeanPlot/API.lean b/LeanPlot/API.lean index 252995b..8cdf092 100644 --- a/LeanPlot/API.lean +++ b/LeanPlot/API.lean @@ -59,13 +59,13 @@ Returns a `ProofWidgets.Html` value that can be rendered with `#plot`. Example: (w : Nat := defaultW) (h : Nat := defaultH) : ProofWidgets.Html := let data := LeanPlot.Components.sample f steps 0 1 -- Infer a reasonable y-axis domain automatically. - let (_lo, _hi) := LeanPlot.AutoDomain.autoDomain f steps + let (lo, hi) := LeanPlot.AutoDomain.autoDomain f steps; + let yDomain : Array Json := #[toJson lo, toJson hi]; -- Assign a colour for the single series "y" using the default palette. - let seriesStrokes := LeanPlot.Palette.autoColours #["y"]; -- TODO fixup grammar so ; cancer excised (perlis) - -- Build the chart manually so we can pass the `domain?` prop. + let seriesStrokes := LeanPlot.Palette.autoColours #["y"]; - + {... seriesStrokes.map (fun (name, colour) => )} From f76ec004abcca66614d53b8ff6f4479e2d333930 Mon Sep 17 00:00:00 2001 From: Alok Singh Date: Tue, 6 May 2025 18:13:47 -0400 Subject: [PATCH 34/38] chore(just): wire lint task to Batteries runLinter script with pre-build step --- Justfile | 6 ++++-- 1 file changed, 4 insertions(+), 2 deletions(-) diff --git a/Justfile b/Justfile index 24ca03a..3ca1830 100644 --- a/Justfile +++ b/Justfile @@ -18,8 +18,10 @@ watch: # Lint (placeholder – adjust when linter chosen) lint: - # Use Batteries linter which our project depends on - lake env lean --run Batteries.Tactic.Lint + # Ensure Batteries linter modules are freshly built with current Lean version + lake build +Batteries.Tactic.Lint + # Run Batteries linter script that checks our project modules + lake env lean --run .lake/packages/batteries/scripts/runLinter.lean # Clean build artefacts clean: From 574a8bc591a239190b7de85eb74151715c04167c Mon Sep 17 00:00:00 2001 From: Alok Singh Date: Wed, 7 May 2025 15:34:34 -0400 Subject: [PATCH 35/38] refactor: Temporarily remove legend in PlotSpec, update todos --- LeanPlot/Specification.lean | 236 ++++++++++++++++++++++++++++++++++++ llms.txt | 25 ++-- 2 files changed, 252 insertions(+), 9 deletions(-) create mode 100644 LeanPlot/Specification.lean diff --git a/LeanPlot/Specification.lean b/LeanPlot/Specification.lean new file mode 100644 index 0000000..cafe56d --- /dev/null +++ b/LeanPlot/Specification.lean @@ -0,0 +1,236 @@ +import LeanPlot.Constants +import LeanPlot.Components +import LeanPlot.Palette +import LeanPlot.ToFloat +import LeanPlot.Axis -- For AxisProps used in Recharts +import LeanPlot.API -- For xyArrayToJson +import LeanPlot.Utils -- For jsonDataHasInvalidFloats +import LeanPlot.WarningBanner -- For WarningBanner +import LeanPlot.Core -- For LeanPlot.Render instance +import ProofWidgets.Component.Recharts +import ProofWidgets.Data.Html -- Explicit import for Html.empty and Html.text +import Lean.Server -- For HtmlEval +-- import ProofWidgets.Data.Legend + +open Lean ProofWidgets ProofWidgets.Recharts LeanPlot.Constants +open LeanPlot -- For WarningBannerProps, WarningBanner, Render +open LeanPlot.Utils -- For jsonDataHasInvalidFloats +open scoped ProofWidgets.Jsx -- This enables JSX syntax +namespace LeanPlot + +structure AxisSpec where + label : Option String := none + dataKey : String := "x" -- Default for x-axis, override for y-axis + -- domain : Option (Json × Json) := none -- Recharts takes Array Json for domain + domain : Option (Array Json) := none + -- Potentially more options like 'type' (category, number), ticks, etc. + deriving Inhabited, ToJson, FromJson + +structure SeriesSpec where + /-- The name of the series, used for legend and default y-axis label. -/ + name : String + /-- The key in chartData for this series' y-values. -/ + dataKey : String := name + /-- The color of the series. -/ + color : String + /-- The type of the series, e.g., "line", "scatter". -/ + type : String -- e.g., "line", "scatter" + /-- Whether to show dots for a line series. `none` means default (true for line, not applicable for scatter). -/ + dot : Option Bool := none + deriving Inhabited, ToJson, FromJson + +/-- The specification for a plot. -/ +structure PlotSpec where + /-- The data for the chart. -/ + chartData : Array Json := #[] + /-- The series in the chart. -/ + series : Array SeriesSpec := #[] + /-- Default x-axis specification. -/ + xAxis : Option AxisSpec := some { dataKey := "x" } + /-- Default y-axis specification. -/ + yAxis : Option AxisSpec := some { dataKey := "y" } + /-- The title of the plot. -/ + title : Option String := none + /-- The width of the plot. -/ + width : Nat := defaultW + /-- The height of the plot. -/ + height : Nat := defaultH + /-- Whether to show the legend. -/ + legend : Bool := true + deriving Inhabited + +-- Basic constructor functions + +/-- Construct a line plot from a function. -/ +@[inline] +def line {β} [ToFloat β] + (fn : Float → β) (name : String := "y") (steps : Nat := 200) + (domainOpt : Option (Float × Float) := none) + (color : Option String := none) : PlotSpec := + let data := LeanPlot.Components.sample fn steps (domainOpt := domainOpt) + let seriesColor := color.getD (LeanPlot.Palette.colourFor 0) + { + chartData := data, + series := #[{ + name := name, + dataKey := "y", -- `sample` produces {x:_, y:_} items + color := seriesColor, + type := "line" + -- dot defaults to none -> true for line + }], + xAxis := some { dataKey := "x", label := some "x" }, -- Default x-axis label + yAxis := some { dataKey := "y", label := some name }, + legend := !(name == "y") -- Hide legend if name is default "y" for single series plot + } + +/-- Construct a scatter plot from an array of points. -/ +@[inline] +def scatter (points : Array (Float × Float)) (name : String := "y") + (color : Option String := none) : PlotSpec := + let data := LeanPlot.API.xyArrayToJson points + let seriesColor := color.getD (LeanPlot.Palette.colourFor 0) + { + chartData := data, + series := #[{ + name := name, + dataKey := "y", -- `xyArrayToJson` produces {x:_, y:_} + color := seriesColor, + type := "scatter" + -- dot is not applicable for scatter + }], + xAxis := some { dataKey := "x", label := some "x" }, -- Default x-axis label + yAxis := some { dataKey := "y", label := some name }, + legend := !(name == "y") + } + +-- Combinators + +namespace PlotSpec + +/-- Set the title of the plot. -/ +@[inline] +def withTitle (spec : PlotSpec) (t : String) : PlotSpec := + { spec with title := some t } + +/-- Set the width of the plot. -/ +@[inline] +def withWidth (spec : PlotSpec) (w : Nat) : PlotSpec := + { spec with width := w } + +/-- Set the height of the plot. -/ +@[inline] +def withHeight (spec : PlotSpec) (h : Nat) : PlotSpec := + { spec with height := h } + +/-- Set the width and height of the plot. -/ +@[inline] +def withSize (spec : PlotSpec) (w h : Nat) : PlotSpec := + { spec with width := w, height := h } + +/-- Set the x-axis label of the plot. -/ +@[inline] +def withXLabel (spec : PlotSpec) (label : String) : PlotSpec := + match spec.xAxis with + | some xAxisSpec => { spec with xAxis := some { xAxisSpec with label := some label } } + | none => { spec with xAxis := some { label := some label, dataKey := "x" } } + +/-- Set the y-axis label of the plot. -/ +@[inline] +def withYLabel (spec : PlotSpec) (label : String) : PlotSpec := + match spec.yAxis with + | some yAxisSpec => { spec with yAxis := some { yAxisSpec with label := some label } } + | none => { spec with yAxis := some { label := some label, dataKey := "y" } } + -- Note: dataKey for yAxis might need to be smarter if multiple series exist + +/-- Show or hide the legend. -/ +@[inline] +def withLegend (spec : PlotSpec) (shouldShow : Bool) : PlotSpec := + { spec with legend := shouldShow } + +/-- Set the x-axis domain. -/ +@[inline] +def withXDomain (spec : PlotSpec) (min max : Float) : PlotSpec := + let newDomain := #[toJson min, toJson max] + match spec.xAxis with + | some xAxisSpec => { spec with xAxis := some { xAxisSpec with domain := some newDomain } } + | none => { spec with xAxis := some { dataKey := "x", domain := some newDomain } } + +/-- Set the y-axis domain. -/ +@[inline] +def withYDomain (spec : PlotSpec) (min max : Float) : PlotSpec := + let newDomain := #[toJson min, toJson max] + match spec.yAxis with + | some yAxisSpec => { spec with yAxis := some { yAxisSpec with domain := some newDomain } } + | none => { spec with yAxis := some { dataKey := "y", domain := some newDomain } } + +-- TODO: Add more combinators: addSeries, etc. + +-- Renderer +-- This is a complex part, converting the spec to Recharts JSX +-- For now, we can adapt the existing mkLineChartFull or similar logic + +/-- Render the plot. -/ +@[inline] +def render (spec : PlotSpec) : Html := + let chartComponents := spec.series.map fun s => + if s.type == "line" then + let dotProp := s.dot.getD true -- Default to true if `none` + ( : Html) + else if s.type == "scatter" then + let scatterProps : LeanPlot.Components.ScatterProps := { dataKey := toJson s.dataKey, fill := s.color } + ( : Html) + else + (Html.text s!"Unsupported series type: {s.type}" : Html) + + let xAxisHtml := match spec.xAxis with + | some ax => + let axProps : LeanPlot.Axis.AxisProps := { dataKey? := toJson ax.dataKey, label? := ax.label, domain? := ax.domain, type := .number } + ( : Html) + | none => (Html.text "" : Html) + + let yAxisHtml := match spec.yAxis with + | some ax => + let axProps : LeanPlot.Axis.AxisProps := { dataKey? := toJson ax.dataKey, label? := ax.label, domain? := ax.domain, type := .number } + ( : Html) + | none => (Html.text "" : Html) + + let legendHtml := if spec.legend then (Html.text "" : Html) else (Html.text "" : Html) -- Temporarily removed Legend + -- Temporarily remove legend until a Legend component is available/created + -- let legendHtml := (Html.text "" : Html) + + let mainChartComponent := + -- Always use LineChart as the main container, it can host Scatter series too. + ( + {xAxisHtml} + {yAxisHtml} + {legendHtml} + {Html.element "Fragment" #[] chartComponents} + : Html) + + let finalHtml := match spec.title with + | some t => + (

{Html.text t}

{mainChartComponent}
: Html) + | none => mainChartComponent + + let keysToCheck := spec.series.map (fun s => s.dataKey) |>.push "x" + if jsonDataHasInvalidFloats spec.chartData keysToCheck then + let warningProps : WarningBannerProps := { message := "Plot data contains invalid values (NaN/Infinity) and may not render correctly." } + let warningHtml := WarningBanner warningProps + (.element "div" #[] #[warningHtml, finalHtml] : Html) + else + finalHtml + +/-- Render the plot. -/ +instance : Render PlotSpec where -- Render is from LeanPlot.Core, brought in by 'open LeanPlot' + render := render + +/-- Allow PlotSpec to be evaluated by #plot command. -/ +instance : HtmlEval PlotSpec where + eval spec := do + -- Since render is pure, we just return it directly. + -- If render needed IO/Rpc actions, they would happen here. + return render spec + +end PlotSpec + +end LeanPlot diff --git a/llms.txt b/llms.txt index ea1a391..42a1591 100644 --- a/llms.txt +++ b/llms.txt @@ -90,10 +90,10 @@ Updated nested checkbox view - [x] Tier-0 chart wrappers - [x] `lineChart` wrapper (defaults N, domain, colours, size) - [x] `scatterChart` wrapper (defaults size, colours) -- [ ] Core plumbing - - [ ] Extend `sample` to accept optional domain - - [ ] Implement `autoDomain` helper - - [ ] Wire wrappers to `mkLineChart` *(awaiting autoDomain integration)* +- [x] Core plumbing + - [x] Extend `sample` to accept optional domain + - [x] Implement `autoDomain` helper + - [x] Wire wrappers to `mkLineChart` (Done for `lineChart` via `sample`) - [x] Constants & palette - [x] `LeanPlot.Constants` with `defaultW`, `defaultH` - [x] Expose `Palette.defaultPalette.head!` via `autoColours` @@ -102,8 +102,8 @@ Updated nested checkbox view - [x] `LeanPlot.Demos.CubicDemo` (Tier-0 usage) - [ ] Tick "Cubic" in `Gallery.md` - [ ] Quality gates - - [ ] `lake build` passes (TODO verify) - - [ ] Linter clean + - [x] `lake build` passes + - [ ] Linter clean (Blocked by upstream `batteries` issue: unknown id `initSrcSearchPath`) - [ ] Optional compile-time JSON check 2025-05-03:10:15 UTC – Documentation updates @@ -119,11 +119,11 @@ Updated nested checkbox view - [x] Tick "Cubic" in `Gallery.md` - [ ] Quality gates - [x] `lake build` passes - - [ ] Linter clean + - [ ] Linter clean (Blocked by upstream `batteries` issue: unknown id `initSrcSearchPath`) - [ ] Optional compile-time JSON check Next tasks: -1. Linter clean-up – run `just linter` and fix warnings. +1. Linter clean-up – run `just linter` and fix warnings. (Currently blocked by upstream `batteries` issue) 2. Explore compile-time JSON key check. 3. Warn banner component for NaN/Inf. @@ -177,4 +177,11 @@ Next tasks (documentation) ------------------------------------------------------ • Decision: Verso documentation pipeline tasks moved to backlog; focus returns to plotting ergonomics. • Committing current WIP (DocsMain stub, DSL experiment) on branch `ergonomics/tier0-chart`. -• Next up: linter clean-up and core auto-domain plumbing. \ No newline at end of file +• Next up: linter clean-up (blocked) and core auto-domain plumbing (now complete for `sample`/`lineChart`). + +NEW_LOG_ENTRY_BELOW +2025-05-06:10:00 UTC – PlotSpec Refinements & Rendering Typeclass +--------------------------------------------------------------------- +- [ ] Investigate and add Recharts Legend component (currently causes "unknown identifier"). +- [ ] Implement typeclass-based rendering for `SeriesSpec`. +- [ ] Define `PlotSpec.stack` or `PlotSpec.addSeries` for multi-series plots. \ No newline at end of file From 404c2d97d8923652b44804f436707dff6983d2ee Mon Sep 17 00:00:00 2001 From: Alok Singh Date: Thu, 8 May 2025 01:05:13 -0400 Subject: [PATCH 36/38] feat(spec): surface axis labels and add PlotSpec.addSeries combinator (#29) --- CHANGELOG.md | 36 ++++++++++++++++++++++++++- LeanPlot/Specification.lean | 49 +++++++++++++++++++++++++------------ 2 files changed, 68 insertions(+), 17 deletions(-) diff --git a/CHANGELOG.md b/CHANGELOG.md index 8eb3d26..c715ba6 100644 --- a/CHANGELOG.md +++ b/CHANGELOG.md @@ -82,4 +82,38 @@ - Introduced `LeanPlot.Core` with the general `Render`, `Layer`, `Plot` abstractions. - Added low-priority generic `HAdd` instance that overlays any `[ToPlot]` values via `Plot.overlay`. - Migrated `LeanPlot.Algebra` to these abstractions, deleting duplicated `Render`/`CoeTC` and bespoke `HAdd`. -- `LinePlot` now only provides a `[ToLayer]` instance and inherits `+` overlay behaviour from the core instance. \ No newline at end of file +- `LinePlot` now only provides a `[ToLayer]` instance and inherits `+` overlay behaviour from the core instance. + +## [0.2.2] – 2025-05-07:19:00 + +### Added + +- **Warning Banner for Invalid Plot Data**: Charts now display a warning banner if the input data contains `NaN` or `Infinity` values. This helps users identify problematic data that might lead to incorrect or empty plots. + - New `LeanPlot.WarningBanner` component for displaying HTML-based warnings. + - New utility functions in `LeanPlot.Utils` (`isInvalidFloat`, `jsonDataHasInvalidFloats`) to detect invalid floating-point numbers in JSON data. + - Chart generation functions in `LeanPlot.Components` (e.g., `mkLineChart`, `mkScatterChart`) now integrate these checks. +- New demo `LeanPlot.Demos.InvalidDataDemo.lean` to showcase the warning banner with functions producing `NaN`/`Infinity`. + +### Changed + +- N/A + +### Fixed + +- Corrected block comment syntax in `LeanPlot/Utils.lean` to resolve parsing errors. +- Adjusted `open` statements in `LeanPlot/Components.lean` to correctly access `jsonDataHasInvalidFloats` from `LeanPlot.Utils`. + +## [0.2.3] – 2025-05-08:01:04 + +### Added + +- Support for axis labels in high‐level `PlotSpec` renderer: `AxisSpec.label` is now passed through to Recharts. +- New `PlotSpec.addSeries` combinator to append additional series to an existing plot. + +### Changed + +- Corrected construction of `AxisProps` in `PlotSpec.render` so that `dataKey?` is wrapped in `some …` as required by the `Option` type. + +### Fixed + +- N/A \ No newline at end of file diff --git a/LeanPlot/Specification.lean b/LeanPlot/Specification.lean index cafe56d..20303bb 100644 --- a/LeanPlot/Specification.lean +++ b/LeanPlot/Specification.lean @@ -7,6 +7,7 @@ import LeanPlot.API -- For xyArrayToJson import LeanPlot.Utils -- For jsonDataHasInvalidFloats import LeanPlot.WarningBanner -- For WarningBanner import LeanPlot.Core -- For LeanPlot.Render instance +import LeanPlot.Legend -- Add import for Legend import ProofWidgets.Component.Recharts import ProofWidgets.Data.Html -- Explicit import for Html.empty and Html.text import Lean.Server -- For HtmlEval @@ -15,6 +16,7 @@ import Lean.Server -- For HtmlEval open Lean ProofWidgets ProofWidgets.Recharts LeanPlot.Constants open LeanPlot -- For WarningBannerProps, WarningBanner, Render open LeanPlot.Utils -- For jsonDataHasInvalidFloats +open LeanPlot.Legend (Legend) -- Open Legend for direct use open scoped ProofWidgets.Jsx -- This enables JSX syntax namespace LeanPlot @@ -163,40 +165,55 @@ def withYDomain (spec : PlotSpec) (min max : Float) : PlotSpec := | some yAxisSpec => { spec with yAxis := some { yAxisSpec with domain := some newDomain } } | none => { spec with yAxis := some { dataKey := "y", domain := some newDomain } } --- TODO: Add more combinators: addSeries, etc. - --- Renderer --- This is a complex part, converting the spec to Recharts JSX --- For now, we can adapt the existing mkLineChartFull or similar logic - -/-- Render the plot. -/ +/-- Append a new series to the plot. The caller must ensure that `spec.chartData` already provides the data for `series.dataKey`. -/ @[inline] -def render (spec : PlotSpec) : Html := - let chartComponents := spec.series.map fun s => +def addSeries (spec : PlotSpec) (series : SeriesSpec) : PlotSpec := + { spec with series := spec.series.push series, legend := true } + +-- Renderer Typeclass +class RenderSeries (α : Type) where + /-- Renders a series specification into HTML. + `seriesSpec` is the specification for the individual series. + `allChartData` is the complete dataset for the chart, passed in case the renderer needs it. -/ + renderSeries (seriesSpec : α) (allChartData : Array Json) : Html + +-- Default instance for SeriesSpec using its `type` field. +-- This moves the old if/else logic into the typeclass instance. +instance : RenderSeries SeriesSpec where + renderSeries (s : SeriesSpec) (_allChartData : Array Json) : Html := -- _allChartData often unused here if s.type == "line" then let dotProp := s.dot.getD true -- Default to true if `none` - ( : Html) + ( : Html) else if s.type == "scatter" then let scatterProps : LeanPlot.Components.ScatterProps := { dataKey := toJson s.dataKey, fill := s.color } ( : Html) else (Html.text s!"Unsupported series type: {s.type}" : Html) + +-- Main Plot Renderer +-- This is a complex part, converting the spec to Recharts JSX +-- For now, we can adapt the existing mkLineChartFull or similar logic + +/-- Render the plot. -/ +@[inline] +def render (spec : PlotSpec) : Html := + let chartComponents := spec.series.map fun s => + RenderSeries.renderSeries s spec.chartData -- Use the typeclass instance + let xAxisHtml := match spec.xAxis with | some ax => - let axProps : LeanPlot.Axis.AxisProps := { dataKey? := toJson ax.dataKey, label? := ax.label, domain? := ax.domain, type := .number } + let axProps : LeanPlot.Axis.AxisProps := { dataKey? := some (toJson ax.dataKey), domain? := ax.domain, label? := ax.label, type := .number } ( : Html) | none => (Html.text "" : Html) let yAxisHtml := match spec.yAxis with | some ax => - let axProps : LeanPlot.Axis.AxisProps := { dataKey? := toJson ax.dataKey, label? := ax.label, domain? := ax.domain, type := .number } + let axProps : LeanPlot.Axis.AxisProps := { dataKey? := some (toJson ax.dataKey), domain? := ax.domain, label? := ax.label, type := .number } ( : Html) | none => (Html.text "" : Html) - let legendHtml := if spec.legend then (Html.text "" : Html) else (Html.text "" : Html) -- Temporarily removed Legend - -- Temporarily remove legend until a Legend component is available/created - -- let legendHtml := (Html.text "" : Html) + let legendHtml := if spec.legend then ( : Html) else (Html.text "" : Html) let mainChartComponent := -- Always use LineChart as the main container, it can host Scatter series too. @@ -204,7 +221,7 @@ def render (spec : PlotSpec) : Html := {xAxisHtml} {yAxisHtml} {legendHtml} - {Html.element "Fragment" #[] chartComponents} + {... chartComponents} : Html) let finalHtml := match spec.title with From 5a7ddc3fb5b966905b27933989c62f5f350e0199 Mon Sep 17 00:00:00 2001 From: Alok Singh Date: Thu, 8 May 2025 01:29:56 -0400 Subject: [PATCH 37/38] docs(notes): add RenderFragment rename roadmap to llms.txt --- llms.txt | 78 +++++++++++++++++++++++++++++++++++++++++++++++++++++++- 1 file changed, 77 insertions(+), 1 deletion(-) diff --git a/llms.txt b/llms.txt index 42a1591..5abfb97 100644 --- a/llms.txt +++ b/llms.txt @@ -184,4 +184,80 @@ NEW_LOG_ENTRY_BELOW --------------------------------------------------------------------- - [ ] Investigate and add Recharts Legend component (currently causes "unknown identifier"). - [ ] Implement typeclass-based rendering for `SeriesSpec`. -- [ ] Define `PlotSpec.stack` or `PlotSpec.addSeries` for multi-series plots. \ No newline at end of file +- [ ] Define `PlotSpec.stack` or `PlotSpec.addSeries` for multi-series plots. + +2025-05-06:10:30 UTC – Potential Dependent Type Design for Series Rendering +---------------------------------------------------------------------------- +Consider a more type-safe and extensible approach for handling heterogeneous series types and their rendering using dependent types (Σ-types). + +1. **`SeriesKind` Enum:** + ```lean + inductive SeriesKind where + | line | scatter | bar + deriving Repr, BEq + ``` + +2. **Specific Detail Structs per Kind:** + ```lean + structure LineSeriesDetails where + color : String + dot : Option Bool := true + -- ... other line-specific options + + structure ScatterSeriesDetails where + color : String + shape : String := "circle" + -- ... other scatter-specific options + ``` + +3. **Dependent Series Specification (`SeriesDSpec` - a Σ-type): + ```lean + structure SeriesDSpec where + kind : SeriesKind + name : String + dataKey : String + details : match kind with + | SeriesKind.line => LineSeriesDetails + | SeriesKind.scatter => ScatterSeriesDetails + | SeriesKind.bar => BarSeriesDetails -- (assuming BarSeriesDetails) + ``` + +4. **`PlotSpec.series` becomes `Array SeriesDSpec`.** + +5. **Refined `RenderSeries` Typeclass (parameterized by `SeriesKind`): + ```lean + class RenderSeries (kind : SeriesKind) where + render (name : String) (dataKey : String) (details : seriesKindToDetailsType kind) (allChartData : Array Json) : Html + ``` + (where `seriesKindToDetailsType` is a type-level function mapping `SeriesKind` to its detail struct type). + + Instances: + ```lean + instance : RenderSeries SeriesKind.line where + render name dataKey lineDetails _ := ... + + instance : RenderSeries SeriesKind.scatter where + render name dataKey scatterDetails _ := ... + ``` + +6. **`PlotSpec.render` uses the dependent renderer:** + Map over `spec.series : Array SeriesDSpec`, typeclass resolution finds the correct `RenderSeries` instance based on `s.kind` to render `s.details`. + +**Advantages:** Type safety (no string dispatch), better extensibility for new series types, improved tooling support, elimination of "unsupported type" runtime errors for series rendering. +**Considerations:** Increased initial complexity and potential boilerplate compared to simpler dispatch mechanisms. Good fit for a robust, extensible "grammar of graphics" style library. + +2025-05-08:05:29 UTC – RenderFragment & LayerSpec rename plan +------------------------------------------------------------- +• Naming audit completed; decided on: + – `RenderSeries` ⇒ **RenderFragment** (typeclass) + – `renderSeries` method ⇒ **render** + – `SeriesSpec` ⇒ **LayerSpec** +• Mermaid diagram drafted for current architecture. +• Next steps: + 1. Create branch `refactor/onomastics-fragment-layer`. + 2. Mechanical rename of types & instances; deprecate old names via `abbrev`. + 3. Update `Specification.lean` render pipeline and combinators. + 4. Add `RenderFragment AxisSpec` instance to demo polymorphism. + 5. Update demos, README, CHANGELOG (bump 0.3.0-alpha). + 6. Run `lake build` and docs pipeline. + 7. Commit per logical chunk; open PR targeting `main`. \ No newline at end of file From 8cc20bf88893ca2c47eff306321008b8753d324f Mon Sep 17 00:00:00 2001 From: Alok Singh Date: Thu, 8 May 2025 17:09:37 -0400 Subject: [PATCH 38/38] feat(core): add overlay operators * and /; demo OperatorPlayground showing multi-series overlay --- LeanPlot/Core.lean | 25 +++++++++++++++------ LeanPlot/Demos/OperatorPlayground.lean | 31 ++++++++++++++++++++++++++ 2 files changed, 49 insertions(+), 7 deletions(-) create mode 100644 LeanPlot/Demos/OperatorPlayground.lean diff --git a/LeanPlot/Core.lean b/LeanPlot/Core.lean index 5383441..0006cc6 100644 --- a/LeanPlot/Core.lean +++ b/LeanPlot/Core.lean @@ -70,18 +70,29 @@ The result is a `Plot` containing all layers from both operands. -/ instance (priority := 2000) [ToPlot α] [ToPlot β] : HAdd α β Plot where hAdd a b := Plot.overlay (toPlot a) (toPlot b) +/-- Generic `*` overlay via `[ToPlot]`. -/ +instance (priority := 2000) [ToPlot α] [ToPlot β] : HMul α β Plot where + hMul a b := Plot.overlay (toPlot a) (toPlot b) + +/-- Generic `/` overlay via `[ToPlot]`. Provided for API symmetry. -/ +instance (priority := 2000) [ToPlot α] [ToPlot β] : HDiv α β Plot where + hDiv a b := Plot.overlay (toPlot a) (toPlot b) + /-! ### Render instance ---------------------------------------------------- -/ instance : Render Layer where render := Layer.html -/-- Render a plot by vertically stacking each layer inside a `
` container. +/-- Render a plot by overlaying all layers in a single relative container. For line/scatter overlays we ideally want a *single* combined Recharts chart; -that is a future optimisation. The vertical stack is "correct" though perhaps -not visually perfect. -/ +that is a future optimisation. -/ instance : Render Plot where render p := - -- simple flex column -
- {... p.layers.map (fun l => l.html)} -
+ let rows := (List.range p.layers.size).toArray.map (fun idx => + let l := p.layers[idx]! + Html.element "div" + #[("key", Json.str (toString idx))] + #[l.html]) + Html.element "div" + #[("style", Json.str "display:flex; flex-direction:column;")] + rows diff --git a/LeanPlot/Demos/OperatorPlayground.lean b/LeanPlot/Demos/OperatorPlayground.lean new file mode 100644 index 0000000..806bfb5 --- /dev/null +++ b/LeanPlot/Demos/OperatorPlayground.lean @@ -0,0 +1,31 @@ +import LeanPlot.Components +import LeanPlot.Palette +import LeanPlot.Plot +import LeanPlot.Core +import LeanPlot +open LeanPlot.Components LeanPlot.Palette LeanPlot +open Lean ProofWidgets +open scoped ProofWidgets.Jsx + +/-! # Operator playground demo – revised + +React complained when stacking multiple full Recharts charts in one +panel. The most reliable demonstration of an *overlay* is therefore to +build **one** chart that already contains every series we want to show. + +Below we construct a three-series chart (id, sqr, sqrt) using +`sampleMany`. Render it with `#plot multiSeries`. -/ + +namespace LeanPlot.OperatorDemo + +private def multiSeries : Html := + mkLineChartFull + (sampleMany #[ + ("id", fun x => x), + ("sqr", fun x => x*x), + ("sqrt", fun x => Float.sqrt x)]) + (autoColours #["id", "sqr", "sqrt"]) + +#plot multiSeries +#plot line (fun x => x^3) +end LeanPlot.OperatorDemo