feat: heuristically render Markdown in docstrings

Adds a pass to docstring rendering that tries various approaches to
get sensible highlighted Lean code, and that makes many examples look
better.

.github/workflows/ci.yml

@@ -92,6 +92,9 @@ jobs:
             sourcecodepro
             sourcesanspro
             sourceserifpro
+            fvextra
+            upquote
+            lineno
 
       - name: Check `tlmgr` version
         run: tlmgr --version

doc/UsersGuide/Basic.lean

@@ -53,6 +53,28 @@ results in
 
 {docstring List.forM}
 
+## More Docstring Examples
+
+{docstring Lean.Syntax}
+
+{docstring List}
+
+{docstring String}
+
+{docstring Subtype}
+
+{docstring OfNat}
+
+{docstring Monad}
+
+:::tactic "induction"
+:::
+
+:::tactic "simp"
+:::
+
+{docstring Nat}
+
 # Index
 %%%
 number := false

src/verso-manual/VersoManual.lean

@@ -285,7 +285,7 @@ def page (toc : List Html.Toc) (path : Path) (textTitle : String) (htmlTitle con
     (extraJsFiles := config.extraJs.toArray ++ state.extraJsFiles.map ("/-verso-js/" ++ ·.1))
 
 def Config.relativize (config : Config) (path : Path) (html : Html) : Html :=
-  if let some _ := config.baseURL then
+  if config.baseURL.isSome then
     -- Make all absolute URLS be relative to the site root, because that'll make them `base`-relative
     Html.relativize #[] html
   else