leanprover-community · Vtec234 · Mar 27, 2026 · Mar 27, 2026 · Mar 27, 2026 · Mar 27, 2026
diff --git a/.github/workflows/build.yml b/.github/workflows/build.yml
@@ -48,6 +48,9 @@ jobs:
       - name: Build package
         run: lake build ProofWidgets
 
+      - name: Check pre-built JS is up-to-date
+        run: git diff --exit-code widget/js/
+
       - name: Try publishing @leanprover-community/proofwidgets4
         if: ${{ startsWith(github.ref, 'refs/tags/v') && !contains(github.ref, '-pre') && matrix.os == 'ubuntu-latest' }}
         continue-on-error: true
@@ -65,15 +68,5 @@ jobs:
         with:
           prerelease: ${{ contains(github.ref, '-pre') }}
 
-      - name: Upload release archive (Ubuntu)
-        if: github.ref_type == 'tag' && matrix.os == 'ubuntu-latest'
-        run: lake upload $RELEASE_TAG
-        env:
-          GITHUB_TOKEN: ${{ secrets.GITHUB_TOKEN }}
-          RELEASE_TAG: ${{ github.ref_name }}
-
-      - name: Test release archive (Ubuntu)
-        if: github.ref_type == 'tag' && matrix.os == 'ubuntu-latest'
-        run: lake clean && lake build :release && lake build --no-build
     env:
       NPM_TOKEN: ${{ secrets.NPM_TOKEN }}
diff --git a/ProofWidgets/Component/Basic.lean b/ProofWidgets/Component/Basic.lean
@@ -74,7 +74,7 @@ preferrable to use the eager `InteractiveCode` in order to avoid the extra clien
 needed for the pretty-printing RPC call. -/
 @[widget_module]
 def InteractiveExpr : Component InteractiveExprProps where
-  javascript := include_str ".." / ".." / ".lake" / "build" / "js" / "interactiveExpr.js"
+  javascript := include_str ".." / ".." / "widget" / "js" / "interactiveExpr.js"
 
 structure InteractiveMessageProps where
   msg : Server.WithRpcRef MessageData

diff --git a/ProofWidgets/Component/FilterDetails.lean b/ProofWidgets/Component/FilterDetails.lean
@@ -24,6 +24,6 @@ but also has a filter button
 that allows you to switch between filtered and unfiltered states. -/
 @[widget_module]
 def FilterDetails : Component FilterDetailsProps where
-  javascript := include_str ".." /  ".." / ".lake" / "build" / "js" / "filterDetails.js"
+  javascript := include_str ".." /  ".." / "widget" / "js" / "filterDetails.js"
 
 end ProofWidgets
diff --git a/ProofWidgets/Component/GraphDisplay.lean b/ProofWidgets/Component/GraphDisplay.lean
@@ -140,6 +140,6 @@ end GraphDisplay
 /-- Display a graph with an interactive force simulation. -/
 @[widget_module]
 def GraphDisplay : Component GraphDisplay.Props where
-  javascript := include_str ".." / ".." / ".lake" / "build" / "js" / "d3Graph.js"
+  javascript := include_str ".." / ".." / "widget" / "js" / "d3Graph.js"
 
 end ProofWidgets
diff --git a/ProofWidgets/Component/HtmlDisplay.lean b/ProofWidgets/Component/HtmlDisplay.lean
@@ -16,11 +16,11 @@ structure HtmlDisplayProps where
 
 @[widget_module]
 def HtmlDisplay : Component HtmlDisplayProps where
-  javascript := include_str ".." / ".." / ".lake" / "build" / "js" / "htmlDisplay.js"
+  javascript := include_str ".." / ".." / "widget" / "js" / "htmlDisplay.js"
 
 @[widget_module]
 def HtmlDisplayPanel : Component HtmlDisplayProps where
-  javascript := include_str ".." / ".." / ".lake" / "build" / "js" / "htmlDisplayPanel.js"
+  javascript := include_str ".." / ".." / "widget" / "js" / "htmlDisplayPanel.js"
 
 open Lean Server Elab Command
 

diff --git a/ProofWidgets/Component/MakeEditLink.lean b/ProofWidgets/Component/MakeEditLink.lean
@@ -63,6 +63,6 @@ and potentially moves the cursor
 or makes a selection. -/
 @[widget_module]
 def MakeEditLink : Component MakeEditLinkProps where
-  javascript := include_str ".." / ".." / ".lake" / "build" / "js" / "makeEditLink.js"
+  javascript := include_str ".." / ".." / "widget" / "js" / "makeEditLink.js"
 
 end ProofWidgets
diff --git a/ProofWidgets/Component/OfRpcMethod.lean b/ProofWidgets/Component/OfRpcMethod.lean
@@ -10,7 +10,7 @@ public meta section
 namespace ProofWidgets
 open Lean Server Meta Elab Term
 
