feat: add ProofWidgets.Demos target and make the tests pass (#38)

* feat: add ProofWidgets.Demos target and make the tests pass

* Apply suggestions from code review

Co-authored-by: Wojciech Nawrocki <[email protected]>

---------

Co-authored-by: Wojciech Nawrocki <[email protected]>

.github/workflows/build.yml

@@ -52,6 +52,9 @@ jobs:
       - name: Build package
         run: lake build ProofWidgets
 
+      - name: Build demos
+        run: lake build ProofWidgets.Demos
+
       - name: Create release for tag
         if: github.ref_type == 'tag'
         uses: softprops/action-gh-release@v1

ProofWidgets/Demos/Conv.lean

@@ -430,6 +430,9 @@ def ConvPanel : Component PanelWidgetProps :=
 
 /-! # Example usage -/
 
+-- Like `sorry` but avoids a warning for demonstration purposes.
+axiom test_sorry {α} : α
+
 example [Add α] [Neg α] [OfNat α (nat_lit 0)]
     (h₁ : ∀ (a : α), a + 0 = a)
     (h₂ : ∀ (a b c : α), (a + b) + c = a + (b + c))
@@ -444,3 +447,5 @@ by with_panel_widgets [ConvPanel]
   rw [← h₂]
   conv =>
     -- Place your cursor in the `conv` block
+    skip
+  exact test_sorry

ProofWidgets/Demos/Euclidean.lean

@@ -267,8 +267,10 @@ def EuclideanConstructions.rpc (props : PanelWidgetProps) : RequestM (RequestTas
 def EuclideanConstructions : Component PanelWidgetProps :=
   mk_rpc_widget% EuclideanConstructions.rpc
 
-example {a b c d : Point} : ∃ L, onLine a L ∧ onLine b L := by
+axiom test_sorry {α} : α
+
+example {a b _c _d : Point} : ∃ L, onLine a L ∧ onLine b L := by
   with_panel_widgets [EuclideanConstructions]
     -- Place your cursor below.
 
-    sorry
+    exact test_sorry

ProofWidgets/Demos/ExprPresentation.lean

@@ -19,7 +19,7 @@ example : 2 + 2 = 4 ∧ 3 + 3 = 6 := by
     rfl
     rfl
 
-example (h : 2 + 2 = 5) : 2 + 2 = 4 := by
+example (_h : 2 + 2 = 5) : 2 + 2 = 4 := by
   with_panel_widgets [SelectionPanel]
     -- Place cursor here and select subexpressions in the goal with shift-click.
     rfl

ProofWidgets/Demos/InteractiveSvg.lean

@@ -16,12 +16,12 @@ def isvg : InteractiveSvg State where
       width := 400
       height := 400 }
 
-  update time Δt action mouseStart mouseEnd selected getData state :=
+  update _time _Δt _action _mouseStart mouseEnd _selected getData state :=
     match getData Nat, mouseEnd with
     | some id, some p => state.set! id p.toAbsolute
     | _, _ => state
 
-  render time mouseStart mouseEnd state :=
+  render _time mouseStart mouseEnd state :=
     {
       elements :=
         let mousePointer :=

ProofWidgets/Demos/LazyComputation.lean

@@ -14,9 +14,8 @@ structure MetaMStringCont where
 structure RunnerWidgetProps where
   /-- A continuation to run and print the results of when the button is clicked. -/
   k : WithRpcRef MetaMStringCont
-
--- Make it possible for widgets to receive `RunnerWidgetProps`. Uses the `TypeName` instance.
-#mkrpcenc RunnerWidgetProps
+  -- Make it possible for widgets to receive `RunnerWidgetProps`. Uses the `TypeName` instance.
+  deriving RpcEncodable
 
 @[server_rpc_method]
 def runMetaMStringCont : RunnerWidgetProps → RequestM (RequestTask String)
@@ -56,7 +55,7 @@ syntax (name := makeRunnerTac) "make_runner" : tactic
         k := x
       }⟩}
     -- Save a widget together with a pointer to `props`.
-    savePanelWidgetInfo tk ``runnerWidget (rpcEncode props)
+    Widget.savePanelWidgetInfo runnerWidget.javascriptHash (rpcEncode props) tk
   | _ => throwUnsupportedSyntax
 
 example : True := by

ProofWidgets/Demos/Plot.lean

@@ -33,8 +33,7 @@ def mkFrames (fn : Float → Float → Float) (steps := 100) : Array Html:=
 structure AnimatedHtmlProps where
   frames : Array Html
   framesPerSecond? : Option Nat := none
-
-#mkrpcenc AnimatedHtmlProps
+  deriving Server.RpcEncodable
 
 @[widget_module]
 def AnimatedHtml : Component AnimatedHtmlProps where

ProofWidgets/Demos/RbTree.lean

@@ -86,15 +86,13 @@ inductive RBTreeVars where
   | empty : RBTreeVars
   | var : CodeWithInfos → RBTreeVars
   | node (color : RBTreeVarsColour) (l : RBTreeVars) (a : CodeWithInfos) (r : RBTreeVars) : RBTreeVars
-
-#mkrpcenc RBTreeVars
+  deriving Server.RpcEncodable
 
 /-! # `Expr` presenter to display red-black trees -/
 
 structure RBDisplayProps where
   tree : RBTreeVars
-
-#mkrpcenc RBDisplayProps
+  deriving Server.RpcEncodable
 
 open ProofWidgets
 

ProofWidgets/Demos/SelectInsertConv.lean

@@ -5,6 +5,7 @@ Authors: Robin Böhne, Wojciech Nawrocki, Patrick Massot
 -/
 import Lean.Meta.ExprLens
 import Std.Lean.Position
+import Std.Data.Json
 import ProofWidgets.Data.Html
 import ProofWidgets.Component.OfRpcMethod
 import ProofWidgets.Component.MakeEditLink
@@ -151,9 +152,13 @@ def ConvSelectionPanel : Component ConvSelectionPanelProps :=
 open scoped Json in
 elab stx:"conv?" : tactic => do
   let some replaceRange := (← getFileMap).rangeOfStx? stx | return
-  savePanelWidgetInfo stx ``ConvSelectionPanel $ pure $ json% { replaceRange: $(replaceRange) }
+  Widget.savePanelWidgetInfo ConvSelectionPanel.javascriptHash
+    (pure $ json% { replaceRange: $(replaceRange) }) stx
+
+-- Like `sorry` but avoids a warning for demonstration purposes.
+axiom test_sorry {α} : α
 
 example (a : Nat) : a + a - a + a = a := by
   conv?
   -- Put your cursor on the next line
-  all_goals { sorry }
+  all_goals exact test_sorry

lakefile.lean

@@ -6,6 +6,9 @@ package proofwidgets where
 
 lean_lib ProofWidgets
 
+lean_lib ProofWidgets.Demos where
+  globs := #[.submodules `ProofWidgets.Demos]
+
 require std from git "https://github.com/leanprover/std4" @ "main"
 
 def npmCmd : String :=