Initial commit from verso-templates/textbook

Author: lzy0505

README.md

@@ -0,0 +1,26 @@
+This is a demonstration of a textbook built in Verso's manual genre.
+
+To build it, run:
+```
+$ lake exe textbook
+```
+
+This textbook is written in the `Manual` genre. It uses the same
+version of Lean for the example code as it does for Verso itself;
+please see [the package description example](../package-docs) for an
+example in which the Lean code is external to the document and written
+in a different version of Lean.
+
+# Code Samples
+
+Additionally, this example demonstrates a non-trivial extension to the
+manual genre: extraction of Lean modules from the inline examples. This
+extension uses [a custom `savedLean` code block](TextbookTemplate/Meta/Lean.lean)
+to indicate that an example or exercise should be saved. At elaboration time,
+a custom block element saves the original filename and the contents of the
+code block. Then, in [`TextbookTemplateMain.lean`](TextbookTemplateMain.lean), the
+custom build step `buildExercises` traverses the entire book prior to HTML
+generation, collecting the exercise blocks. The collected blocks are assembled
+into files and written to the `example-code` subdirectory of the output.
+
+

TextbookTemplate.lean

@@ -0,0 +1,151 @@
+/-
+Copyright (c) 2024-2025 Lean FRO LLC. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Author: David Thrane Christiansen
+-/
+
+import VersoManual
+import TextbookTemplate.Meta.Lean
+import TextbookTemplate.Papers
+
+-- This is a chapter that's included
+import TextbookTemplate.Nat
+
+-- This gets access to most of the manual genre (which is also useful for textbooks)
+open Verso.Genre Manual
+
+-- This gets access to Lean code that's in code blocks, elaborated in the same process and
+-- environment as Verso
+open Verso.Genre.Manual.InlineLean
+
+
+open TextbookTemplate
+
+set_option pp.rawOnError true
+
+
+#doc (Manual) "A Textbook" =>
+
+%%%
+authors := ["David Thrane Christiansen"]
+%%%
+
+{index}[example]
+Here's an example project showing how to build a certain kind of textbook with Verso.
+It's a good idea to read the document's source together with the rendered output, because it demonstrates how to use various features.
+
+
+# Lean Code
+
+The tools in this section come from the Verso namespace `Verso.Genre.Manual.InlineLean`.
+
+The {lean}`lean` code block allows Lean code to be included in the text.
+It is elaborated in the context of the text's elaboration.
+
+```lean
+inductive NatList where
+  | nil
+  | cons : Nat → NatList → NatList
+```
+
+Use the {lean}`leanSection` directive to create a Lean section that delimits scope changes.
+The {lean}`lean` role allows Lean terms to be included as inline elements in paragraphs.
+Use {lean}`name` to refer to a name that can't be easily elaborated as a term, e.g. due to implicit parameters or type classes.
+
+## Saved Lean Code
+
+The tools in this section come from the Verso namespace `TextbookTemplate` in the module `TextbookTemplate.Meta.Lean`.
+
+The {lean}`savedLean` code block is just like the {lean}`lean` block, except it additionally saves the contents to a file when the book is built.
+The code is saved to the output directory, in the subdirectory `example-code` (by default, this is `_out/example-code`), with its filename being that of the file in which it is edited.
+Use {lean}`savedImport` to save code for the file header.
+
+```savedComment
+Here's some commentary for the file
+```
+```savedLean
+def x : Nat := 15
+```
+
+When named, the code block's output is saved.
+It can be both checked and included in the document using {lean}`leanOutput`:
+
+```savedLean (name := xVal)
+#eval x
+```
+```leanOutput xVal
+15
+```
+
+Expected error messages must be indicated explicitly:
+```lean +error (name := yVal)
+#eval y
+```
+```leanOutput yVal
+Unknown identifier `y`
+```
+
+{include 1 TextbookTemplate.Nat}
+
+# Notes
+
+Use {lean}`margin` to create a marginal note.{margin}[Marginal notes should be used like footnotes.]
+
+# Citations
+
+Cite works using {lean}`citet`, {lean}`citep`, or {lean}`citehere`.
+They take a name of a citable reference value as a parameter.
+References should be defined as values, typically in one module that is imported (similar to the role of a `.bib` file in LaTeX).
+
+Textual citations, as with {citet someThesis}[], look like this.
+Parenthetical {citep someArXiv}[] looks like this.
+Use {lean}`citehere` to literally include the cite rather than making a margin note, e.g. {citehere somePaper}[].
+Literally-included cites are mostly useful when performing citation inside a margin note.
+
+# Section References
+%%%
+tag := "sec-ref"
+%%%
+
+Sections with tags can be cross-referenced.
+They additionally gain permalink indicators that can be used to link to them even if the document is reorganized.
+Tags are added in section metadata, e.g.
+```
+%%%
+tag := "my-tag"
+%%%
+```
+They can be linked to using {lean}`ref`.
+Here's one to {ref "sec-ref"}[this section].
+
+
+
+# Viewing the Output
+
+Verso's HTML doesn't presently work correctly when opened directly in a browser, so it should be served via a server.{margin}[This is due to security restrictions on retrieved files: some of the code hovers are deduplicated to a JSON file that's fetched on demand.]
+One portable way to do this is documented in the root of this repository.
+
+# Using an Index
+
+{index}[index]
+The index should contain an entry for “lorem ipsum”.
+{index}[lorem ipsum] foo
+{index (subterm := "of lorem")}[ipsum]
+{index (subterm := "per se")}[ipsum]
+{index}[ipsum]
+Lorem ipsum dolor {index}[dolor] sit amet, consectetur adipiscing elit, sed {index}[sed] do eiusmod tempor incididunt ut labore et dolore magna aliqua. Ut enim ad minim veniam, quis nostrud exercitation ullamco laboris {index}[laboris] {see "lorem ipsum"}[laboris] {seeAlso "dolor"}[laboris] nisi ut aliquip ex ea commodo consequat. Duis aute irure dolor in reprehenderit in voluptate velit esse cillum dolore eu fugiat nulla pariatur. Excepteur sint occaecat cupidatat non proident, sunt in culpa qui officia deserunt mollit anim id est laborum.
+
+This is done using the `{index}[term]` syntax. Sub-terms {index (subterm := "sub-term")}[entry] can be added using the `subterm` parameter to `index`.
+
+Multiple index {index}[index] targets for a term also work.
+
+{ref "index"}[Index link]
+
+
+# Index
+%%%
+number := false
+tag := "index"
+%%%
+
+{theIndex}

TextbookTemplate/Meta/Lean.lean

@@ -0,0 +1,57 @@
+/-
+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 VersoManual
+
+open Verso.Genre Manual
+open Verso.Doc Elab
+open Verso.ArgParse
+open Lean
+
+namespace TextbookTemplate
+
+block_extension Block.savedLean (file : String) (source : String) where
+  data := .arr #[.str file, .str source]
+
+  traverse _ _ _ := pure none
+  toTeX := none
+  toHtml := some fun _ goB _ _ contents =>
+    contents.mapM goB
+
+block_extension Block.savedImport (file : String) (source : String) where
+  data := .arr #[.str file, .str source]
+
+  traverse _ _ _ := pure none
+  toTeX := none
+  toHtml := some fun _ _ _ _ _ =>
+    pure .empty
+
+/--
+Lean code that is saved to the examples file.
+-/
+@[code_block savedLean]
+def savedLean : CodeBlockExpanderOf InlineLean.LeanBlockConfig
+  | args, code => do
+    let underlying ← InlineLean.lean args code
+    ``(Block.other (Block.savedLean $(quote (← getFileName)) $(quote (code.getString))) #[$underlying])
+
+/--
+An import of some other module, to be located in the saved code. Not rendered.
+-/
+@[code_block]
+def savedImport : CodeBlockExpanderOf Unit
+  | (), code => do
+    ``(Block.other (Block.savedImport $(quote (← getFileName)) $(quote (code.getString))) #[])
+
+/--
+Comments to be added as module docstrings to the examples file.
+-/
+@[code_block]
+def savedComment : CodeBlockExpanderOf Unit
+  | (), code => do
+    let str := code.getString.trimAsciiEnd.copy
+    let comment := s!"/-!\n{str}\n-/"
+    ``(Block.other (Block.savedLean $(quote (← getFileName)) $(quote comment)) #[])

TextbookTemplate/Nat.lean

@@ -0,0 +1,93 @@
+/-
+Copyright (c) 2024-2025 Lean FRO LLC. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Author: David Thrane Christiansen
+-/
+
+import VersoManual
+import TextbookTemplate.Meta.Lean
+import TextbookTemplate.Papers
+
+-- This gets access to most of the manual genre (which is also useful for textbooks)
+open Verso.Genre Manual
+
+-- This gets access to Lean code that's in code blocks, elaborated in the same process and
+-- environment as Verso
+open Verso.Genre.Manual.InlineLean
+
+
+open TextbookTemplate
+
+set_option pp.rawOnError true
+
+
+
+#doc (Manual) "The Natural Numbers" =>
+
+```savedLean
+namespace MyNats
+```
+
+```savedLean
+inductive Nat where
+  | zero
+  | succ : Nat → Nat
+```
+
+```savedLean
+def Nat.ofNat : _root_.Nat → Nat
+  | 0 => .zero
+  | n + 1 => .succ (.ofNat n)
+```
+
+```savedLean
+instance : OfNat Nat n where
+  ofNat := .ofNat n
+```
+
+```savedLean
+@[match_pattern]
+def Nat.add (n k : Nat) : Nat :=
+  match k with
+  | .zero => n
+  | .succ k' => .succ (n.add k')
+```
+
+```savedLean
+instance : Add Nat where
+  add := Nat.add
+```
+
+```savedLean
+def Nat.toNat : MyNats.Nat → _root_.Nat
+  | 0 => 0
+  | n + 1 => toNat n + 1
+```
+
+
+```lean (name := verboseOut)
+#eval (4 : MyNats.Nat) + 2
+```
+```leanOutput verboseOut
+MyNats.Nat.succ
+  (MyNats.Nat.succ (MyNats.Nat.succ (MyNats.Nat.succ (MyNats.Nat.succ (MyNats.Nat.succ (MyNats.Nat.zero))))))
+```
+
+```lean
+instance : Repr Nat where
+  reprPrec n _prec := repr n.toNat
+
+instance : ReprAtom Nat where
+```
+
+```lean (name := betterOut)
+#eval (4 : MyNats.Nat) + 2
+```
+```leanOutput betterOut
+6
+```
+
+
+```savedLean
+end MyNats
+```

TextbookTemplate/Papers.lean

@@ -0,0 +1,28 @@
+/-
+Copyright (c) 2024-2025 Lean FRO LLC. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Author: David Thrane Christiansen
+-/
+import VersoManual
+open Verso.Genre.Manual
+
+-- Here, `inlines!` is a macro that parses a string constant into Verso inline elements
+
+def someThesis : Thesis where
+  title := inlines!"A Great Thesis"
+  author := inlines!"A. Great Student"
+  year := 2025
+  university := inlines!"A University"
+  degree := inlines!"Something"
+
+def somePaper : InProceedings where
+  title := inlines!"Grommulation of Flying Lambdas"
+  authors := #[inlines!"A. Great Student"]
+  year := 2025
+  booktitle := inlines!"Proceedings of the Best Conference Ever"
+
+def someArXiv : ArXiv where
+  title := inlines!"Grommulation of Flying Lambdas"
+  authors := #[inlines!"A. Great Student"]
+  year := 2025
+  id := "...insert arXiv id here..."