feat: Add first-class Graphic type with algebraic operators and PNG/SVG export

Core Features:
- Graphic type with +, |||, / operators for overlay/faceting
- HtmlEval instance for #eval rendering in infoview
- Fluent combinators: .domain, .samples, .color, .title, etc.
- Interactive sliders with source code rewriting via #iplot

PNG Rendering Infrastructure:
- Bitmap module for RGB colors and pixel manipulation
- CRC32 and Adler32 checksums for PNG encoding
- Rasterization primitives (Bresenham's line algorithm)
- savePNG/saveSVG export functions

Documentation Fixes:
- Fixed Verso header nesting errors
- Fixed mermaid code block to plain text
- Converted lean code blocks to plain for examples
- Updated module docstrings for Verso compatibility

Also includes TestExport.lean for verifying PNG/SVG export works.

Author: alok

.gitignore

@@ -8,3 +8,8 @@ _out/
 *.un~
 .venv/
 node_modules/
+
+# Generated test files
+*.png
+*.svg
+!doc/img/*.svg

LeanPlot.lean

@@ -5,27 +5,39 @@ Interactive plotting for Lean 4.
 
 ## Main API
 
-Import `LeanPlot.API` and `LeanPlot.DSL` for the primary plotting functions:
-- `plot` - Single function plots
+Import `LeanPlot.Graphic` for first-class algebraic graphics:
+- `plot f` - Create a function plot
+- `scatter pts` - Scatter plot from points
+- `bar pts` - Bar chart from points
+- Algebraic operators: `+` (overlay), `|||` (horizontal facet), `/` (vertical facet)
+- Fluent combinators: `.domain`, `.samples`, `.color`, `.title`, etc.
+
+Import `LeanPlot.API` and `LeanPlot.DSL` for legacy plotting functions:
 - `plotMany` - Multiple function comparison
-- `scatter` - Scatter plots
-- `bar` - Bar charts
 - `#plot` - Convenient syntax for quick visualization
 
+## PNG/SVG Export
+
+Import `LeanPlot.Render.Export` for file export:
+- `g.savePNG "path.png"` - Save graphic to PNG
+- `g.saveSVG "path.svg"` - Save graphic to SVG
+
 ## Advanced Features
 
 - `LeanPlot.GrammarOfGraphics` - Grammar of Graphics DSL
+- `LeanPlot.Interactive` - Two-way slider widgets
 - `LeanPlot.PlotComposition` - Subplot grids and composition
 - `LeanPlot.Transform` - Data transformations (log, sqrt, etc.)
 - `LeanPlot.Faceting` - Small multiples layouts
-- `LeanPlot.Debug` - PNG export utilities
 
 ## Demos
 
 See `LeanPlot.Demos.*` for example usage.
 -/
 
 -- Core API (what users should import)
+import LeanPlot.Graphic  -- First-class algebraic graphics
+import LeanPlot.Interactive  -- Two-way slider widgets
 import LeanPlot.API
 import LeanPlot.DSL
 import LeanPlot.ToFloat
@@ -51,6 +63,14 @@ import LeanPlot.Faceting
 import LeanPlot.Debug
 import LeanPlot.Metaprogramming
 
+-- Rendering / Export
+import LeanPlot.Render.Bitmap
+import LeanPlot.Render.Rasterize
+import LeanPlot.Render.PNG.CRC32
+import LeanPlot.Render.PNG.Adler32
+import LeanPlot.Render.PNG.Encode
+import LeanPlot.Render.Export
+
 -- Internal (re-exported for compatibility)
 import LeanPlot.Series
 import LeanPlot.Core

LeanPlot/API.lean

@@ -90,7 +90,7 @@ These are now the **recommended** way to create plots in LeanPlot.
 /-- **Simple line chart** - Just pass your function, get beautiful plot!
 
 Examples:
-```lean
+```
 #plot plot (fun t => t^2)                    -- Automatic "time" labels
 #plot plot (fun x => Float.sin x)           -- Automatic "x" labels
 #plot plot (fun i => i * 3) (steps := 100)  -- Custom sample count
@@ -106,7 +106,7 @@ This is the new recommended way to plot functions. Zero configuration needed!
 /-- **Simple multi-function plot** - Multiple functions, automatic everything!
 
 Examples:
-```lean
+```
 #plot plotMany #[("sin", fun x => Float.sin x), ("cos", fun x => Float.cos x)]
 #plot plotMany #[("linear", fun t => t), ("quadratic", fun t => t^2)] (domain := (0.0, 2.0))
 ```
@@ -122,7 +122,7 @@ Automatic colors, legend, and labels. Perfect for comparing functions!
 
 Examples:
 
-```lean
+```
 #plot scatter (fun x => x + Random.rand)  -- Show function with noise
 #plot scatter (fun t => Float.sin t) (steps := 50)  -- Fewer points
 ```
@@ -135,7 +135,7 @@ Examples:
 /-- **Simple bar chart** - Bars with automatic styling!
 
 Examples:
-```lean
+```
 #plot bar (fun i => i^2) (steps := 10)     -- Discrete function as bars
 #plot bar (fun x => Float.floor x) (steps := 20)  -- Step function
 ```

LeanPlot/Demos/BarDemo.lean

@@ -3,10 +3,10 @@ import LeanPlot.Plot
 
 open LeanPlot
 open LeanPlot.PlotSpec
-
+set_option doc.verso true
 namespace LeanPlot.Demos
 
-/-- A tiny dataset of five bars illustrating the `bar` constructor. -/
+/-- A tiny dataset of five bars illustrating the {name}`bar` constructor. -/
 @[inline] def barData : Array (Float × Float) := #[(0.0, 1.0), (1.0, 2.0), (2.0, 3.0), (3.0, 2.0), (4.0, 1.0)]
 
 /- Render the bar chart. -/

LeanPlot/Demos/SimpleSyntaxDemo.lean

@@ -21,21 +21,21 @@ namespace LeanPlot.Demos.SimpleSyntaxDemo
 /-- Example 2: With custom sample count -/
 #plot (fun t => Float.sin t) using 400
 
-/-- Example 3: Works with any function
+/-- Example 3: Works with any function -/
 #plot (fun x => Float.exp (-x) * Float.cos (3 * x))
 
--- Example 4: Without parentheses also works
+/-- Example 4: Without parentheses also works -/
 #plot fun x => Float.tanh (x - 1)
 
--- Example 5: With type annotations
+/-- Example 5: With type annotations -/
 #plot (fun x : Float => x^3 - 2*x)
 
 /-! ## Doc Comments as Captions
 
 You can add a doc comment before `#plot` to display a caption:
 -/
 
-/-- The classic parabola y = x² -/
+/-- The classic quadratic function y = x² -/
 #plot (fun x => x^2)
 
 /-- A damped oscillation: exponential decay × cosine -/
@@ -68,4 +68,66 @@ Now you can write:
 It's that simple!
 -/
 
+/-! ## Syntax Experiment: Exactly 0 or 2 Doc Strings
+
+Just for fun, here's a command that requires either no doc strings or exactly two
+(title + subtitle). Uses `(docComment docComment)?` pattern.
+-/
+
+open Lean Elab Command ProofWidgets in
+/-- A plot command that takes exactly 0 or 2 doc strings (title + subtitle). -/
+syntax (name := plot2docs) (docComment docComment)? "#plot₂ " term : command
+
+open Lean Elab Command ProofWidgets LeanPlot.PlotCommand in
+/-- A plot command that takes exactly 0 or 2 doc strings (title + subtitle). -/
+@[command_elab plot2docs]
+def elabPlot2Docs : CommandElab := fun stx => do
+  let (title?, subtitle?, term) ← match stx with
+    | `($t:docComment $s:docComment #plot₂ $e:term) =>
+      pure (some t.getDocString, some s.getDocString, e)
+    | `(#plot₂ $e:term) =>
+      pure (none, none, e)
+    | _ => throwUnsupportedSyntax
+  let wrappedStx ← `(LeanPlot.API.plot $term)
+  let htX ← liftTermElabM <| HtmlCommand.evalCommandMHtml <| ← ``(ProofWidgets.HtmlEval.eval $wrappedStx)
+  let ht ← htX
+  -- Build HTML with optional title + subtitle
+  let finalHtml := match title?, subtitle? with
+    | some t, some s =>
+      let style : Json := Json.mkObj [
+        ("display", "flex"), ("flexDirection", "column"), ("marginBottom", "8px")
+      ]
+      let titleStyle : Json := Json.mkObj [
+        ("fontSize", "16px"), ("fontWeight", "600"), ("color", "#1f2937"),
+        ("fontFamily", "ui-monospace, SFMono-Regular, Menlo, Monaco, Consolas, monospace")
+      ]
+      let subStyle : Json := Json.mkObj [
+        ("fontSize", "12px"), ("color", "#6b7280"), ("fontStyle", "italic"),
+        ("fontFamily", "ui-monospace, SFMono-Regular, Menlo, Monaco, Consolas, monospace")
+      ]
+      Html.element "div" #[] #[
+        Html.element "div" #[("style", style)] #[
+          Html.element "div" #[("style", titleStyle)] #[.text t],
+          Html.element "div" #[("style", subStyle)] #[.text s]
+        ],
+        ht
+      ]
+    | _, _ => ht
+  liftCoreM <| Widget.savePanelWidgetInfo
+    (hash ProofWidgets.HtmlDisplayPanel.javascript)
+    (return json% { html: $(← Server.rpcEncode finalHtml) })
+    stx
+
+-- ✅ Works: No doc strings
+#plot₂ (fun x => x^2)
+
+-- ✅ Works: Exactly two doc strings (title + subtitle)
+/-- The Parabola -/
+/-- A classic quadratic function showing y = x² -/
+#plot₂ (fun x => x^2)
+
+-- ❌ Won't parse: Just one doc string (try uncommenting!)
+-- /-- Only one doc string -/
+-- #plot₂ (fun x => x^3)
+
 end LeanPlot.Demos.SimpleSyntaxDemo