feat: tutorials genre (#600)

Adds a genre for tutorials.

Tutorials are very much like the manual genre, and re-use most of its
infrastructure and extensions. The differences are:
1. The rendering of tutorials is more flexible, designed to fit in to
existing web designs (and in particular, the Lean design).
2. Tutorials have different metadata, and will not initially support
non-HTML output.

Additionally, tutorials will feature support for loading their content
on live.lean-lang.org and downloading their example code.

Author: david-christiansen

.gitignore

@@ -9,3 +9,6 @@ _out
 /.verso/
 /src/tests/integration/**/output
 /node_modules
+*.hash
+profile.json
+profile.json.gz

examples/tutorial-examples/Main.lean

@@ -0,0 +1,36 @@
+/-
+Copyright (c) 2025 Lean FRO LLC. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Author: David Thrane Christiansen
+-/
+import VersoTutorial
+import TutorialExample
+
+open Verso.Genre Tutorial
+
+open Verso.Doc.Concrete in
+def content : Tutorials where
+  content :=
+    (verso (Blog.Page) "Example Tutorial Site"
+    ::::
+    Here are some examples of the tutorials feature.
+    ::::).toPart
+
+  topics := #[
+    { title := #[inlines!"Data"],
+      titleString := "Data",
+      description := #[blocks!"These tutorials describe the use of data in Lean."]
+      tutorials := #[
+        %doc TutorialExample.Data,
+        %doc TutorialExample.HashMap,
+        literate_part⟨"." TutorialExample.Lit "Literately-Produced Tutorial" {slug := "literate", summary := "checks that we can load them", exampleStyle := .inlineLean `Lit} : Tutorial⟩ |>.toPart]
+    },
+    { title := #[inlines!"Tactics"],
+      titleString := "Tactics",
+      description := #[]
+      tutorials := #[%doc TutorialExample.RCases]
+    }
+
+  ]
+
+def main := tutorialsMain content (config := { destination := "_out/tut" })

examples/tutorial-examples/TutorialExample.lean

@@ -0,0 +1,9 @@
+/-
+Copyright (c) 2025 Lean FRO LLC. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Author: David Thrane Christiansen
+-/
+import TutorialExample.Data
+import TutorialExample.HashMap
+import TutorialExample.RCases
+-- Important: don't import Lit here