-def ofRpcMethodTemplate := include_str ".." / ".." / ".lake" / "build" / "js" / "ofRpcMethod.js"
+def ofRpcMethodTemplate := include_str ".." / ".." / "widget" / "js" / "ofRpcMethod.js"
 
 /-- The elaborator `mk_rpc_widget%` allows writing certain widgets in Lean instead of JavaScript.
 Specifically, it translates an RPC method of type `MyProps → RequestM (RequestTask Html)`

diff --git a/ProofWidgets/Component/Panel/GoalTypePanel.lean b/ProofWidgets/Component/Panel/GoalTypePanel.lean
@@ -9,6 +9,6 @@ namespace ProofWidgets
 /-- Display the goal type using known `Expr` presenters. -/
 @[widget_module]
 def GoalTypePanel : Component PanelWidgetProps where
-  javascript := include_str ".." / ".." / ".." / ".lake" / "build" / "js" / "goalTypePanel.js"
+  javascript := include_str ".." / ".." / ".." / "widget" / "js" / "goalTypePanel.js"
 
 end ProofWidgets
diff --git a/ProofWidgets/Component/Panel/SelectionPanel.lean b/ProofWidgets/Component/Panel/SelectionPanel.lean
@@ -49,6 +49,6 @@ presenter should be used to display each of those expressions.
 Expressions can be selected using shift-click. -/
 @[widget_module]
 def SelectionPanel : Component PanelWidgetProps where
-  javascript := include_str ".." / ".." / ".." / ".lake" / "build" / "js" / "presentSelection.js"
+  javascript := include_str ".." / ".." / ".." / "widget" / "js" / "presentSelection.js"
 
 end ProofWidgets
diff --git a/ProofWidgets/Component/PenroseDiagram.lean b/ProofWidgets/Component/PenroseDiagram.lean
@@ -44,7 +44,7 @@ and can be accessed as, for example, `theme.foreground` in the provided `sty` in
 the editor theme. -/
 @[widget_module]
 def Diagram : Component DiagramProps where
-  javascript := include_str ".." / ".." / ".lake" / "build" / "js" / "penroseDisplay.js"
+  javascript := include_str ".." / ".." / "widget" / "js" / "penroseDisplay.js"
 
 /-! # `DiagramBuilderM` -/
 

diff --git a/ProofWidgets/Component/Recharts.lean b/ProofWidgets/Component/Recharts.lean
@@ -9,7 +9,7 @@ open Lean
 
 @[widget_module]
 def Recharts : Widget.Module where
-  javascript := include_str ".." / ".." / ".lake" / "build" / "js" / "recharts.js"
+  javascript := include_str ".." / ".." / "widget" / "js" / "recharts.js"
 
 inductive LineChartLayout where
   | horizontal

diff --git a/ProofWidgets/Component/RefreshComponent.lean b/ProofWidgets/Component/RefreshComponent.lean
@@ -148,7 +148,7 @@ The component resets its state when rendered with a new `props.state`.
 Conversely, reusing `props.state` preserves the client-side state.  -/
 @[widget_module]
 def RefreshComponent : Component Props where
-  javascript := include_str ".." /  ".." / ".lake" / "build" / "js" / "RefreshComponent.js"
+  javascript := include_str ".." /  ".." / "widget" / "js" / "RefreshComponent.js"
 
 /-! ## API for creating a `RefreshComponent` -/
 

