feat: start simp chapter

Manual/Elaboration.lean

@@ -14,5 +14,19 @@ set_option pp.rawOnError true
  * Describe the roles of the {deftech}_kernel_, the interpreter, the compiler, the {deftech key:="elaborate"}[elaborator], and how they interact
  * Sketch the pipeline (parser -> command elaborator (with macro expansion) -> term elaborator (with macro expansion) -> ...
  * Cost model for programs - what data is present at which stage?
+:::
+
+
+# Initialization
+
+:::planned
+Describe {deftech}[initialization]
+:::
+
+:::syntax command
+```grammar
+initialize
+  $cmd*
+```
 
 :::

Manual/Language.lean

@@ -65,6 +65,11 @@ Propositions have the following properties:
 
   With the exception of singletons, propositions cannot be eliminated into non-proposition types.
 
+: {deftech key:="propositional extensionality"}[Extensionality] {index subterm:="of propositions"}[extensionality]
+
+  Any two logically equivalent propositions can be proven to be equal with the {lean}`propext` axiom.
+
+{docstring propext}
 
 ## Universes
 
@@ -628,6 +633,11 @@ tag := "well-founded-recursion"
 This section will describe the translation of {deftech}[well-founded recursion].
 :::
 
+## Controlling Reduction
+
+:::planned
+This section will describe {deftech}[reducible], {deftech}[semireducible], and {deftech}[irreducible] definitions.
+:::
 
 # Type Classes
 

Manual/Meta.lean

@@ -10,6 +10,7 @@ import Verso.Code
 import SubVerso.Highlighting
 import SubVerso.Examples
 
+import Manual.Meta.Attribute
 import Manual.Meta.Basic
 import Manual.Meta.CustomStyle
 import Manual.Meta.Example

Manual/Meta/Attribute.lean

@@ -0,0 +1,75 @@
+import VersoManual
+
+import Verso.Code.Highlighted
+
+import Manual.Meta.Basic
+import Manual.Meta.PPrint
+
+open Verso Doc Elab
+open Verso.Genre Manual
+open Verso.ArgParse
+open Verso.Code (highlightingJs)
+open Verso.Code.Highlighted.WebAssets
+
+
+open Lean Elab Parser
+open Lean.Widget (TaggedText)
+open SubVerso.Highlighting
+open Verso.Code
+
+namespace Manual
+
+def Inline.attr : Inline where
+  name := `Manual.attr
+
+@[role_expander attr]
+def attr : RoleExpander
+  | args, inlines => do
+    let () ← ArgParse.done.run args
+    let #[arg] := inlines
+      | throwError "Expected exactly one argument"
+    let `(inline|code{ $a:str }) := arg
+      | throwErrorAt arg "Expected code literal with the attribute"
+    let altStr ← parserInputString a
+
+    match Parser.runParserCategory (← getEnv) `attr altStr (← getFileName) with
+    | .error e => throwErrorAt a e
+    | .ok stx =>
+      match stx.getKind with
+      | `Lean.Parser.Attr.simple =>
+        let attrName := stx[0].getId
+        throwErrorAt a "Simple: {attrName} {isAttribute (← getEnv) attrName}"
+      | .str (.str (.str (.str .anonymous "Lean") "Parser") "Attr") k =>
+        match getAttributeImpl (← getEnv) k.toName with
+        | .error e => throwErrorAt a e
+        | .ok {descr, name, ref, ..} =>
+          let attrTok := a.getString
+          let hl : Highlighted := attrToken ref descr attrTok
+          discard <| realizeGlobalConstNoOverloadWithInfo (mkIdentFrom a ref)
+          pure #[← `(Verso.Doc.Inline.other {Inline.attr with data := ToJson.toJson $(quote hl)} #[Verso.Doc.Inline.code $(quote attrTok)])]
+      | other =>
+      throwErrorAt a "Kind is {stx.getKind} {isAttribute (← getEnv) stx.getKind} {attributeExtension.getState (← getEnv) |>.map |>.toArray |>.map (·.fst) |>.qsort (·.toString < ·.toString) |> repr}"
+
+where
+  -- TODO: This will eventually generate the right cross-reference, but VersoManual needs to have a
+  -- domain for syntax categories/kinds upstreamed to it first (and then the appropriate link target
+  -- code added)
+  attrToken (ref : Name) (descr : String) (tok : String) : Highlighted :=
+    .token ⟨.keyword ref none (some descr), tok⟩
+
+@[inline_extension attr]
+def attr.descr : InlineDescr where
+  traverse _ _ _ := do
+    pure none
+  toTeX := none
+  extraCss := [highlightingStyle, docstringStyle]
+  extraJs := [highlightingJs]
+  toHtml :=
+    open Verso.Output.Html Verso.Doc.Html in
+    some <| fun _ _ data _ => do
+      match FromJson.fromJson? data with
+      | .error err =>
+        HtmlT.logError <| "Couldn't deserialize Lean attribute code while rendering HTML: " ++ err
+        pure .empty
+      | .ok (hl : Highlighted) =>
+        hl.inlineHtml "examples"

Manual/Meta/Example.lean

@@ -109,6 +109,9 @@ r#".example {
   font-style: italic;
   font-family: var(--verso-structure-font-family);
 }
