chore: move to v4.8.0-rc1

ProofWidgets/Data/Html.lean

@@ -156,14 +156,14 @@ partial def delabHtmlElement' : DelabM (TSyntax `jsxElement) := do
   let_expr Html.element tag _attrs _children := ← getExpr | failure
 
   let .lit (.strVal s) := tag | failure
-  let tag ← withNaryArg 0 <| annotateTermLikeInfo <| mkIdent s
+  let tag ← withNaryArg 0 <| annotateTermLikeInfo <| mkIdent <| .mkSimple s
 
   let attrs ← withNaryArg 1 <|
     try
       delabArrayLiteral <| withAnnotateTermLikeInfo do
         let_expr Prod.mk _ _ a _ := ← getExpr | failure
         let .lit (.strVal a) := a | failure
-        let attr ← withNaryArg 2 <| annotateTermLikeInfo <| mkIdent a
+        let attr ← withNaryArg 2 <| annotateTermLikeInfo <| mkIdent <| .mkSimple a
         withNaryArg 3 do
           let v ← getExpr
           -- If the attribute's value is a string literal,

ProofWidgets/Demos/Euclidean.lean

@@ -245,7 +245,7 @@ def EuclideanConstructions.rpc (props : PanelWidgetProps) : RequestM (RequestTas
           -- Find which hypotheses are selected.
           let selectedHyps ← props.selectedLocations.filterMapM fun
             | ⟨mv, .hyp fv⟩ | ⟨mv, .hypType fv _⟩ =>
-              return if mv == g.mvarId then some (← fv.getDecl) else none
+              if mv == g.mvarId then return some (← fv.getDecl) else return none
             | _ =>
               return none
 

ProofWidgets/Demos/Venn.lean

@@ -99,7 +99,7 @@ def VennDisplay.rpc (props : PanelWidgetProps) : RequestM (RequestTask Html) :=
         Meta.withLCtx lctx md.localInstances do
           let locs : Array LocalDecl ← props.selectedLocations.filterMapM fun
             | ⟨mv, .hyp fv⟩ | ⟨mv, .hypType fv _⟩ =>
-              return if mv == g.mvarId then some (← fv.getDecl) else none
+              if mv == g.mvarId then return some (← fv.getDecl) else return none
             | _ => return none
           match ← isSetGoal? locs with
           | some html => return html

lake-manifest.json

@@ -4,10 +4,10 @@
  [{"url": "https://github.com/leanprover/std4",
    "type": "git",
    "subDir": null,
-   "rev": "32983874c1b897d78f20d620fe92fc8fd3f06c3a",
+   "rev": "9fab3b45b6def355de20550141354cea24396224",
    "name": "std",
    "manifestFile": "lake-manifest.json",
-   "inputRev": "v4.7.0",
+   "inputRev": "nightly-testing",
    "inherited": false,
    "configFile": "lakefile.lean"}],
  "name": "proofwidgets",

lakefile.lean

@@ -10,7 +10,7 @@ lean_lib ProofWidgets
 lean_lib ProofWidgets.Demos where
   globs := #[.submodules `ProofWidgets.Demos]
 
-require std from git "https://github.com/leanprover/std4" @ "v4.7.0"
+require std from git "https://github.com/leanprover/std4" @ "main"
 
 def npmCmd : String :=
   if Platform.isWindows then "npm.cmd" else "npm"
@@ -32,7 +32,7 @@ target widgetPackageLock : FilePath := do
 Rebuilds whenever the `.tsx` source, or any part of the build configuration, has changed. -/
 def widgetTsxTarget (pkg : NPackage _package.name) (nodeModulesMutex : IO.Mutex Bool)
     (tsxName : String) (deps : Array (BuildJob FilePath)) (isDev : Bool) :
-    IndexBuildM (BuildJob FilePath) := do
+    FetchM (BuildJob FilePath) := do
   let jsFile := pkg.buildDir / "js" / s!"{tsxName}.js"
   buildFileAfterDepArray jsFile deps fun _srcFile => do
     /-
@@ -67,7 +67,7 @@ def widgetTsxTarget (pkg : NPackage _package.name) (nodeModulesMutex : IO.Mutex
 
 /-- Target to build all TypeScript widget modules that match `widget/src/*.tsx`. -/
 def widgetJsAllTarget (pkg : NPackage _package.name) (isDev : Bool) :
-    IndexBuildM (BuildJob (Array FilePath)) := do
+    FetchM (BuildJob (Array FilePath)) := do
   let fs ← (widgetDir / "src").readDir
   let tsxs : Array FilePath := fs.filterMap fun f =>
     let p := f.path; if let some "tsx" := p.extension then some p else none

lean-toolchain

@@ -1 +1 @@
-leanprover/lean4:v4.7.0
+leanprover/lean4:v4.8.0-rc1