chore: improve presentation of unconfigured blogs

examples/anchor-examples/AnchorExamples.lean

@@ -9,7 +9,10 @@ import AnchorExamples.Basic
 -- ANCHOR: t
 def someTree : Tree Nat :=
 -- ANCHOR: tDef
-  .branch (.branch .leaf 1 .leaf) 2 (.branch (.branch .leaf 3 .leaf) 4 .leaf)
+  .branch
+    (.branch .leaf 1 .leaf)
+    2
+    (.branch (.branch .leaf 3 .leaf) 4 .leaf)
 -- ANCHOR_END: tDef
 -- ANCHOR_END: t
 
@@ -25,7 +28,8 @@ deriving instance Repr for Tree
 
 
 -- ANCHOR: proof1
-theorem Tree.flip_flip_eq_id : flip ∘ flip = (id : Tree α → Tree α) := by
+theorem Tree.flip_flip_eq_id :
+    flip ∘ flip = (id : Tree α → Tree α) := by
   funext t
   induction t with
   | leaf => rfl
@@ -37,7 +41,8 @@ theorem Tree.flip_flip_eq_id : flip ∘ flip = (id : Tree α → Tree α) := by
 
 -- ANCHOR: proof2
 -- Show more tactic combinators and placement of proof states
-theorem Tree.flip_flip_id' (t : Tree α) : t.flip.flip = t := by
+theorem Tree.flip_flip_id' (t : Tree α) :
+    t.flip.flip = t := by
   induction t
   case leaf => rfl
   next l v r ih1 ih2 =>

examples/anchor-examples/lake-manifest.json

@@ -6,7 +6,7 @@
       "url": "https://github.com/leanprover/subverso",
       "type": "git",
       "subDir": null,
-      "rev": "6d5c658ad7ae2ee1bf954f2edf0d0252b35f1c76",
+      "rev": "f174913cae5c976a3bcc218fddb996fe0ab0a28e",
       "name": "subverso",
       "manifestFile": "lake-manifest.json",
       "inputRev": "main",

examples/documented-package/lake-manifest.json

@@ -7,7 +7,7 @@
       "type": "git",
       "subDir": null,
       "scope": "",
-      "rev": "6d5c658ad7ae2ee1bf954f2edf0d0252b35f1c76",
+      "rev": "f174913cae5c976a3bcc218fddb996fe0ab0a28e",
       "name": "subverso",
       "manifestFile": "lake-manifest.json",
       "inputRev": "main",

examples/textbook/DemoTextbook.lean

@@ -24,7 +24,6 @@ open DemoTextbook
 set_option pp.rawOnError true
 
 
-
 #doc (Manual) "A Textbook" =>
 
 %%%

examples/website-examples/lake-manifest.json

@@ -6,7 +6,7 @@
       "url": "https://github.com/leanprover/subverso",
       "type": "git",
       "subDir": null,
-      "rev": "6d5c658ad7ae2ee1bf954f2edf0d0252b35f1c76",
+      "rev": "f174913cae5c976a3bcc218fddb996fe0ab0a28e",
       "name": "subverso",
       "manifestFile": "lake-manifest.json",
       "inputRev": "main",

examples/website-literate/lake-manifest.json

@@ -7,7 +7,7 @@
       "type": "git",
       "subDir": null,
       "scope": "",
-      "rev": "6d5c658ad7ae2ee1bf954f2edf0d0252b35f1c76",
+      "rev": "f174913cae5c976a3bcc218fddb996fe0ab0a28e",
       "name": "subverso",
       "manifestFile": "lake-manifest.json",
       "inputRev": "main",

examples/website/DemoSite/Blog/AnchorBased.lean

@@ -35,12 +35,18 @@ Here's a tree:
 
 ```anchor t
 def someTree : Tree Nat :=
-  .branch (.branch .leaf 1 .leaf) 2 (.branch (.branch .leaf 3 .leaf) 4 .leaf)
+  .branch
+    (.branch .leaf 1 .leaf)
+    2
+    (.branch (.branch .leaf 3 .leaf) 4 .leaf)
 ```
 
 And here's just part of its definition:
 ```anchor tDef
-  .branch (.branch .leaf 1 .leaf) 2 (.branch (.branch .leaf 3 .leaf) 4 .leaf)
+  .branch
+    (.branch .leaf 1 .leaf)
+    2
+    (.branch (.branch .leaf 3 .leaf) 4 .leaf)
 ```
 
 It's left branch is {anchorTerm tDef}`.branch .leaf 1 .leaf` which includes a reference to {anchorName tDef}`.leaf`.
@@ -58,7 +64,8 @@ Tree.branch
 
 As does proofs and parts of proofs:
 ```anchor proof1
-theorem Tree.flip_flip_eq_id : flip ∘ flip = (id : Tree α → Tree α) := by
+theorem Tree.flip_flip_eq_id :
+    flip ∘ flip = (id : Tree α → Tree α) := by
   funext t
   induction t with
   | leaf => rfl
@@ -77,7 +84,8 @@ branch l v r ih1 ih2
 
 This rendering of the same proof doesn't have proof states:
 ```anchor proof1 (showProofStates := false)