+.example .hl.lean.block {
+  overflow-x: auto;
+}
 "#
   ]
 

Manual/Meta/Syntax.lean

@@ -22,6 +22,7 @@ namespace Manual
 --   let stx ← `(command|universe $xs*)
 --   dbg_trace stx
 
+-- TODO upstream this to enable cross-reference generation the usual Verso way
 def syntaxKindDomain := `Manual.syntaxKind
 
 def Block.syntax : Block where
@@ -36,6 +37,7 @@ def Inline.keywordOf : Inline where
 structure SyntaxConfig where
   name : Name
   «open» : Bool := true
+  label : String := "syntax"
   aliases : List Name := []
 
 structure KeywordOfConfig where
@@ -99,7 +101,7 @@ def keywordOf.descr : InlineDescr where
         content.mapM goI
   extraCss := [
 r#".keyword-of .kw {
-  font-weight: bold;
+  font-weight: 500;
 }
 .keyword-of .hover-info {
   display: none;
@@ -158,6 +160,7 @@ def SyntaxConfig.parse [Monad m] [MonadInfoTree m] [MonadLiftT CoreM m] [MonadEn
   SyntaxConfig.mk <$>
     .positional `name .name <*>
     ((·.getD true) <$> (.named `open .bool true)) <*>
+    ((·.getD "syntax") <$> .named `label .string true) <*>
     (many (.named `alias .resolvedName false) <* .done)
 
 inductive GrammarTag where
@@ -194,7 +197,7 @@ partial def «syntax» : DirectiveExpander
         firstGrammar := false
       | _ =>
         content := content.push <| ← elabBlock b
-    pure #[← `(Doc.Block.other {Block.syntax with data := ToJson.toJson (α := Name × Option Tag × Array Name) ($(quote config.name), none, $(quote config.aliases.toArray))} #[$content,*])]
+    pure #[← `(Doc.Block.other {Block.syntax with data := ToJson.toJson (α := Name × String × Option Tag × Array Name) ($(quote config.name), $(quote config.label), none, $(quote config.aliases.toArray))} #[$content,*])]
 where
   isGrammar? : Syntax → Option (Array Syntax × String × SourceInfo × Syntax × Syntax × SourceInfo × Syntax)
   | `<low|(Verso.Syntax.codeblock (column ~col@(.atom _ _col)) ~«open» ~(.node i `null #[nameStx, .node _ `null argsStx]) ~str@(.atom info contents) ~close )> =>
@@ -325,7 +328,7 @@ where
 @[block_extension «syntax»]
 def syntax.descr : BlockDescr where
   traverse id data contents := do
-    if let .ok (kind, tag, aliases) := FromJson.fromJson? (α := Name × Option Tag × Array Name) data then
+    if let .ok (kind, label, tag, aliases) := FromJson.fromJson? (α := Name × String × Option Tag × Array Name) data then
       modify fun st => st.saveDomainObject syntaxKindDomain kind.toString id
       for a in aliases do
         modify fun st => st.saveDomainObject syntaxKindDomain a.toString id
@@ -334,21 +337,27 @@ def syntax.descr : BlockDescr where
       else
         let path := (← read).path
         let tag ← Verso.Genre.Manual.externalTag id path kind.toString
-        pure <| some <| Block.other {Block.syntax with id := some id, data := toJson (kind, some tag, aliases)} contents
+        pure <| some <| Block.other {Block.syntax with id := some id, data := toJson (kind, label, some tag, aliases)} contents
     else
       logError "Couldn't deserialize kind name for syntax block"
       pure none
   toTeX := none
   toHtml :=
     open Verso.Output.Html Verso.Doc.Html in
-    some <| fun _ goB id _ content => do
+    some <| fun _ goB id data content => do
+      let label ←
+        match FromJson.fromJson? (α := Name × String × Option Tag × Array Name) data with
+        | .ok (_, label, _, _) => pure label
+        | .error e =>
+          HtmlT.logError s!"Failed to deserialize syntax docs: {e}"
+          pure "syntax"
       let xref ← HtmlT.state
       let attrs := match xref.externalTags[id]? with
         | none => #[]
         | some (_, t) => #[("id", t)]
       pure {{
         <div class="namedocs" {{attrs}}>
-          <span class="label">"syntax"</span>
+          <span class="label">{{label}}</span>
           <div class="text">
             {{← content.mapM goB}}
           </div>
@@ -359,7 +368,7 @@ def grammar := ()
 
 def grammarCss :=
 r#".grammar .keyword {
-  font-weight: bold;
+  font-weight: 500 !important;
 }
 .grammar .nonterminal {
   font-style: italic;