fix

.github/workflows/build.yml

@@ -50,7 +50,7 @@ jobs:
         run: lake build ProofWidgets
 
       - name: Try publishing @leanprover-community/proofwidgets4
-        if: ${{ startsWith(github.ref, 'refs/tags/v') && !endsWith(github.ref, '-pre') && matrix.os == 'ubuntu-latest' }}
+        if: ${{ startsWith(github.ref, 'refs/tags/v') && !contains(github.ref, '-pre') && matrix.os == 'ubuntu-latest' }}
         continue-on-error: true
         run: cd widget/ && npm publish --access=public
 
@@ -59,7 +59,9 @@ jobs:
 
       - name: Create GitHub release for tag (Ubuntu)
         if: github.ref_type == 'tag' && matrix.os == 'ubuntu-latest'
-        uses: softprops/action-gh-release@v1
+        uses: softprops/action-gh-release@v2
+        with:
+          prerelease: ${{ contains(github.ref, '-pre') }}
 
       - name: Upload release archive (Ubuntu)
         if: github.ref_type == 'tag' && matrix.os == 'ubuntu-latest'

ProofWidgets/Component/Recharts.lean

@@ -38,10 +38,20 @@ def LineChart : Component LineChartProps where
   javascript := Recharts.javascript
   «export» := "LineChart"
 
+inductive AxisType where
+  /-- Treat values as numbers: spacing on axis by numeric difference. -/
+  | number
+  /-- Treat values as categorical: equal spacing between values. -/
+  | category
+  deriving FromJson, ToJson
+
 structure AxisProps where
   dataKey? : Option Json := none
   domain? : Option (Array Json) := none
   allowDataOverflow : Bool := false
+  /-- How values along this axis should be interpreted.
+  The Recharts default is `category`. -/
+  type : AxisType := .number
   -- TODO: There are many more props
   deriving FromJson, ToJson
 

ProofWidgets/Data/Svg.lean

@@ -158,7 +158,7 @@ end Svg
 
 def mkIdToIdx {f} (elements : Array (Svg.Element f)) : Std.HashMap String (Fin elements.size) :=
   let idToIdx := elements
-    |>.mapFinIdx (λ idx el => (idx, el)) -- zip with index
+    |>.mapFinIdx (λ idx el h => (⟨idx, h⟩, el)) -- zip with `Fin` index
     |>.filterMap (λ (idx,el) => el.id.map (λ id => (id, idx))) -- keep only elements with specified id
     |>.toList
     |> Std.HashMap.ofList

lake-manifest.json

@@ -5,10 +5,10 @@
    "type": "git",
    "subDir": null,
    "scope": "leanprover-community",
-   "rev": "7805acf1864ba1a2e359f86a8f092ccf1438ad83",
+   "rev": "e8dc5fc16c625fc4fe08f42d625523275ddbbb4b",
    "name": "batteries",
    "manifestFile": "lake-manifest.json",
-   "inputRev": "v4.15.0-rc1",
+   "inputRev": "v4.15.0",
    "inherited": false,
    "configFile": "lakefile.toml"}],
  "name": "proofwidgets",

lakefile.lean

@@ -6,7 +6,7 @@ package proofwidgets where
   buildArchive? := "ProofWidgets4.tar.gz"
   releaseRepo := "https://github.com/leanprover-community/ProofWidgets4"
 
-require "leanprover-community" / "batteries" @ git "v4.15.0-rc1"
+require "leanprover-community" / "batteries" @ git "v4.16.0-rc2"
 
 def npmCmd : String :=
   if Platform.isWindows then "npm.cmd" else "npm"

lean-toolchain

@@ -1 +1 @@
-leanprover/lean4:nightly-2024-12-19
+leanprover/lean4:nightly-2025-01-20