chore: permalinks and repo links (#125)

Bump Verso to get repo links and permalink widgets; also add tags to
every section to get stable link targets.

Main.lean

@@ -19,5 +19,7 @@ where
     extraJs := ["/static/katex/katex.min.js", "/static/math.js", "/static/print.js"],
     emitTeX := false,
     emitHtmlSingle := true, -- for proofreading
-    logo := some "/static/lean_logo.svg"
+    logo := some "/static/lean_logo.svg",
+    sourceLink := some "https://github.com/leanprover/reference-manual",
+    issueLink := some "https://github.com/leanprover/reference-manual/issues"
   }

Manual.lean

@@ -18,6 +18,10 @@ open Verso.Genre Manual
 set_option pp.rawOnError true
 
 #doc (Manual) "The Lean Language Reference" =>
+%%%
+tag := "lean-language-reference"
+%%%
+
 
 This is the _Lean Language Reference_, an in-progress reference work on Lean.
 It is intended to be a comprehensive, precise description of Lean: a reference work in which Lean users can look up detailed information, rather than a tutorial for new users.
@@ -32,6 +36,10 @@ For other documentation, please refer to the [Lean documentation site](https://l
 {include Manual.Terms}
 
 # Monads and `do`-Notation
+%%%
+tag := "monads-and-do"
+%%%
+
 
 :::planned 102
 This chapter will describe `do`-notation in Lean:
@@ -41,6 +49,10 @@ This chapter will describe `do`-notation in Lean:
 :::
 
 # IO
+%%%
+tag := "io"
+%%%
+
 :::planned 102
 This chapter will describe features for writing programs that can have side effects on the real world.
 :::
@@ -52,12 +64,20 @@ This chapter will describe features for writing programs that can have side effe
 {include 0 Manual.BasicTypes}
 
 # Standard Library
+%%%
+tag := "standard-library"
+%%%
+
 
 :::planned 109
 Overview of the standard library, including types from the prelude and those that require imports.
 :::
 
 ## Optional Values
+%%%
+tag := "option"
+%%%
+
 :::planned 110
 Describe {name}`Option`, including the default coercions and its API.
 :::
@@ -69,12 +89,19 @@ tag := "language-extension"
 %%%
 
 ## Notations
+%%%
+tag := "notations"
+%%%
+
 
 :::planned 69
 A presentation of the `notation` command and how to define infix operators
 :::
 
 ## Syntax Categories and Extensions
+%%%
+tag := "syntax-categories"
+%%%
 
 :::planned 70
  * Syntax extension and syntax categories
@@ -107,6 +134,10 @@ For now, a quick overview of elaborators - detailed description to be written in
 :::
 
 # Elan
+%%%
+tag := "elan"
+%%%
+
 
 ::: planned 74
 
@@ -119,15 +150,26 @@ This section will describe Elan and how to use it:
 :::
 
 # Lake and Reservoir
+%%%
+tag := "build-tools-and-distribution"
+%%%
 
 ## Lake
+%%%
+tag := "lake"
+%%%
+
 
 ::: planned 75
  * Port and organize the information in the Lake README
  * Describe the underlying Lake-specific concepts of traces, artifacts, workspaces, and facets
 :::
 
 ## Reservoir
+%%%
+tag := "reservoir"
+%%%
+
 
 ::: planned 76
  * Concepts

Manual/BasicTypes.lean

@@ -18,6 +18,10 @@ set_option pp.rawOnError true
 
 
 #doc (Manual) "Basic Types" =>
+%%%
+tag := "basic-types"
+%%%
+
 
 Lean includes a number of built-in datatypes that are specially supported by the compiler.
 Some, such as {lean}`Nat`, additionally have special support in the kernel.
@@ -26,19 +30,31 @@ Other types don't have special compiler support _per se_, but rely in important
 {include 0 Manual.BasicTypes.Nat}
 
 # Integers
+%%%
+tag := "Int"
+%%%
+
 ::: planned 104
  * Compile-time and run-time characteristics, and how they're inherited from {lean}`Nat`
  * API reference
 :::
 
 # Fixed-Precision Integer Types
+%%%
+tag := "fixed-ints"
+%%%
+
 
 ::: planned 105
  * Compile-time and run-time characteristics for {lean}`UInt8`, {lean}`UInt16`, {lean}`UInt32`, {lean}`UInt64`
  * API reference
 :::
 
 # Bitvectors
+%%%
+tag := "BitVec"
+%%%
+
 
 :::planned 106
  * Run-time and kernel representations of {name}`BitVec`
@@ -47,6 +63,10 @@ Other types don't have special compiler support _per se_, but rely in important
 :::
 
 # Floating-Point Numbers
+%%%
+tag := "Float"
+%%%
+
 
 :::planned 107
  * Run-time and kernel representations
@@ -55,23 +75,44 @@ Other types don't have special compiler support _per se_, but rely in important
 :::
 
 # Characters
+%%%
+tag := "Char"
+%%%
+
 
 {docstring Char}
 
 ## Syntax
-
-## Logical Model
+%%%
+tag := "char-syntax"
+%%%
 
 
+## Logical Model
+%%%
+tag := "char-model"
+%%%
 
 ## Run-Time Representation
+%%%
+tag := "char-runtime"
+%%%
+
 
 In monomorphic contexts, characters are represented as 32-bit immediate values. In other words, a field of a datatype or structure of type `Char` does not require indirection to access. In polymorphic contexts, characters are boxed.
 
 
 ## API Reference
+%%%
+tag := "char-api"
+%%%
+
 
 ### Character Classes
+%%%
+tag := "char-api-classes"
+%%%
+
 
 {docstring Char.isAlpha}
 
@@ -89,6 +130,10 @@ In monomorphic contexts, characters are represented as 32-bit immediate values.
 {include 0 Manual.BasicTypes.String}
 
 # Linked Lists
+%%%
+tag := "List"
+%%%
+
 
 ::: planned 108
  * Representation at compile time and run time
@@ -98,6 +143,9 @@ In monomorphic contexts, characters are represented as 32-bit immediate values.
 :::
 
 # Arrays
+%%%
+tag := "Array"
+%%%
 
 ::: planned 91
 Description and API reference for {name}`Thunk`:
@@ -108,6 +156,10 @@ Description and API reference for {name}`Thunk`:
 
 
 # Lazy Computations
+%%%
+tag := "Thunk"
+%%%
+
 
 ::: planned 92
 Description and API reference for {name}`Thunk`:
@@ -117,6 +169,10 @@ Description and API reference for {name}`Thunk`:
 :::
 
 # Tasks and Threads
+%%%
+tag := "concurrency"
+%%%
+
 
 ::: planned 90
 Description and API reference for {name}`Task` and runtime threads, including {lean}`IO.Promise`