diff --git a/ProofWidgets/Demos/InteractiveSvg.lean b/ProofWidgets/Demos/InteractiveSvg.lean
@@ -48,7 +48,7 @@ def updateSvg (params : UpdateParams State) : RequestM (RequestTask (UpdateResul
 
 @[widget_module]
 def SvgWidget : Component (UpdateResult State) where
-  javascript := include_str ".." / ".." / ".lake" / "build" / "js" / "interactiveSvg.js"
+  javascript := include_str ".." / ".." / "widget" / "js" / "interactiveSvg.js"
 
 def init : UpdateResult State := {
   html := <div>Init!!!</div>,

diff --git a/ProofWidgets/Demos/Plot.lean b/ProofWidgets/Demos/Plot.lean
@@ -41,7 +41,7 @@ structure AnimatedHtmlProps where
 
 @[widget_module]
 def AnimatedHtml : Component AnimatedHtmlProps where
-  javascript := include_str ".." / ".." / ".lake" / "build" / "js" / "animatedHtml.js"
+  javascript := include_str ".." / ".." / "widget" / "js" / "animatedHtml.js"
 
 open scoped ProofWidgets.Jsx in
 -- put your cursor on the below line to see an animated widget

diff --git a/ProofWidgets/Demos/RbTree.lean b/ProofWidgets/Demos/RbTree.lean
@@ -102,7 +102,7 @@ open ProofWidgets
 
 @[widget_module]
 def RBDisplay : Component RBDisplayProps where
-  javascript := include_str ".." / ".." / ".lake" / "build" / "js" / "rbTree.js"
+  javascript := include_str ".." / ".." / "widget" / "js" / "rbTree.js"
 
 open scoped Jsx in
 partial def drawTree? (e : Expr) : MetaM (Option Html) := do

diff --git a/ProofWidgets/Demos/Rubiks.lean b/ProofWidgets/Demos/Rubiks.lean
@@ -13,7 +13,7 @@ structure RubiksProps where
 
 @[widget_module]
 def Rubiks : Component RubiksProps where
-  javascript := include_str ".." / ".." / ".lake" / "build" / "js" / "rubiks.js"
+  javascript := include_str ".." / ".." / "widget" / "js" / "rubiks.js"
 
 def eg := #["L", "L", "D⁻¹", "U⁻¹", "L", "D", "D", "L", "U⁻¹", "R", "D", "F", "F", "D"]
 

diff --git a/ProofWidgets/Presentation/Expr.lean b/ProofWidgets/Presentation/Expr.lean
@@ -95,6 +95,6 @@ are used to render the expression when selected. The one with highest precedence
 default. -/
 @[widget_module]
 def ExprPresentation : Component ExprPresentationProps where
-  javascript := include_str ".." / ".." / ".lake" / "build" / "js" / "exprPresentation.js"
+  javascript := include_str ".." / ".." / "widget" / "js" / "exprPresentation.js"
 
 end ProofWidgets
diff --git a/README.md b/README.md
@@ -23,48 +23,48 @@ for the foreseeable future.
 
 ### Viewing the demos
 
-The easiest way to get started is to clone a **release tag** of ProofWidgets and run
-`lake build :release`, as follows:
+To get started, clone ProofWidgets and run `lake build`, as follows:
 
 ```bash
-# You should replace v0.0.3 with the latest version published under Releases
-git clone https://github.com/leanprover-community/ProofWidgets4 --branch v0.0.3
+git clone https://github.com/leanprover-community/ProofWidgets4 --depth 1
 cd ProofWidgets4/
-lake build :release
+lake build
 ```
 
-After doing this you will hopefully be able to view the demos in `ProofWidgets/Demos/`. Top tip: use
-the pushpin icon (![pin](https://raw.githubusercontent.com/microsoft/vscode-codicons/31b33da05aab662f1973ba5667dad672c8e20fbc/src/icons/pin.svg))
-to keep a widget in view. You can then live code your widgets.
+After doing this you will hopefully be able to view the demos in `ProofWidgets/Demos/`.
+Top tip: use the pushpin icon (![pin](https://raw.githubusercontent.com/microsoft/vscode-codicons/31b33da05aab662f1973ba5667dad672c8e20fbc/src/icons/pin.svg))
+to keep a widget in view. You can then live-code your widgets.
 
 ### Using ProofWidgets as a dependency
 
-Put this in your `lakefile.lean`, making sure to reference a **release tag**
-rather than the `main` branch:
+To ensure ProofWidgets works with your version of the Lean toolchain,
+reference a **release tag** rather than the `main` branch.
+Add the following to your `lakefile.lean`:
 
 ```lean
--- You should replace v0.0.3 with the latest version published under Releases
-require proofwidgets from git "https://github.com/leanprover-community/ProofWidgets4"@"v0.0.3"
+-- Replace v0.0.3 with a version published under Releases
+require "leanprover-community" / "proofwidgets" @ git "v0.0.3"
 ```
 
 [Developing ProofWidgets](#developing-proofwidgets) involves building TypeScript code with NPM.
 When depending on `ProofWidgets` but not writing any custom TypeScript yourself,
-you likely want to spare yourself and your users from having to install and run NPM.
-ProofWidgets is configured to use Lake's [cloud releases](https://github.com/leanprover/lake/#cloud-releases) feature
-which will automatically fetch pre-built JavaScript files *as long as* you require a release tag
-rather than the `main` branch.
-In this mode, you and your users should not need to have NPM installed.
-However, fetching cloud release may sometimes fail,
-in which case ProofWidgets may still revert to a full build.
-You can force ProofWidgets to fail with a custom error in this case by importing it like so:
+you may want to spare yourself and your users from having to install and run NPM.
+This repository contains pre-built JavaScript files (`widget/js/`)
+which will be reused as long as none of the sources have changed.
+Consequently, you and your users should not need to have NPM installed.
+
+However, in case there is a bug in the build process,
+ProofWidgets may still revert to a full build.
+You can force ProofWidgets to fail with a custom error instead by importing it like so:
 
 ```lean
--- You should replace v0.0.3 with the latest version published under Releases
-require proofwidgets with NameMap.empty.insert `errorOnBuild "<my message>" from git "https://github.com/leanprover-community/ProofWidgets4"@"v0.0.3"
+-- Replace v0.0.3 with a version published under Releases
+require "leanprover-community" / "proofwidgets" @ git "v0.0.3"
+  with NameMap.empty.insert `errorOnBuild "<my message>"
 ```
 
 ⚠️ [EXPERIMENTAL] To use ProofWidgets4 JS components in widgets defined in other Lean packages,
-you can import [@leanprover-community/proofwidgets4](https://www.npmjs.com/package/@leanprover-community/proofwidgets4) from NPM.
+import [@leanprover-community/proofwidgets4](https://www.npmjs.com/package/@leanprover-community/proofwidgets4) from NPM.
 
 ## Features
 
@@ -124,17 +124,14 @@ In order to build only the TypeScript, run `lake build widgetJsAll`.
 Widgets can also be built in development mode using `lake build widgetJsAllDev`.
 This makes them easier to inspect in developer tools.
 
-💡 The NPM part of the build process may sometimes fail with missing packages.
-If this happens, run `npm clean-install` in the `widget/` directory and then try `lake build` again.
-
 We use the `include_str` term elaborator
 to splice the minified JavaScript
 produced during the first part of the build (by `tsc` and Rollup)
 into ProofWidgets Lean modules.
-The minifed JS is stored in `.lake/build/js/`.
+The minifed JS is stored in `widget/js/`.
 Modifying any TypeScript source will trigger a rebuild,
 and should correctly propagate the new minified code
-to where it used in Lean.
+to where it is used in Lean.
 
 ⚠️ Note however that due to Lake issue [#86](https://github.com/leanprover/lake/issues/86),
 *all* the widget sources are rebuilt whenever any single one changes,

diff --git a/RELEASES.md b/RELEASES.md
@@ -4,6 +4,12 @@ This file contains work-in-progress notes for the upcoming release, as well as p
 Please check the [releases](https://github.com/leanprover-community/ProofWidgets4/releases) page
 for the build artifacts.
 
+v0.0.95
+-------
+
+* Add pre-built JS files to the repository.
+  This removes our reliance on the Lake cloud release fetching these.
+
 v0.0.93
 -------
 

diff --git a/lakefile.lean b/lakefile.lean
@@ -2,9 +2,6 @@ import Lake
 open Lake DSL System
 
 package proofwidgets where
-  preferReleaseBuild := true
-  buildArchive? := "ProofWidgets4.tar.gz"
-  releaseRepo := "https://github.com/leanprover-community/ProofWidgets4"
 
 def widgetDir : FilePath := "widget"
 
@@ -59,17 +56,11 @@ def widgetJsAllTarget (pkg : Package) (isDev : Bool) : FetchM (Job Unit) := do
   let rollupConfig ← widgetRollupConfig.fetch
   let tsconfig ← widgetTsconfig.fetch
   let widgetPackageLock ← widgetPackageLock.fetch
-  /- `widgetJsAll` is built via `needs`,
-  and Lake's default build order is `needs -> cloud release -> main build`.
-  We must instead ensure that the cloud release is fetched first
-  so that this target does not build from scratch unnecessarily.
-  `afterBuildCacheAsync` guarantees this. -/
-  pkg.afterBuildCacheAsync do
   srcs.bindM (sync := true) fun _ =>
   rollupConfig.bindM (sync := true) fun _ =>
   tsconfig.bindM (sync := true) fun _ =>
   widgetPackageLock.mapM fun _ => do
-    let traceFile := pkg.buildDir / "js" / "lake.trace"
+    let traceFile := pkg.widgetDir / "js" / "lake.trace"
     buildUnlessUpToDate traceFile (← getTrace) traceFile do
       if let some msg := get_config? errorOnBuild then
         error msg
@@ -78,7 +69,6 @@ def widgetJsAllTarget (pkg : Package) (isDev : Bool) : FetchM (Job Unit) := do
        It would probably be better to have a proper target for `node_modules`
        that all the JS/TS modules depend on.
        BUT when we are being built as a dependency of another package
-       using the cloud releases feature,
        we wouldn't want that target to trigger
        since in that case NPM is not necessarily installed.
        Hence, we put this block inside the build process for JS/TS files

diff --git a/widget/js/RefreshComponent.js b/widget/js/RefreshComponent.js
diff --git a/widget/js/animatedHtml.js b/widget/js/animatedHtml.js
diff --git a/widget/js/cancellable.js b/widget/js/cancellable.js
diff --git a/widget/js/d3Graph.js b/widget/js/d3Graph.js
diff --git a/widget/js/exprPresentation.js b/widget/js/exprPresentation.js