Merge pull request #78 from leanprover-community/bump/v4.12.0

chore: merge bump/v4.12.0 and move toolchain to v4.12.0-rc1

ProofWidgets/Cancellable.lean

@@ -1,5 +1,6 @@
 import Lean.Data.Json.FromToJson
 import Lean.Server.Rpc.RequestHandling
+import Std.Data.HashMap
 import ProofWidgets.Compat
 
 /-! Experimental support for cancellable RPC requests.
@@ -9,7 +10,7 @@ and the requests map should be stored in `RequestM`,
 or somewhere in the server anyway. -/
 
 namespace ProofWidgets
-open Lean Server Meta
+open Lean Server Meta Std
 
 abbrev RequestId := Nat
 structure CancellableTask where
@@ -20,8 +21,8 @@ structure CancellableTask where
 
 /-- Maps the ID of each currently executing request to its task. -/
 initialize runningRequests :
-    IO.Ref (RequestId × HashMap RequestId CancellableTask) ←
-  IO.mkRef (0, HashMap.empty)
+    IO.Ref (RequestId × Std.HashMap RequestId CancellableTask) ←
+  IO.mkRef (0, Std.HashMap.empty)
 
 /-- Transforms a request handler returning `β`
 into one that returns immediately with a `RequestId`.
@@ -42,7 +43,7 @@ Does nothing if `rid` is invalid. -/
 @[server_rpc_method]
 def cancelRequest (rid : RequestId) : RequestM (RequestTask String) := do
   RequestM.asTask do
-    let t? ← runningRequests.modifyGet fun (id, m) => (m.find? rid, (id, m.erase rid))
+    let t? ← runningRequests.modifyGet fun (id, m) => (m[rid]?, (id, m.erase rid))
     if let some t := t? then
       t.cancel
     return "ok"
@@ -66,7 +67,7 @@ another possible addition to the RPC protocol? -/
 def checkRequest (rid : RequestId) : RequestM (RequestTask CheckRequestResponse) := do
   RequestM.asTask do
     let (_, m) ← runningRequests.get
-    match m.find? rid with
+    match m[rid]? with
     | none =>
       throw $ RequestError.invalidParams
         s!"Request '{rid}' has already finished, or the ID is invalid."

ProofWidgets/Component/InteractiveSvg.lean

@@ -1,7 +1,7 @@
 import ProofWidgets.Data.Svg
 
 namespace ProofWidgets
-open Lean
+open Lean Std
 
 private def _root_.Float.toInt (x : Float) : Int :=
   if x >= 0 then
@@ -67,15 +67,15 @@ def InteractiveSvg.serverRpcMethod {State : Type} (isvg : InteractiveSvg State)
   -- right now we just assume that all actions are uqually spaced within the frame
   let Δt := (params.elapsed - params.state.time) / params.actions.size.toFloat
 
-  let idToData : HashMap String Json := HashMap.ofList params.state.idToData
+  let idToData : Std.HashMap String Json := HashMap.ofList params.state.idToData
 
   let mut time := params.state.time
   let mut state := params.state.state
   let mut selected := params.state.selected
 
   let getData := λ (α : Type) [FromJson α] => do
     let id ← selected;
-    let data ← idToData[id]
+    let data ← idToData[id]?
     match fromJson? (α:=α) data with
     | .error _ => none
     | .ok val => some val
@@ -111,7 +111,7 @@ def InteractiveSvg.serverRpcMethod {State : Type} (isvg : InteractiveSvg State)
 
   -- highlight selection
   if let some id := selected then
-    if let some idx := svg.idToIdx[id] then
+    if let some idx := svg.idToIdx[id]? then
       svg := { elements := svg.elements.modify idx λ e => e.setStroke (1.,1.,0.) (.px 5) }
 
 

ProofWidgets/Component/PenroseDiagram.lean

@@ -1,8 +1,9 @@
 import ProofWidgets.Component.Basic
 import ProofWidgets.Data.Html
+import Std.Data.HashMap
 
 namespace ProofWidgets.Penrose
-open Lean Server
+open Lean Server Std
 
 structure DiagramProps where
   embeds      : Array (String × Html)
@@ -49,7 +50,7 @@ structure DiagramState where
   sub : String := ""
   /-- Components to display as labels in the diagram,
   stored in the map as name ↦ (type, html). -/
-  embeds : HashMap String (String × Html) := .empty
+  embeds : Std.HashMap String (String × Html) := .empty
 
 /-- A monad to easily build Penrose diagrams in. -/
 abbrev DiagramBuilderM := StateT DiagramState MetaM

ProofWidgets/Data/Svg.lean

@@ -1,7 +1,8 @@
 import ProofWidgets.Data.Html
+import Std.Data.HashMap
 
 namespace ProofWidgets
-open Lean
+open Lean Std
 
 private def _root_.Float.toInt (x : Float) : Int :=
   if x >= 0 then
@@ -155,12 +156,12 @@ def polygon {f} (pts : Array (Point f)) : Element f := { shape := .polygon pts }
 
 end Svg
 
-def mkIdToIdx {f} (elements : Array (Svg.Element f)) : HashMap String (Fin elements.size) :=
+def mkIdToIdx {f} (elements : Array (Svg.Element f)) : Std.HashMap String (Fin elements.size) :=
   let idToIdx := (elements
     |>.mapIdx (λ idx el => (idx,el))) -- zip with index
     |>.filterMap (λ (idx,el) => el.id.map (λ id => (id,idx))) -- keep only elements with specified id
     |>.toList
-    |> HashMap.ofList
+    |> Std.HashMap.ofList
   idToIdx
 
 structure Svg (f : Svg.Frame) where
@@ -183,14 +184,14 @@ def idToDataList {f} (svg : Svg f) : List (String × Json) :=
     | some id, some data => (id,data)::l
     | _, _ => l)
 
-def idToData {f} (svg : Svg f) : HashMap String Json :=
+def idToData {f} (svg : Svg f) : Std.HashMap String Json :=
   HashMap.ofList svg.idToDataList
 
 instance {f} : GetElem (Svg f) Nat (Svg.Element f) (λ svg idx => idx < svg.elements.size) where
   getElem svg i h := svg.elements[i]
 
 instance {f} : GetElem (Svg f) String (Option (Svg.Element f)) (λ _ _ => True) where
-  getElem svg id _ := svg.idToIdx[id].map (λ idx => svg.elements[idx])
+  getElem svg id _ := svg.idToIdx[id]?.map (λ idx => svg.elements[idx])
 
 def getData {f} (svg : Svg f) (id : String) : Option Json :=
   match svg[id] with

lake-manifest.json

@@ -5,7 +5,7 @@
    "type": "git",
    "subDir": null,
    "scope": "",
-   "rev": "9c6c2d647e57b2b7a0b42dd8080c698bd33a1b6f",
+   "rev": "fa571ea02a804b52a59e58012b1e21fe4f0514f2",
    "name": "batteries",
    "manifestFile": "lake-manifest.json",
    "inputRev": "main",