Merge pull request #108 from leanprover-community/bump_to_v4.18.0-rc1

chore: bump toolchain to v4.18.0-rc1

ProofWidgets/Cancellable.lean

@@ -34,9 +34,9 @@ def mkCancellable [RpcEncodable β] (handler : α → RequestM (RequestTask β))
     α → RequestM (RequestTask RequestId) := fun a => do
   RequestM.asTask do
     let t ← handler a
-    let t' := t.map (·.map rpcEncode)
+    let t' := t.mapCheap (·.map rpcEncode)
     runningRequests.modifyGet fun (id, m) =>
-      (id, (id+1, m.insert id ⟨t', IO.cancel t⟩))
+      (id, (id+1, m.insert id ⟨t'.task, t.cancel⟩))
 
 /-- Cancel the request with ID `rid`.
 Does nothing if `rid` is invalid. -/

lake-manifest.json

@@ -5,10 +5,10 @@
    "type": "git",
    "subDir": null,
    "scope": "leanprover-community",
-   "rev": "efcc7d9bd9936ecdc625baf0d033b60866565cd5",
+   "rev": "092b30de8e7ee78e96b24c235d99e26f2942d77e",
    "name": "batteries",
    "manifestFile": "lake-manifest.json",
-   "inputRev": "v4.17.0",
+   "inputRev": "v4.18.0-rc1",
    "inherited": false,
    "configFile": "lakefile.toml"}],
  "name": "proofwidgets",

lakefile.lean

@@ -6,7 +6,7 @@ package proofwidgets where
   buildArchive? := "ProofWidgets4.tar.gz"
   releaseRepo := "https://github.com/leanprover-community/ProofWidgets4"
 
-require "leanprover-community" / "batteries" @ git "v4.17.0"
+require "leanprover-community" / "batteries" @ git "v4.18.0-rc1"
 
 def npmCmd : String :=
   if Platform.isWindows then "npm.cmd" else "npm"

lean-toolchain

@@ -1 +1 @@
-leanprover/lean4:v4.17.0
+leanprover/lean4:v4.18.0-rc1