chore: update to latest Verso and fix deprecations

Main.lean

@@ -11,35 +11,32 @@ import Manual.ExtractExamples
 open Verso.Genre.Manual
 open Verso.Genre.Manual.InlineLean
 
-open Verso.Output.Html in
-def plausible := {{
+def plausible := html%{
     <script async src="https://plausible.io/js/pa-RTua_4FfKHhfAvAc3liZd.js"></script>
-    <script>{{.raw r#"
+    <script>{.raw r#"
       window.plausible=window.plausible||function(){(plausible.q=plausible.q||[]).push(arguments)},plausible.init=plausible.init||function(i){plausible.o=i||{}};
       plausible.init()
-    "#}}</script>
-  }}
+    "#}</script>
+  }
 
-open Verso.Output.Html in
-def staticJs := {{
+def staticJs := html%{
     <script src="static/metadata.js"></script>
     <script src="static/print.js"></script>
-    {{ if false then -- Flip this bit to test live links locally
-        {{ <script>"window.metadata = {'latest': true};"</script> }}
+    { if false then -- Flip this bit to test live links locally
+        html%{<script>{"window.metadata = {'latest': true};"}</script>}
       else
-        .empty }}
-  }}
+        .empty }
+  }
 
-open Verso.Output.Html in
-def staticCss := {{
+def staticCss := html%{
     <link rel="stylesheet" href="static/colors.css" />
     <link rel="stylesheet" href="static/theme.css" />
     <link rel="stylesheet" href="static/print.css" />
     <link rel="stylesheet" href="static/fonts/source-serif/source-serif-text.css" />
     <link rel="stylesheet" href="static/fonts/source-code-pro/source-code-pro.css" />
     <link rel="stylesheet" href="static/fonts/source-sans/source-sans-3.css" />
     <link rel="stylesheet" href="static/fonts/noto-sans-mono/noto-sans-mono.css" />
-  }}
+  }
 
 def main :=
   manualMain (%doc Manual) (config := config) (extraSteps := [extractExamples])

Manual/BasicTypes/Fin.lean

@@ -157,7 +157,7 @@ Heterogeneous operators such as {lean}`Fin.natAdd` do not have corresponding het
 
 ## Bitwise Operations
 
-Typically, bitwise operations on {name}`Fin` should be accessed using Lean's overloaded bitwise operators, particularly via the instances {inst}`ShiftLeft (Fin n)`, {inst}`ShiftRight (Fin n)`, {inst}`AndOp (Fin n)`, {inst}`OrOp (Fin n)`, {inst}`Xor (Fin n)`
+Typically, bitwise operations on {name}`Fin` should be accessed using Lean's overloaded bitwise operators, particularly via the instances {inst}`ShiftLeft (Fin n)`, {inst}`ShiftRight (Fin n)`, {inst}`AndOp (Fin n)`, {inst}`OrOp (Fin n)`, {inst}`XorOp (Fin n)`
 
 {docstring Fin.shiftLeft}
 

Manual/ErrorExplanations.lean

@@ -33,11 +33,11 @@ inline_extension Inline.errorExplanationShortName (errorName : Name) where
   extraCss := [".error-explanation-short-name { hyphenate-character: ''; }"]
   toTeX := none
   toHtml := some fun _go _id info _content =>
-    open Verso.Output Html in do
+    open Verso.Output in do
     let .ok (some errorName) := fromJson? (α := Option String) info
       | reportError "Invalid data for explanation name element"
         pure .empty
-    let html := {{ <code class="error-explanation-short-name">{{errorName}}</code> }}
+    let html := html%{<code class="error-explanation-short-name">{errorName}</code>}
     return html
 
 

Manual/IO/Async.lean

@@ -1198,6 +1198,8 @@ done
 :::leanSection
 ```lean -show
 open Std.Async.IO
+open Std (Channel Broadcast)
+variable {α : Type} [Inhabited α]
 ```
 The type classes {name}`AsyncRead`, {name}`AsyncWrite`, and {name}`AsyncStream` provide buffered asynchronous I/O.
 The main {name}`AsyncRead` instances are {inst}`AsyncRead (Channel α) α`, {inst}`AsyncRead (CloseableChannel α) (Option α)`, and {inst}`AsyncRead (Broadcast.Receiver α) (Option α)`.

Manual/Interaction/FormatRepr.lean

@@ -551,6 +551,11 @@ This precedence can be used to decide whether to insert parentheses: if the prec
 tag := "repr-instance-howto"
 %%%
 
+:::leanSection
+```lean -show
+open Std (HashSet)
+variable {α : Type} [BEq α] [Hashable α] [Repr α]
+```
 Lean can produce an appropriate {name}`Repr` instance for most types automatically using {ref "deriving-instances"}[instance deriving].
 In some cases, however, it's necessary to write an instance by hand:
 
@@ -565,6 +570,7 @@ In some cases, however, it's necessary to write an instance by hand:
 
 * The derived {name}`Repr` instance for structures uses {tech}[structure instance] notation.
   A hand-written instance can use the constructor's name explicitly or use {tech}[anonymous constructor syntax].
+:::
 
 ```lean -show -keep
 /-- info: Std.HashSet.ofList [0, 3, 5] -/

Manual/MVCGen.lean

@@ -24,7 +24,6 @@ set_option linter.unusedVariables false
 set_option linter.typography.quotes true
 set_option linter.typography.dashes true
 
-set_option mvcgen.warning false
 set_option linter.deprecated.syntax false
 
 open Manual (comment)
@@ -131,7 +130,6 @@ import Std.Tactic.Do
 ```lean -show
 open Std.Do
 
-set_option mvcgen.warning false
 set_option linter.deprecated.syntax false
 
 ```
@@ -395,8 +393,8 @@ The function must be {deftech (key := "mvcgen conjunctive")}_conjunctive_, which
 ```lean -show
 variable {σ : List (Type u)} {ps : PostShape} {x y : PredTrans ps α} {Q : Assertion ps}
 ```
-The {inst}`LE PredTrans` instance is defined in terms of their logical strength; one transformer is stronger than another if the result of applying it always entails the result of applying the other.
-In other words, {lean}`∀ Q, y Q ⊢ₛ x Q`, then {lean}`x ≤ y`.
+The {inst}`LE (PredTrans ps α)` instance is defined in terms of logical strength; one transformer is stronger than another if the result of applying it always entails the result of applying the other.
+In other words, {lean}`∀ Q, y.apply Q ⊢ₛ x.apply Q`, then {lean}`x ≤ y`.
 This means that stronger predicate transformers are considered greater than weaker ones.
 :::
 
@@ -448,7 +446,6 @@ import Std.Tactic.Do
 ```lean -show
 open Std.Do
 
-set_option mvcgen.warning false
 set_option linter.deprecated.syntax false
 
 ```
@@ -609,7 +606,6 @@ import Std.Tactic.Do
 ```lean -show
 open Std.Do
 
-set_option mvcgen.warning false
 set_option linter.deprecated.syntax false
 
 ```
@@ -723,7 +719,6 @@ import Std.Tactic.Do
 ```lean -show
 open Std.Do
 
-set_option mvcgen.warning false
 set_option linter.deprecated.syntax false
 
 ```
@@ -761,7 +756,6 @@ import Std.Tactic.Do
 ```lean -show
 open Std.Do
 
-set_option mvcgen.warning false
 set_option linter.deprecated.syntax false
 
 ```
@@ -906,7 +900,6 @@ import Std.Tactic.Do
 ```lean -show
 open Std.Do
 
-set_option mvcgen.warning false
 set_option linter.deprecated.syntax false
 
 ```

Manual/Meta.lean

@@ -170,9 +170,8 @@ div.TODO::before {
 }
 "#]
   toHtml :=
-    open Verso.Output.Html in
     some <| fun _ goB _ _ content => do
-      pure {{<div class="TODO">{{← content.mapM goB}}</div>}}
+      pure html%{<div class="TODO">{← content.mapM goB}</div>}
 
 @[inline_extension TODO]
 def TODO.inlineDescr : InlineDescr where
@@ -195,9 +194,8 @@ span.TODO {
 }
 "#]
   toHtml :=
-    open Verso.Output.Html in
     some <| fun go _ _ content => do
-      pure {{<span class="TODO">{{← content.mapM go}}</span>}}
+      pure html%{<span class="TODO">{← content.mapM go}</span>}
 
 def Block.warn : Block where
   name := `Manual.warn
@@ -219,16 +217,15 @@ def warn.descr : BlockDescr where
 .namedocs.warn > .text { border-top: none; }
 "#]
   toHtml :=
-    open Verso.Output.Html in
     some <| fun _ goB _ _ content => do
-      pure {{
+      pure html%{
         <div class="namedocs warn">
-          <span class="label">"Warning"</span>
+          <span class="label">Warning</span>
           <div class="text">
-            {{← content.mapM goB}}
+            {← content.mapM goB}
           </div>
         </div>
-      }}
+      }
 
 def Inline.noVale : Inline where
   name := `Manual.noVale
@@ -254,8 +251,8 @@ meta def noVale : RoleExpander
 def noVale.descr : InlineDescr where
   traverse _ _ _ := pure none
   toTeX := none
-  toHtml := some <| fun go _ _ content => open Verso.Output.Html in do
-    pure {{<span class="no-vale">{{← content.mapM go}}</span>}}
+  toHtml := some <| fun go _ _ content => do
+    pure html%{<span class="no-vale">{← content.mapM go}</span>}
 
 structure PlannedConfig where
   issue : Option Nat
@@ -310,29 +307,28 @@ div.planned .label {
 }
 "#]
   toHtml :=
-    open Verso.Output.Html in
     some <| fun _ goB _ data content => do
       let issue : Option Nat ←
         match FromJson.fromJson? (α := Option Nat × Option (Nat × String)) data with
         | .ok v => pure v.1
         | .error e =>
           reportError s!"Failed to deserialize issue number from {data}: {e}"
           pure none
-      pure {{
+      pure html%{
         <div class="planned">
-          <div class="label">"Planned Content"</div>
-          {{← content.mapM goB}}
-          {{if let some issue := issue then {{
+          <div class="label">Planned Content</div>
+          {← content.mapM goB}
+          {if let some issue := issue then html%{
             <p>
-              "Tracked at issue "
-                <a href=s!"https://github.com/leanprover/reference-manual/issues/{issue}">
-                  s!"#{issue}"
+              {"Tracked at issue "}
+                <a href={s!"https://github.com/leanprover/reference-manual/issues/{issue}"}>
+                  {s!"#{issue}"}
                 </a>
             </p>
-            }} else .empty
-          }}
+            } else .empty
+          }
         </div>
-      }}
+      }
 
 @[role_expander versionString]
 meta def versionString : RoleExpander
@@ -410,8 +406,8 @@ meta def ckw : RoleExpander
 def ckw.descr : InlineDescr where
   traverse _ _ _ := pure none
   toTeX := none
-  toHtml := some fun goI _ _ content => open Verso.Output.Html in do
-    return {{<span class="c-keyword">{{← content.mapM goI}}</span>}}
+  toHtml := some fun goI _ _ content => do
+    return html%{<span class="c-keyword">{← content.mapM goI}</span>}
   extraCss :=
     [".c-keyword code { font-weight: 600; }"]
 
@@ -443,30 +439,29 @@ def ffi.descr : BlockDescr where
     pure none
   toHtml := some <| fun _goI goB id info contents =>
     open Verso.Doc.Html in
-    open Verso.Output Html in do
+    open Verso.Output in do
       let .ok (_name, ffiType, signature) := FromJson.fromJson? (α := String × FFIDocType × String) info
         | do reportError "Failed to deserialize FFI doc data"; pure .empty
-      let sig : Html := {{<pre>{{signature}}</pre>}}
+      let sig : Html := html%{<pre>{signature}</pre>}
 
       let xref ← HtmlT.state
       let idAttr := xref.htmlId id
 
-      return {{
-        <div class="namedocs" {{idAttr}}>
-          <span class="label">"FFI " {{ffiType.describe}}</span>
-          <pre class="signature">{{sig}}</pre>
+      return html%{
+        <div class="namedocs" {...idAttr}>
+          <span class="label">FFI {ffiType.describe}</span>
+          <pre class="signature">{sig}</pre>
           <div class="text">
-            {{← contents.mapM goB}}
+            {← contents.mapM goB}
           </div>
         </div>
-      }}
+      }
   toTeX := some <| fun _goI goB _ _ contents =>
     contents.mapM goB -- TODO
 
-open Verso.Output.Html in
 inline_extension Inline.multiCode where
   traverse _ _ _ := pure none
-  toHtml := some <| fun goI _id _data contents => do return {{<span class="multi-code">{{← contents.mapM goI}}</span>}}
+  toHtml := some <| fun goI _id _data contents => do return html%{<span class="multi-code">{← contents.mapM goI}</span>}
   toTeX := none
 
 @[role]

Manual/Meta/ConfigFile.lean

@@ -47,15 +47,14 @@ inline_extension Inline.configFile (filename : String) where
     pure none
 
   toHtml :=
-    open Verso.Output.Html in
     open Verso.Doc.Html in
     some fun _ id data _ => do
       let .str filename := data
         | reportError s!"Failed to deserialize {data} as a string for the filename"
           pure .empty
       let xref ← HtmlT.state
       let idAttr := xref.htmlId id
-      return {{<code {{idAttr}}>{{filename}}</code>}}
+      return html%{<code {...idAttr}>{filename}</code>}
 
   toTeX := none
 

Manual/Meta/CustomStyle.lean

@@ -23,16 +23,15 @@ block_extension Block.customCSS (css : String) where
   traverse _ _ _ := pure none
   toTeX := none
   toHtml :=
-    open Verso.Output.Html in
     some <| fun _ _ _ data _ => do
       match FromJson.fromJson? data with
       | .error err =>
         reportError <| "Couldn't deserialize CSS while rendering HTML: " ++ err
         pure .empty
       | .ok (css : String) =>
-        pure {{
-          <style>{{css}}</style>
-        }}
+        pure html%{
+          <style>{css}</style>
+        }
 
 @[code_block]
 meta def customCSS : CodeBlockExpanderOf Unit