chore: store pre-built JS in source tree (#165)

* chore: move JS build dir to widget/js/

* doc: new pre-built strategy

* chore: update widget/js

* ci: adjust to changes

* chore: bump @leanprover-community/proofwidgets4

Author: Vtec234

.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 }}

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

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

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

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
 

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

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)`

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

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

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` -/