feat: adaptations for leanprover/lean4#2964

Mathlib/Data/List/Join.lean

@@ -52,7 +52,7 @@ theorem join_filter_isEmpty_eq_false [DecidablePred fun l : List α => l.isEmpty
   | [] :: L => by
       simp [join_filter_isEmpty_eq_false (L := L), isEmpty_iff_eq_nil]
   | (a :: l) :: L => by
-      simp [join_filter_isEmpty_eq_false (L := L), isEmpty_cons]
+      simp [join_filter_isEmpty_eq_false (L := L)]
 #align list.join_filter_empty_eq_ff List.join_filter_isEmpty_eq_false
 
 @[simp]

Mathlib/RingTheory/Localization/Basic.lean

@@ -811,17 +811,17 @@ theorem isLocalization_iff_of_algEquiv [Algebra R P] (h : S ≃ₐ[R] P) :
 #align is_localization.is_localization_iff_of_alg_equiv IsLocalization.isLocalization_iff_of_algEquiv
 
 theorem isLocalization_iff_of_ringEquiv (h : S ≃+* P) :
-    IsLocalization M S ↔
-      haveI := (h.toRingHom.comp <| algebraMap R S).toAlgebra; IsLocalization M P :=
+    IsLocalization M S ↔ haveI := (h.toRingHom.comp <| algebraMap R S).toAlgebra;
+      IsLocalization M P :=
   letI := (h.toRingHom.comp <| algebraMap R S).toAlgebra
   isLocalization_iff_of_algEquiv M { h with commutes' := fun _ => rfl }
 #align is_localization.is_localization_iff_of_ring_equiv IsLocalization.isLocalization_iff_of_ringEquiv
 
 variable (S)
 
 theorem isLocalization_of_base_ringEquiv [IsLocalization M S] (h : R ≃+* P) :
-    haveI := ((algebraMap R S).comp h.symm.toRingHom).toAlgebra
-    IsLocalization (M.map h.toMonoidHom) S := by
+    haveI := ((algebraMap R S).comp h.symm.toRingHom).toAlgebra;
+      IsLocalization (M.map h.toMonoidHom) S := by
   letI : Algebra P S := ((algebraMap R S).comp h.symm.toRingHom).toAlgebra
   constructor
   · rintro ⟨_, ⟨y, hy, rfl⟩⟩

Mathlib/Tactic/Widget/Calc.lean

@@ -54,7 +54,7 @@ structure CalcParams extends SelectInsertParams where
   isFirst : Bool
   /-- indentation level of the calc block. -/
   indent : Nat
-  deriving SelectInsertParamsClass, RpcEncodable
+  deriving SelectInsertParamsClass, ToJson, FromJson
 
 open Lean Meta
 
@@ -118,7 +118,7 @@ def CalcPanel.rpc := mkSelectionPanelRPC suggestSteps
 
 /-- The calc widget. -/
 @[widget_module]
-def CalcPanel : Component CalcParams :=
+def CalcPanel : PanelWidget CalcParams :=
   mk_rpc_widget% CalcPanel.rpc
 
 namespace Lean.Elab.Tactic
@@ -134,9 +134,6 @@ elab_rules : tactic
   for step in ← Lean.Elab.Term.getCalcSteps steps do
     let some replaceRange := (← getFileMap).rangeOfStx? step | unreachable!
     let `(calcStep| $(_) := $proofTerm) := step | unreachable!
-    let json := open scoped Std.Json in json% {"replaceRange": $(replaceRange),
-                                                        "isFirst": $(isFirst),
-                                                        "indent": $(indent)}
-    ProofWidgets.savePanelWidgetInfo proofTerm `CalcPanel (pure json)
+    savePanelWidgetInfo' CalcPanel { replaceRange, isFirst, indent } proofTerm
     isFirst := false
   evalCalc (← `(tactic|calc%$calcstx $stx))

Mathlib/Tactic/Widget/Congrm.lean

@@ -43,12 +43,12 @@ def CongrmSelectionPanel.rpc := mkSelectionPanelRPC makeCongrmString
 
 /-- The congrm widget. -/
 @[widget_module]
-def CongrmSelectionPanel : Component SelectInsertParams :=
+def CongrmSelectionPanel : PanelWidget SelectInsertParams :=
   mk_rpc_widget% CongrmSelectionPanel.rpc
 
 open scoped Json in
 /-- Display a widget panel allowing to generate a `congrm` call with holes specified by selecting
 subexpressions in the goal.-/
 elab stx:"congrm?" : tactic => do
   let some replaceRange := (← getFileMap).rangeOfStx? stx | return
-  savePanelWidgetInfo stx ``CongrmSelectionPanel $ pure $ json% { replaceRange: $(replaceRange) }
+  savePanelWidgetInfo' CongrmSelectionPanel { replaceRange } stx

Mathlib/Tactic/Widget/Conv.lean

@@ -125,12 +125,12 @@ mkSelectionPanelRPC insertEnter
 
 /-- The conv widget. -/
 @[widget_module]
-def ConvSelectionPanel : Component SelectInsertParams :=
+def ConvSelectionPanel : PanelWidget SelectInsertParams :=
   mk_rpc_widget% ConvSelectionPanel.rpc
 
 open scoped Json in
 /-- Display a widget panel allowing to generate a `conv` call zooming to the subexpression selected
 in the goal.-/
 elab stx:"conv?" : tactic => do
   let some replaceRange := (← getFileMap).rangeOfStx? stx | return
-  savePanelWidgetInfo stx ``ConvSelectionPanel $ pure $ json% { replaceRange: $(replaceRange) }
+  savePanelWidgetInfo' ConvSelectionPanel { replaceRange } stx

Mathlib/Tactic/Widget/Gcongr.lean

@@ -41,12 +41,12 @@ def GCongrSelectionPanel.rpc := mkSelectionPanelRPC makeGCongrString
 
 /-- The gcongr widget. -/
 @[widget_module]
-def GCongrSelectionPanel : Component SelectInsertParams :=
+def GCongrSelectionPanel : PanelWidget SelectInsertParams :=
   mk_rpc_widget% GCongrSelectionPanel.rpc
 
 open scoped Json in
 /-- Display a widget panel allowing to generate a `gcongr` call with holes specified by selecting
 subexpressions in the goal.-/
 elab stx:"gcongr?" : tactic => do
   let some replaceRange := (← getFileMap).rangeOfStx? stx | return
-  savePanelWidgetInfo stx ``GCongrSelectionPanel $ pure $ json% { replaceRange: $(replaceRange) }
+  savePanelWidgetInfo' GCongrSelectionPanel { replaceRange } stx

Mathlib/Tactic/Widget/SelectInsertParamsClass.lean

@@ -17,12 +17,6 @@ open Lean Meta Server
 
 /-- Structures providing parameters for a Select and insert widget. -/
 class SelectInsertParamsClass (α : Type) where
-  /-- Cursor position in the file at which the widget is being displayed. -/
-  pos : α → Lsp.Position
-  /-- The current tactic-mode goals. -/
-  goals : α → Array Widget.InteractiveGoal
-  /-- Locations currently selected in the goal state. -/
-  selectedLocations : α → Array SubExpr.GoalsLocation
   /-- The range in the source document where the command will be inserted. -/
   replaceRange : α → Lsp.Range
 
@@ -31,8 +25,7 @@ open Command Meta Parser Term
 
 private def mkSelectInsertParamsInstance (declName : Name) : TermElabM Syntax.Command :=
   `(command|instance : SelectInsertParamsClass (@$(mkCIdent declName)) :=
-    ⟨fun prop => prop.pos, fun prop => prop.goals,
-     fun prop => prop.selectedLocations, fun prop => prop.replaceRange⟩)
+    ⟨fun prop => prop.replaceRange⟩)
 
 /-- Handler deriving a `SelectInsertParamsClass` instance. -/
 def mkSelectInsertParamsInstanceHandler (declNames : Array Name) : CommandElabM Bool := do

Mathlib/Tactic/Widget/SelectPanelUtils.lean

@@ -9,6 +9,7 @@ import Std.Data.Nat.Init.Lemmas
 
 import ProofWidgets.Component.MakeEditLink
 import ProofWidgets.Component.OfRpcMethod -- needed in all files using this one.
+import ProofWidgets.Component.Panel.Basic
 
 import Mathlib.Tactic.Widget.SelectInsertParamsClass
 
@@ -47,15 +48,9 @@ open ProofWidgets
 
 /-- Structures providing parameters for a Select and insert widget. -/
 structure SelectInsertParams where
-  /-- Cursor position in the file at which the widget is being displayed. -/
-  pos : Lsp.Position
-  /-- The current tactic-mode goals. -/
-  goals : Array Widget.InteractiveGoal
-  /-- Locations currently selected in the goal state. -/
-  selectedLocations : Array SubExpr.GoalsLocation
   /-- The range in the source document where the command will be inserted. -/
   replaceRange : Lsp.Range
-  deriving SelectInsertParamsClass, RpcEncodable
+  deriving ToJson, FromJson, SelectInsertParamsClass
 
 open scoped Jsx in open SelectInsertParamsClass Lean.SubExpr in
 /-- Helper function to create a widget allowing to select parts of the main goal
@@ -78,41 +73,41 @@ We also make sure `mkCmdStr` is executed in the right context.
  -/
 def mkSelectionPanelRPC {Params : Type} [SelectInsertParamsClass Params]
     (mkCmdStr : (pos : Array GoalsLocation) → (goalType : Expr) → Params →
-   MetaM (String × String × Option (String.Pos × String.Pos)))
-  (helpMsg : String) (title : String) (onlyGoal := true) (onlyOne := false) :
-  (params : Params) → RequestM (RequestTask Html) :=
-fun params ↦ RequestM.asTask do
-let doc ← RequestM.readDoc
-if h : 0 < (goals params).size then
-  let mainGoal := (goals params)[0]
-  let mainGoalName := mainGoal.mvarId.name
-  let all := if onlyOne then "The selected sub-expression" else "All selected sub-expressions"
-  let be_where := if onlyGoal then "in the main goal." else "in the main goal or its context."
-  let errorMsg := s!"{all} should be {be_where}"
-  let inner : Html ← (do
-    if onlyOne && (selectedLocations params).size > 1 then
-      return <span>{.text "You should select only one sub-expression"}</span>
-    for selectedLocation in selectedLocations params do
-      if selectedLocation.mvarId.name != mainGoalName then
-        return <span>{.text errorMsg}</span>
-      else if onlyGoal then
-        if !(selectedLocation.loc matches (.target _)) then
-          return <span>{.text errorMsg}</span>
-    if (selectedLocations params).isEmpty then
-      return <span>{.text helpMsg}</span>
-    mainGoal.ctx.val.runMetaM {} do
-      let md ← mainGoal.mvarId.getDecl
-      let lctx := md.lctx |>.sanitizeNames.run' {options := (← getOptions)}
-      Meta.withLCtx lctx md.localInstances do
-        let (linkText, newCode, range?) ← mkCmdStr (selectedLocations params) md.type.consumeMData
-          params
-        return .ofComponent
-          MakeEditLink
-          (.ofReplaceRange doc.meta (replaceRange params) newCode range?)
-          #[ .text linkText ])
-  return <details «open»={true}>
-      <summary className="mv2 pointer">{.text title}</summary>
-      <div className="ml1">{inner}</div>
-    </details>
-else
-  return <span>{.text "There is no goal to solve!"}</span> -- This shouldn't happen.
+    MetaM (String × String × Option (String.Pos × String.Pos)))
+    (helpMsg : String) (title : String) (onlyGoal := true) (onlyOne := false) :
+    Params × PanelWidgetProps → RequestM (RequestTask Html) :=
+  fun (params, { goals, selectedLocations, .. }) ↦ RequestM.asTask do
+    let doc ← RequestM.readDoc
+    if h : 0 < goals.size then
+      let mainGoal := goals[0]
+      let mainGoalName := mainGoal.mvarId.name
+      let all := if onlyOne then "The selected sub-expression" else "All selected sub-expressions"
+      let be_where := if onlyGoal then "in the main goal." else "in the main goal or its context."
+      let errorMsg := s!"{all} should be {be_where}"
+      let inner : Html ← (do
+        if onlyOne && selectedLocations.size > 1 then
+          return <span>{.text "You should select only one sub-expression"}</span>
+        for selectedLocation in selectedLocations do
+          if selectedLocation.mvarId.name != mainGoalName then
+            return <span>{.text errorMsg}</span>
+          else if onlyGoal then
+            if !(selectedLocation.loc matches (.target _)) then
+              return <span>{.text errorMsg}</span>
+        if selectedLocations.isEmpty then
+          return <span>{.text helpMsg}</span>
+        mainGoal.ctx.val.runMetaM {} do
+          let md ← mainGoal.mvarId.getDecl
+          let lctx := md.lctx |>.sanitizeNames.run' {options := (← getOptions)}
+          Meta.withLCtx lctx md.localInstances do
+            let (linkText, newCode, range?) ← mkCmdStr selectedLocations md.type.consumeMData
+              params
+            return .ofComponent
+              MakeEditLink
+              (.ofReplaceRange doc.meta (replaceRange params) newCode range?)
+              #[ .text linkText ])
+      return <details «open»={true}>
+          <summary className="mv2 pointer">{.text title}</summary>
+          <div className="ml1">{inner}</div>
+        </details>
+    else
+      return <span>{.text "There is no goal to solve!"}</span> -- This shouldn't happen.

lake-manifest.json

@@ -4,10 +4,10 @@
  [{"url": "https://github.com/leanprover/std4",
    "type": "git",
    "subDir": null,
-   "rev": "49b36f282e56ce9a695923e2df156cd4abf33fc8",
+   "rev": "823a1f46a8c1e327b9fe5a205f0c01703dd33a28",
    "name": "std",
    "manifestFile": "lake-manifest.json",
-   "inputRev": "bump/v4.5.0",
+   "inputRev": "bump_bump",
    "inherited": false,
    "configFile": "lakefile.lean"},
   {"url": "https://github.com/leanprover-community/quote4",
@@ -31,10 +31,10 @@
   {"url": "https://github.com/leanprover-community/ProofWidgets4",
    "type": "git",
    "subDir": null,
-   "rev": "909febc72b4f64628f8d35cd0554f8a90b6e0749",
+   "rev": "4bc9cd80ba2d346d3af30e592e3aa22f437ed4cf",
    "name": "proofwidgets",
    "manifestFile": "lake-manifest.json",
-   "inputRev": "v0.0.23",
+   "inputRev": "v0.0.24-pre",
    "inherited": false,
    "configFile": "lakefile.lean"},
   {"url": "https://github.com/leanprover/lean4-cli",

lakefile.lean

@@ -26,10 +26,10 @@ package mathlib where
 meta if get_config? doc = some "on" then -- do not download and build doc-gen4 by default
 require «doc-gen4» from git "https://github.com/leanprover/doc-gen4" @ "main"
 
-require std from git "https://github.com/leanprover/std4" @ "bump/v4.5.0"
+require std from git "https://github.com/leanprover/std4" @ "bump_bump"
 require Qq from git "https://github.com/leanprover-community/quote4" @ "master"
 require aesop from git "https://github.com/leanprover-community/aesop" @ "master"
-require proofwidgets from git "https://github.com/leanprover-community/ProofWidgets4" @ "v0.0.23"
+require proofwidgets from git "https://github.com/leanprover-community/ProofWidgets4" @ "v0.0.24-pre"
 require Cli from git "https://github.com/leanprover/lean4-cli" @ "main"
 
 /-!

lean-toolchain

@@ -1 +1 @@
-leanprover/lean4:nightly-2023-12-19
+leanprover/lean4:nightly-2023-12-21

test/matrix.lean

@@ -1,7 +1,3 @@
-/-
-manually ported from
-https://github.com/leanprover-community/mathlib/blob/4f4a1c875d0baa92ab5d92f3fb1bb258ad9f3e5b/test/matrix.lean
--/
 import Mathlib.Data.Matrix.Notation
 import Mathlib.GroupTheory.Perm.Fin
 import Mathlib.LinearAlgebra.Matrix.Determinant