chore: merge main

.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/Cancellable.lean

@@ -4,6 +4,9 @@ public meta import Lean.Data.Json.FromToJson
 public meta import Lean.Server.Rpc.RequestHandling
 public meta import Std.Data.HashMap
 public meta import ProofWidgets.Compat
+public meta import ProofWidgets.Util
+
+/-! # This file is DEPRECATED since v0.0.93 -/
 
 public meta section
 
@@ -45,12 +48,11 @@ def mkCancellable [RpcEncodable β] (handler : α → RequestM (RequestTask β))
 /-- Cancel the request with ID `rid`.
 Does nothing if `rid` is invalid. -/
 @[server_rpc_method]
-def cancelRequest (rid : RequestId) : RequestM (RequestTask String) := do
+def cancelRequest (rid : RequestId) : RequestM (RequestTask Unit) := do
   RequestM.asTask do
     let t? ← runningRequests.modifyGet fun (id, m) => (m[rid]?, (id, m.erase rid))
     if let some t := t? then
       t.cancel
-    return "ok"
 
 /-- The status of a running cancellable request. -/
 inductive CheckRequestResponse
@@ -99,6 +101,14 @@ initialize
     see `callCancellable` in `cancellable.ts`."
     applicationTime := AttributeApplicationTime.afterCompilation
     add := fun decl _ _ => Prod.fst <$> MetaM.run do
+      logWarning "\
+        This attribute is deprecated since ProofWidgets v0.0.93.\n\n\
+        To migrate, replace `@[server_rpc_method_cancellable]` with `@[server_rpc_method]`,\n\
+        and replace calls to `IO.checkCanceled` with `RequestM.checkCancelled`.\n\n\
+        If the RPC method spawns `CoreM` computations,\n\
+        it is also encouraged to pass `RequestContext.cancelTk.cancelledByCancelRequest`
+        into `Core.Context`."
+
       let name := decl ++ cancellableSuffix
       let value ← mkAppM ``mkCancellable #[mkConst decl]
       addAndCompile $ .defnDecl {

ProofWidgets/Compat.lean

@@ -7,6 +7,7 @@ public meta section
 namespace ProofWidgets
 open Lean Server Elab
 
+/-- See `RpcEncodable`. -/
 abbrev LazyEncodable α := StateM RpcObjectStore α
 
 -- back from exile

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

@@ -10,20 +10,16 @@ open ProofWidgets in
 /-- Save the expression corresponding to a goals location. -/
 def Lean.SubExpr.GoalsLocation.saveExprWithCtx (loc : GoalsLocation) : MetaM ExprWithCtx :=
   let mvarId := loc.mvarId
-  match loc.loc with
-  | .hyp fv =>
-    mvarId.withContext <|
-      ExprWithCtx.save (mkFVar fv)
-  | .hypType fv pos => mvarId.withContext do
-    let tp ← Meta.inferType (mkFVar fv)
-    Meta.viewSubexpr (visit := fun _ => ExprWithCtx.save) pos tp
-  | .hypValue fv pos => mvarId.withContext do
-    let some val ← fv.getValue?
-      | throwError "fvar {mkFVar fv} is not a let-binding"
-    Meta.viewSubexpr (visit := fun _ => ExprWithCtx.save) pos val
-  | .target pos => mvarId.withContext do
-    let tp ← Meta.inferType (mkMVar mvarId)
-    Meta.viewSubexpr (visit := fun _ => ExprWithCtx.save) pos tp
+  mvarId.withContext do
+    match loc.loc with
+    | .hyp fvarId => ExprWithCtx.save (.fvar fvarId)
+    | .hypType fvarId pos =>
+      Meta.viewSubexpr (fun _ => ExprWithCtx.save) pos (← instantiateMVars (← fvarId.getType))
+    | .hypValue fvarId pos =>
+      let some val ← fvarId.getValue? | throwError "fvar {Expr.fvar fvarId} is not a let-binding"
+      Meta.viewSubexpr (fun _ => ExprWithCtx.save) pos (← instantiateMVars val)
+    | .target pos =>
+      Meta.viewSubexpr (fun _ => ExprWithCtx.save) pos (← instantiateMVars (← mvarId.getType))
 
 namespace ProofWidgets
 open Lean Server
@@ -53,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` -/
 

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