fix: CI lint driver issue and add Verso code roles

- Remove batteries lintDriver (not a dependency)
- Disable lint in lean-action CI workflow
- Add {lit} roles to Palette.lean hex colors
- Add scripts/install.sh for easy setup
- Update Justfile: replace lint with setup command

Author: alok

.github/workflows/lean_action_ci.yml

@@ -12,3 +12,5 @@ jobs:
     steps:
       - uses: actions/checkout@v4
       - uses: leanprover/lean-action@v1
+        with:
+          lint: false  # We don't use batteries linter

Justfile

@@ -12,9 +12,9 @@ build:
 clean:
 	lake clean
 
-# Run linter
-lint:
-	lake lint
+# Setup/install dependencies
+setup:
+	./scripts/install.sh
 
 # Generate documentation images (SVG)
 doc-images:

LeanPlot/Components.lean

@@ -311,64 +311,64 @@ of dots.  The bar color is supplied via {lit}`fillColor`.
 /-! ## Simple Plotting (Zero-Configuration Plots) -/
 
 /-- 🎯 Plot a function with automatic everything. Just works!
-    
+
 Examples:
 - {lit}`plotSimple (fun t => t^2)` - Simple quadratic plot
 - {lit}`plotSimple (fun x => x + 1)` - Linear function
 - {lit}`plotSimple (fun i => i * 2)` - Linear scaling
 
 You never have to think about axis labels again!
 -/
-def plotSimple {β} [ToFloat β] (f : Float → β) (steps : Nat := 200) 
+def plotSimple {β} [ToFloat β] (f : Float → β) (steps : Nat := 200)
     (domain : Option (Float × Float) := none) (w h : Nat := 400) : Html :=
   -- Sample the function
   let data := sample f steps domain
-  
+
   -- Generate axis labels (this would use metaprogramming in full implementation)
   -- For now, provide sensible defaults that work with the common patterns
-  let xLabel := "x" 
+  let xLabel := "x"
   let yLabel := "f(x)"
   let seriesStrokes := #[("y", "#2563eb")]  -- Nice blue color
-  
+
   mkLineChartWithLabels data seriesStrokes (some xLabel) (some yLabel) w h
 
 /-- Plot multiple functions with automatic labeling.
     Just pass your functions and get a beautiful multi-line plot!
-    
-Examples:  
+
+Examples:
 - {lit}`plotManySimple #[("sin", fun t => Float.sin t), ("cos", fun t => Float.cos t)]`
 - {lit}`plotManySimple #[("linear", fun x => x), ("quadratic", fun x => x^2)]`
 
 Everything is automatic - colors, labels, legend!
 -/
-def plotManySimple {β} [ToFloat β] (fns : Array (String × (Float → β))) 
-    (steps : Nat := 200) (domain : Float × Float := (0.0, 1.0)) 
+def plotManySimple {β} [ToFloat β] (fns : Array (String × (Float → β)))
+    (steps : Nat := 200) (domain : Float × Float := (0.0, 1.0))
     (w h : Nat := 400) : Html :=
   -- Sample all functions
   let data := sampleMany fns steps domain.1 domain.2
-  
-  -- Generate axis labels  
+
+  -- Generate axis labels
   let xLabel := "x"  -- Could be enhanced with metaprogramming
   let yLabel := "y"  -- Could be enhanced with metaprogramming
-  
+
   -- Auto-generate colors for each series
   let colors := #["#2563eb", "#dc2626", "#16a34a", "#ca8a04", "#7c3aed", "#db2777"]
-  let seriesStrokes := fns.mapIdx fun i (name, _) => 
+  let seriesStrokes := fns.mapIdx fun i (name, _) =>
     let color := colors.getD (i % colors.size) "#64748b"
     (name, color)
-  
+
   mkLineChartFull data seriesStrokes (some xLabel) (some yLabel) w h
 
 /-- Scatter plot with automatic labeling. -/
-def scatterSimple {β} [ToFloat β] (f : Float → β) (steps : Nat := 200) 
+def scatterSimple {β} [ToFloat β] (f : Float → β) (steps : Nat := 200)
     (domain : Option (Float × Float) := none) (w h : Nat := 400) : Html :=
   let data := sample f steps domain
   mkScatterChart data "#dc2626" w h  -- Nice red color
 
-/-- Bar chart with automatic labeling. -/  
+/-- Bar chart with automatic labeling. -/
 def barSimple {β} [ToFloat β] (f : Float → β) (steps : Nat := 200)
     (domain : Option (Float × Float) := none) (w h : Nat := 400) : Html :=
-  let data := sample f steps domain  
+  let data := sample f steps domain
   mkBarChart data "#16a34a" w h  -- Nice green color
 
 /-- Enhanced line chart builder with automatic axis label generation.

LeanPlot/Palette.lean

@@ -30,10 +30,10 @@ def bluePurple : Color := "#3e4a89"
 /-- Medium blue ({lit}`#31688e`). -/
 def blue : Color := "#31688e"
 
-/-- Turquoise (#26828e). -/
+/-- Turquoise ({lit}`#26828e`). -/
 def turquoise : Color := "#26828e"
 
-/-- Green-turquoise (#1f9e89). -/
+/-- Green-turquoise ({lit}`#1f9e89`). -/
 def greenTurquoise : Color := "#1f9e89"
 
 /-- Green ({lit}`#35b779`). -/

lakefile.toml

@@ -5,9 +5,6 @@ version = "0.1.0"
 # Build default
 defaultTargets = ["leanplot"]
 
-# Tell `lake lint` which executable to invoke. Batteries ships a `runLinter` executable
-# that understands its extended linting framework, so we delegate to it here.
-lintDriver = "batteries/runLinter"
 
 [leanOptions]
 pp.unicode.fun = true

scripts/install.sh

@@ -0,0 +1,33 @@
+#!/usr/bin/env bash
+# LeanPlot installation script
+# Usage: ./scripts/install.sh
+
+set -euo pipefail
+
+echo "=== LeanPlot Setup ==="
+
+# Check for elan
+if ! command -v elan &> /dev/null; then
+    echo "Installing elan (Lean toolchain manager)..."
+    curl https://raw.githubusercontent.com/leanprover/elan/master/elan-init.sh -sSf | sh -s -- -y --default-toolchain none
+    export PATH="$HOME/.elan/bin:$PATH"
+else
+    echo "✓ elan already installed"
+fi
+
+# Ensure elan is in PATH
+if [[ ":$PATH:" != *":$HOME/.elan/bin:"* ]]; then
+    export PATH="$HOME/.elan/bin:$PATH"
+fi
+
+# Get dependencies and build
+echo "Fetching dependencies..."
+lake update
+
+echo "Building LeanPlot..."
+lake build
+
+echo ""
+echo "=== Setup Complete ==="
+echo "Run 'just' to see available commands"
+