diff --git a/ProofWidgets/Cancellable.lean b/ProofWidgets/Cancellable.lean index 4e105e8..5098159 100644 --- a/ProofWidgets/Cancellable.lean +++ b/ProofWidgets/Cancellable.lean @@ -4,6 +4,7 @@ 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 public meta section @@ -45,12 +46,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 diff --git a/ProofWidgets/Component/RefreshComponent.lean b/ProofWidgets/Component/RefreshComponent.lean new file mode 100644 index 0000000..5b88e2f --- /dev/null +++ b/ProofWidgets/Component/RefreshComponent.lean @@ -0,0 +1,215 @@ +/- +Copyright (c) 2025 Jovan Gerbscheid. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: Jovan Gerbscheid +-/ +import ProofWidgets.Data.Html +import ProofWidgets.Util + +/-! +## The `RefreshComponent` widget + +This file defines `RefreshComponent`, which allows you to have an HTML widget that updates +incrementally as more results are computed by a Lean computation. + +For this interaction, we use an `IO.Ref` that the JavaScript reads from. +It stores the HTML that should currently be on display, and a task returning the next HTML. +To determine whether the widget is up to date, each computed HTML has an associated version number. +(So, the `n`-th HTML will have index `n`) + +When the widget (re)loads, it first loads the current HTML from the ref, and then +repeatedly awaits further HTML result. +-/ + +namespace ProofWidgets +open Lean Server Widget Jsx +namespace RefreshComponent + +/-- The result that is sent to the `RefreshComponent` after each query. -/ +structure VersionedHtml where + /-- The new HTML that will replace the current HTML. -/ + html : Html + /-- The version number of the HTML. It is a count of how many HTMLs were created. -/ + idx : Nat + deriving RpcEncodable, Inhabited + +/-- The `RefreshState` stores the incremental result of the HTML computation. -/ +structure RefreshState where + /-- The state that the widget should currently be in. -/ + curr : VersionedHtml + /-- A task that returns the next state for the widget. + It is implemented using `IO.Promise.result?`, or `.pure none`. -/ + next : Task (Option VersionedHtml) + +/-- A reference to a `RefreshState`. This is used to keep track of the refresh state. -/ +def RefreshRef := IO.Ref RefreshState + +instance : TypeName RefreshRef := unsafe .mk RefreshRef ``RefreshRef + +/-- The data used to call `awaitRefresh`, for updating the HTML display. -/ +structure AwaitRefreshParams where + /-- The reference to the `RefreshState`. -/ + state : WithRpcRef RefreshRef + /-- The index of the HTML that is currently on display. -/ + oldIdx : Nat + deriving RpcEncodable + + +/-- `awaitRefresh` is called through RPC to obtain the next HTML to display. -/ +@[server_rpc_method] +def awaitRefresh (props : AwaitRefreshParams) : RequestM (RequestTask (Option VersionedHtml)) := do + let { curr, next } ← props.state.val.get + -- If `props.oldIdx < curr.idx`, that means that the state has updated in the meantime. + -- So, returning `curr` will give a refresh. + -- If `props.oldIdx = curr.idx`, then we need to await `next` to get a refresh + if props.oldIdx = curr.idx then + return .mapCheap .ok ⟨next⟩ + else + return .pure curr + +/-- +`getCurrState` is called through RPC whenever the widget reloads. +This can be because the infoview was closed and reopened, +or because a different expression was selected in the goal. +-/ +@[server_rpc_method] +def getCurrState (ref : WithRpcRef RefreshRef) : RequestM (RequestTask VersionedHtml) := do + return .pure (← ref.val.get).curr + + +deriving instance TypeName for IO.CancelToken + +/-- `cancelRefresh` is called through RPC by `RefreshComponent` upon cancellation. +It sets the cancel token for the task(s) on the Lean side. -/ +@[server_rpc_method] +def cancelRefresh (cancelTk : WithRpcRef IO.CancelToken) : RequestM (RequestTask Unit) := do + cancelTk.val.set + return .pure () + + +/-- The arguments passed to `RefreshComponent`. -/ +structure RefreshComponentProps where + /-- The refresh state that is queried for updating the display. -/ + state : WithRpcRef RefreshRef + /-- The cancel token that will be set when the component is unloaded/reloaded. -/ + cancelTk : Option (WithRpcRef IO.CancelToken) + deriving RpcEncodable + +/-- Display an inital HTML, and repeatedly update the display with new HTML objects +as they appear in `state`. A dedicated thread should be spawned in order to modify `state`. -/ +@[widget_module] +def RefreshComponent : Component RefreshComponentProps where + javascript := include_str ".." / ".." / ".lake" / "build" / "js" / "RefreshComponent.js" + + +/-! ## API for creating `RefreshComponent`s -/ + +/-- The monad transformer for maintaining a `RefreshComponent`. -/ +abbrev RefreshT (m : Type → Type) := + ReaderT (IO.Promise VersionedHtml) <| StateRefT' IO.RealWorld RefreshState m + +variable {m : Type → Type} [Monad m] [MonadLiftT BaseIO m] + [MonadLiftT (ST IO.RealWorld) m] + +/-- `RefreshStep` represents an update to the refresh state. -/ +inductive RefreshStep (m : Type → Type) where + /-- Leaves the current HTML in place and stops the refreshing. -/ + | none + /-- Sets the current HTML to `html` and stops the refreshing. -/ + | last (html : Html) + /-- Sets the current HTML to `html` and continues refreshing with `cont`. -/ + | cont' (html : Html) (cont : RefreshT m Unit) + deriving Inhabited + +/-- Update `RefreshState` and resolve `IO.Promise VersionedHtml` using the given `RefreshStep`. -/ +def runRefreshStep (k : RefreshStep m) : RefreshT m Unit := do + let idx := (← get).curr.idx + 1 + match k with + | .none => + modify fun { curr, .. } => { curr, next := .pure none } + -- we drop the reference to the promise, so the corresponding task will return `none`. + | .last html => + MonadState.set { curr := { html, idx }, next := .pure none } + (← read).resolve { html, idx } + | .cont' html cont => + let newPromise ← IO.Promise.new + MonadState.set { curr := { html, idx }, next := newPromise.result? } + (← read).resolve { html, idx } + withReader (fun _ => newPromise) cont + +/-- Update `RefreshState` and resolve `IO.Promise VersionedHtml` using the given `RefreshStep`. +Also catch all exceptions that `k` might throw. -/ +def runRefreshStepM [i : MonadAlwaysExcept Exception m] (k : m (RefreshStep m)) : RefreshT m Unit := do + have := i.except + runRefreshStep <| ← + try k + catch e => + if let .internal id _ := e then + if id == interruptExceptionId then + return .last <| .text "This component was cancelled" + return .last + + Error refreshing this component: + + +@[inherit_doc RefreshStep.cont'] +def RefreshStep.cont [MonadAlwaysExcept Exception m] + (html : Html) (cont : m (RefreshStep m)) : RefreshStep m := + .cont' html (runRefreshStepM cont) + +/-- Store a `IO.CancelToken` for all widgets initialized by `mkGoalRefreshComponent`. -/ +initialize cancelTokenMap : IO.Ref (Std.HashMap Name IO.CancelToken) ← + IO.mkRef {} + +end RefreshComponent + +open RefreshComponent + +/-- +Create a `RefreshComponent` in the context of a `Widget.InteractiveGoal`. +This should be used when the refreshing widget depends on shift-clicked expressions in the goal. + +Warning: after the expression selections in the goal have been updated, the thread that +updates the `RefreshState` has started running on the Lean server before the new version of the +widget is loaded. The advantage is that there is no delay before the computation starts. +The disadvantage is that if a `RefreshComponent` is reloaded too quickly, +(for example when rapidly clicking on expressions in the goal) +it doesn't call `cancelRefresh`, and the thread will continue running unneccessarily. +To fix this, we globally store a cancel token for each such widget. +The argument `key` is used to differentiate the widgets for this purpose. +If the same widget is loaded again, we set the previous cancel token. +As a result, there can be at most one instance of that particular widget +running at a time, and any other instances will say `This component was cancelled`. +This is usually not an issue because there is no reason to have the widget duplicated. + +TODO: when the infoview gets closed, `cancelRefresh` isn't run, and I don't know how to fix this. +-/ +def mkGoalRefreshComponent (goal : Widget.InteractiveGoal) (initial : Html) + (k : MetaM (RefreshStep MetaM)) (key : Name := by exact decl_name%) : BaseIO Html := do + let cancelTk ← IO.CancelToken.new + if let some oldTk ← cancelTokenMap.modifyGet fun map => (map[key]?, map.insert key cancelTk) then + oldTk.set + let promise ← IO.Promise.new + let ref ← IO.mkRef { curr := { html := initial, idx := 0 }, next := promise.result? } + discard <| IO.asTask (prio := .dedicated) do + goal.ctx.val.runMetaM {} do withTheReader Core.Context ({ · with cancelTk? := cancelTk }) do + let decl ← goal.mvarId.getDecl + let lctx := decl.lctx |>.sanitizeNames.run' {options := (← getOptions)} + Meta.withLCtx lctx decl.localInstances <| (runRefreshStepM k) promise ref + return + +/-- Create a `RefreshComponent`. To support cancellation, `m` should extend `CoreM`, +and hence have access to a cancel token. -/ +def mkRefreshComponentM {m ε} [Monad m] [MonadDrop m (EIO ε)] [MonadLiftT BaseIO m] + [MonadLiftT (ST IO.RealWorld) m] [MonadAlwaysExcept Exception m] + (initial : Html) (k : m (RefreshStep m)) : m Html := do + let promise ← IO.Promise.new + let ref ← IO.mkRef { curr := { html := initial, idx := 0 }, next := promise.result? } + discard <| EIO.asTask (prio := .dedicated) <| ← dropM <| (runRefreshStepM k) promise ref + return + +end ProofWidgets diff --git a/ProofWidgets/Demos/RefreshComponent.lean b/ProofWidgets/Demos/RefreshComponent.lean new file mode 100644 index 0000000..356dbea --- /dev/null +++ b/ProofWidgets/Demos/RefreshComponent.lean @@ -0,0 +1,134 @@ +import ProofWidgets.Component.RefreshComponent +import ProofWidgets.Component.HtmlDisplay +import ProofWidgets.Component.OfRpcMethod +import ProofWidgets.Component.Panel.SelectionPanel + +/-! +This file showcases the `RefreshComponent` using some basic examples. + +We use `dbg_trace` to help see which Lean processes are active at any time. +-/ + +open Lean.Widget ProofWidgets RefreshComponent Jsx Lean Server + + +/-! Example 1: Counting up to 10 -/ + +partial def countToTen : CoreM Html := do + mkRefreshComponentM (.text "Let's count to ten!!!") (count 0) +where + count (n : Nat) : CoreM (RefreshStep CoreM) := do + IO.sleep 1000 + dbg_trace "counted {n}" + Core.checkSystem "count to ten" + if n = 10 then + return .last <| .text s!"Wie niet weg is, is gezien, ik kom!!!" + else + return .cont (.text s!"{n + 1}!!!") (count (n + 1)) + +-- If you close and reopen the infoview, the counting continues as if it was open the whole time. +#html countToTen + +-- Here, we duplicate the widget using the same underlying computation +-- #html (do let x ← countToTen; return {x}
{x}) + +-- Here, we duplicate the widget and duplicate the underlying computation +-- #html (return {← countToTen}
{← countToTen}) + + + +/-! Example 2: print the selected expressions one by one in an infinite loop -/ + +@[server_rpc_method] +partial def cycleSelections (props : PanelWidgetProps) : RequestM (RequestTask Html) := + RequestM.asTask do + let some goal := props.goals[0]? | return .text "there are no goals" + mkGoalRefreshComponent goal (.text "loading...") do + let args ← props.selectedLocations.mapM (·.saveExprWithCtx) + if h : args.size ≠ 0 then + have : NeZero args.size := ⟨h⟩ + loop args 0 + else + return .last <| .text "please select some expression" +where + loop (args : Array ExprWithCtx) (i : Fin args.size) : MetaM (RefreshStep MetaM) := do + return .cont do + dbg_trace "cycled through expression {i}" + IO.sleep 1000 + Core.checkSystem "cycleSelections" + have : NeZero args.size := ⟨by cases i; grind⟩ + loop args (i + 1) + +@[widget_module] +def cycleComponent : Component PanelWidgetProps := + mk_rpc_widget% cycleSelections + +elab stx:"cycleSelections" : tactic => do + Widget.savePanelWidgetInfo (hash cycleComponent.javascript) (pure <| json% {}) stx + +-- show_panel_widgets [cycleComponent, cycleComponent] +example : 1 + 2 + 3 = 6 ^ 1 := by + cycleSelections -- place your cursor here and select some expressions + rfl +-- If you activate the widget multiple times, then thanks to the global cancel token ref, +-- all but one of the widget computations will say `This component was cancelled`. + + + +/-! Example 3: compute the fibonacci numbers from 400000 to 400040, in parallel, +and show the results as they come up. -/ + +def fibo (n : Nat) : Nat := Id.run do + let mut (a, b) := (0, 1) + for _ in 0...n do + (a, b) := (b, a + b) + return a + +structure FiboState where + pending : Array (Nat × Task Html) + results : Array (Nat × Html) := #[] + +def FiboState.update (s : FiboState) : BaseIO FiboState := do + let mut results := s.results + let mut pending := #[] + for (n, t) in s.pending do + if ← IO.hasFinished t then + results := results.push (n, t.get) + else + pending := pending.push (n, t) + results := results.insertionSort (·.1 < ·.1) + return { results, pending } + +def FiboState.render (s : FiboState) (t : Option Nat := none) : Html := + let header := match t with + | some t => s!"Finished in {t}ms" + | none => "Computing Fibonacci numbers ⏳"; +
+ + {.text header} + + {Html.element "ul" #[("style", json% { "padding-left" : "30px"})] (s.results.map (·.2))} +
+ +def generateFibo (n : Nat) : Html := +
  • {.text s!"the {n}-th Fibonacci number has {(fibo n).log2} binary digits."}
    • + +partial def FiboWidget : CoreM Html := do + mkRefreshComponentM (.text "loading...") do + IO.sleep 1 -- If we don't wait 1ms first, the infoview lags too much. + let pending := (400000...=400040).toArray.map fun n => (n, Task.spawn fun _ => generateFibo n) + let t0 ← IO.monoMsNow + loop t0 { pending } +where + loop (t0 : Nat) (s : FiboState) : CoreM (RefreshStep CoreM) := do + Core.checkSystem "FiboWidget" + while !(← s.pending.anyM (IO.hasFinished ·.2)) do + IO.sleep 10 + Core.checkSystem "FiboWidget" + let s ← s.update + if s.pending.isEmpty then + return .last <| s.render ((← IO.monoMsNow) - t0) + else + return .cont s.render (loop t0 s) + +-- #html FiboWidget diff --git a/ProofWidgets/Util.lean b/ProofWidgets/Util.lean index ecfab89..fdea292 100644 --- a/ProofWidgets/Util.lean +++ b/ProofWidgets/Util.lean @@ -1,8 +1,8 @@ /- - Copyright (c) 2024 Eric Wieser. All rights reserved. - Released under Apache 2.0 license as described in the file LICENSE. - Authors: Eric Wieser - -/ +Copyright (c) 2024 Eric Wieser. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: Eric Wieser, Jovan Gerbscheid +-/ module public meta import Lean.PrettyPrinter.Delaborator.Basic @@ -72,3 +72,36 @@ def withAnnotateTermLikeInfo (d : DelabM (TSyntax n)) : DelabM (TSyntax n) := do annotateTermLikeInfo stx end Lean.PrettyPrinter.Delaborator + +section MonadDrop + +/-- +The class `MonadDrop m n` allows a computation in monad `m` to be run in monad `n`. +For example, a `MetaM` computation can be ran in `EIO Exception`, +which can then be ran as a task using `EIO.asTask`. +-/ +class MonadDrop (m : Type → Type) (n : outParam <| Type → Type) where + /-- Translates an action from monad `m` into monad `n`. -/ + dropM {α} : m α → m (n α) + +export MonadDrop (dropM) + +variable {m n : Type → Type} [Monad m] [MonadDrop m n] + +instance : MonadDrop m m where + dropM := pure + +instance {ρ} : MonadDrop (ReaderT ρ m) n where + dropM act := fun ctx => dropM (act ctx) + +instance {σ} : MonadDrop (StateT σ m) n where + dropM act := do liftM <| dropM <| act.run' (← get) + +instance {ω σ} [MonadLiftT (ST ω) m] : MonadDrop (StateRefT' ω σ m) n where + dropM act := do liftM <| dropM <| act.run' (← get) + +end MonadDrop + +instance : Lean.Server.RpcEncodable Unit where + rpcEncode _ := pure .null + rpcDecode _ := pure () diff --git a/widget/src/RefreshComponent.tsx b/widget/src/RefreshComponent.tsx new file mode 100644 index 0000000..066f592 --- /dev/null +++ b/widget/src/RefreshComponent.tsx @@ -0,0 +1,66 @@ +/* +Copyright (c) 2025 Jovan Gerbscheid. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: Jovan Gerbscheid +*/ +import React from "react"; +import { useRpcSession, RpcPtr } from "@leanprover/infoview"; +import HtmlDisplay, { Html } from './htmlDisplay'; + +/** The arguments passed to a `RefreshComponent` */ +interface RefreshComponentProps { + /** The ref to the refresh state of the HTML display */ + state : RpcPtr<'RefreshRef'> + /** A cancel token that will cancel the refresh computation */ + cancelTk? : RpcPtr<'IO.CancelToken'> +} + +interface RequestProps { + state : RpcPtr<'RefreshRef'> + oldIdx : number +} + +interface ResultProps { + /** The new HTML to display */ + html : Html + idx : number +} + +export default function RefreshComponent(props: RefreshComponentProps): JSX.Element { + const rs = useRpcSession() + const [html, setHtml] = React.useState(null) + + // Repeatedly call Lean to update + React.useEffect(() => { + let cancelled = false + async function loop(idx: number) { + const result = await rs.call( + "ProofWidgets.RefreshComponent.awaitRefresh", { oldIdx: idx, state: props.state }) + if (cancelled || !result) return + setHtml(result.html) + return loop(result.idx) + } + (async () => { + // Set the HTML to the current value at the start of each re-render + const result = await rs.call, ResultProps>( + "ProofWidgets.RefreshComponent.getCurrState", props.state) + if (cancelled) return + setHtml(result.html) + // And then repeatedly refresh the HTML + return loop(result.idx) + })() + return () => { + cancelled = true + if (props.cancelTk) { + rs.call, void>( + "ProofWidgets.RefreshComponent.cancelRefresh", props.cancelTk) + } + } + // React checks if `props` has changed using pointer equality. + // We claim that here this is equivalent to deep equality of the objects. + // This is because whenever a new `props` is created, this is done by Lean + // in a way that creates fresh `RpcPtr`s. + }, [props]) + // For the short time that `html` doesn't have a value yet, we return the empty HTML. + return html ? : <> +}