-theorem Tree.flip_flip_eq_id : flip ∘ flip = (id : Tree α → Tree α) := by
+theorem Tree.flip_flip_eq_id :
+    flip ∘ flip = (id : Tree α → Tree α) := by
   funext t
   induction t with
   | leaf => rfl

examples/website/DemoSite/Blog/Conditionals.lean

@@ -179,35 +179,43 @@ theorem grow_10_id {α} : grow (α := α) 6 = id := by
 
 Here is a proof with big terms in the context:
 ```lean demo
+section
+open Lean
 
-open Lean in
-def quotedStx [Monad m] [MonadQuotation m] [MonadRef m] (str : String) : m Syntax := do
+variable [Monad m] [MonadQuotation m] [MonadRef m]
+
+def quoted (str : String) : m Syntax := do
   let s ← `(a b c #[x, $(quote str), z])
   pure s
 
-open Lean in
-example [Monad m] [MonadQuotation m] [MonadRef m] : ¬(quotedStx (m := m) = fun (x : String) => pure .missing) := by
-  unfold quotedStx
+example : ¬(quoted (m := m) = fun x => pure .missing) := by
+  unfold quoted
   intro h
   let g : String → m Syntax := fun str => do
     let s ← `(a b c #[x, $(quote str), z])
     pure s
   have : g "hello" ≠ pure .missing := by skip; sorry
   sorry
+
+end
 ```
 
 It's possible to render a lot of info on one example:
 ```lean demo
-elab "%much_info(" t:term ")" : term => open Lean Elab Term in do
+open Lean Elab Term in
+elab "%much_info(" t:term ")" : term => do
   for i in [0:20] do
     logInfoAt t m!"Hello! ({i})"
   logInfoAt t "Some multi-line\ninfo too"
   elabTerm t none
 
-elab "%more_info(" t:term ")" : term => open Lean Elab Term in do
+open Lean Elab Term in
+elab "%more_info(" t:term ")" : term => do
   for i in [0:20] do
     logInfoAt t m!"Hello again! ({i})"
-  logErrorAt t "And a great big error, much wider than the other info!"
+  logErrorAt t <|
+    "And a great big error, " ++
+    "much wider than the other info!"
   elabTerm t none
 ```
 

examples/website/DemoSiteMain.lean

@@ -32,25 +32,28 @@ def theme : Theme := { Theme.default with
     return {{
       <html>
         <head>
-          <meta charset="UTF-8"/>
+          <meta charset="utf-8"/>
+          <meta name="viewport" content="width=device-width, initial-scale=1"/>
+          <meta name="color-scheme" content="light dark"/>
+          <link rel="stylesheet" href="https://cdn.jsdelivr.net/npm/sakura.css/css/sakura.css" type="text/css"/>
           <title>{{ (← param (α := String) "title") }} " — Verso "</title>
           <link rel="stylesheet" href="/static/style.css"/>
           {{← builtinHeader }}
         </head>
         <body>
           <header>
             <div class="inner-wrap">
-            <a class="logo" href="/"><img src="/static/logo.png"/></a>
+            <a class="logo" href="/"><h1>"A Verso Site"</h1></a>
             {{ ← topNav }}
             </div>
           </header>
-          <div class="main" role="main">
+          <main>
             <div class="wrap">
               {{ (← param "content") }}
               {{ postList }}
               {{ catList }}
             </div>
-          </div>
+          </main>
         </body>
       </html>
     }}

examples/website/static_files/style.css

@@ -1,88 +1,19 @@
 
-/* http://meyerweb.com/eric/tools/css/reset/
-   v2.0 | 20110126
-   License: none (public domain)
-*/
-
-html, body, div, span, applet, object, iframe,
-h1, h2, h3, h4, h5, h6, p, blockquote, pre,
-a, abbr, acronym, address, big, cite, code,
-del, dfn, em, img, ins, kbd, q, s, samp,
-small, strike, strong, sub, sup, tt, var,
-b, u, i, center,
-dl, dt, dd, ol, ul, li,
-fieldset, form, label, legend,
-table, caption, tbody, tfoot, thead, tr, th, td,
-article, aside, canvas, details, embed,
-figure, figcaption, footer, header, hgroup,
-menu, nav, output, ruby, section, summary,
-time, mark, audio, video {
-    margin: 0;
-    padding: 0;
-    border: 0;
-    font-size: 100%;
-    font: inherit;
-    vertical-align: baseline;
-}
-/* HTML5 display-role reset for older browsers */
-article, aside, details, figcaption, figure,
-footer, header, hgroup, menu, nav, section {
-    display: block;
-}
-body {
-    line-height: 1;
-    font-size: 14px;
-}
-/***********************************/
-
-li {
-    margin-left: 1.5em;
-}
-
-pre {
-    font-family: monospace;
-}
-
-p, pre, code.block {
-    line-height: 1.25;
-}
-
-h1 {
-    font-size: 150%;
-}
-
-h2 {
-    font-size: 140%;
-}
-
-h3 {
-    font-size: 130%;
-}
-
-h4 {
-    font-size: 120%;
-}
-
-h5 {
-    font-size: 110%;
-}
-
-h6 {
-    font-size: 105%;
-}
-
-header, div.main {
-    margin-left: 4em;
-    margin-right: 4em;
-    max-width: 50em;
-}
+/**************************/
 
-header {
-    margin-bottom: 1.5em;
+nav ol {
+  display: flex;
+  flex-wrap: wrap; /* Wrap to new lines on small screens */
+  list-style: none;
+  margin: 0;
+  padding: 0;
+  gap: 3rem;
 }
 
-.main p, .main pre, .main code.block {
-  margin-bottom: 0.5em;
+@media (max-width: 600px) {
+  nav ol {
+    flex-direction: column; /* Stack vertically on mobile */
+  }
 }
 
 div.metadata {
@@ -154,6 +85,12 @@ code {
 
 /**************************/
 
+.hl.lean.block {
+  margin-bottom: 2.5rem; /* Match sakura.css's setting for block elements */
+}
+
+/**************************/
+
 .lexed.json .brace {
     color: #0000aa;
 }

lake-manifest.json

@@ -15,7 +15,7 @@
    "type": "git",
    "subDir": null,
    "scope": "",
-   "rev": "6d5c658ad7ae2ee1bf954f2edf0d0252b35f1c76",
+   "rev": "f174913cae5c976a3bcc218fddb996fe0ab0a28e",
    "name": "subverso",
    "manifestFile": "lake-manifest.json",
    "inputRev": "main",

lakefile.lean

@@ -12,10 +12,15 @@ lean_lib VersoUtil where
   srcDir := "src/verso-util"
   roots := #[`VersoUtil]
 
+input_file versoVars where
+  text := true
+  path := "static-web/verso-vars.css"
+
 @[default_target]
 lean_lib Verso where
   srcDir := "src/verso"
   roots := #[`Verso]
+  needs := #[versoVars]
 
 @[default_target]
 lean_lib MultiVerso where

src/verso-blog/VersoBlog.lean

@@ -31,6 +31,7 @@ open Verso ArgParse Doc Elab
 open Verso.SyntaxUtils (parserInputString)
 
 open SubVerso.Examples (loadExamples Example)
+open SubVerso.Examples.Messages (messagesMatch)
 open SubVerso.Module (ModuleItem)
 
 def classArgs : ArgParse DocElabM String := .named `«class» .string false
@@ -764,7 +765,7 @@ where
     pure <| withNewline <| head ++ (← message.data.toString)
 
   mostlyEqual (ws : WhitespaceMode) (s1 s2 : String) : Bool :=
-    ws.apply s1.trim == ws.apply s2.trim
+    messagesMatch (ws.apply s1.trim) (ws.apply s2.trim)
 
 open Lean Elab Command in
 elab "define_lexed_text" blockName:ident " ← " lexerName:ident : command => do

src/verso-blog/VersoBlog/Template.lean

@@ -14,6 +14,7 @@ import VersoBlog.Basic
 import VersoBlog.Site
 import VersoBlog.Component
 import Verso.Output.Html
+import Verso.Output.Html.CssVars
 import Verso.Code
 
 open Std (HashSet)
@@ -149,7 +150,7 @@ def blockHtml (g : Genre)
     withReader (fun ρ => { ρ with codeOptions.inlineProofStates := showProofStates }) <|
     hls.blockHtml (toString contextName) (g := g)
   | .message summarize msg, _contents => do
-    return {{<pre class="lean-output hl lean">{{← msg.toHtml (g := g)}}</pre>}}
+    return {{<pre class=s!"lean-output hl lean {msg.severity.class}">{{← msg.toHtml (g := g)}}</pre>}}
   | .htmlDetails classes summary, contents => do
     pure {{ <details class={{classes}}><summary>{{summary}}</summary> {{← contents.mapM goB}}</details>}}
   | .htmlWrapper name attrs, contents => do
@@ -300,8 +301,11 @@ def param [TypeName α] (key : String) : TemplateM α := do
     if let some v := val.get? (α := α) then return v
     else throw <| .wrongParamType key (TypeName.typeName α)
 
+
 def builtinHeader : TemplateM Html := do
   let mut out := .empty
+  -- These should come first so later stylesheets can easily override them.
+  out := out ++ {{<style>{{«verso-vars.css»}}</style>}}
   for style in (← read).builtInStyles do
     out := out ++ {{<style>"\n"{{.text false style}}"\n"</style>"\n"}}
   for script in (← read).builtInScripts do