feat: tactics chapter (leanprover#34)

Main.lean

@@ -6,13 +6,12 @@ open Verso.Genre.Manual
 
 
 def main :=
-  manualMain (%doc Manual)
-    (config := config)
+  manualMain (%doc Manual) (config := config)
 where
   config := {
     extraFiles := [("static", "static")],
-    extraCss := ["/static/colors.css", "/static/theme.css", "/static/inter/inter.css", "/static/firacode/fira_code.css", "/static/katex/katex.min.css"],
-    extraJs := ["/static/katex/katex.min.js", "/static/math.js"]
+    extraCss := ["/static/colors.css", "/static/theme.css", "/static/print.css", "/static/inter/inter.css", "/static/firacode/fira_code.css", "/static/katex/katex.min.css"],
+    extraJs := ["/static/katex/katex.min.js", "/static/math.js", "/static/print.js"]
     emitTeX := false
-    emitHtmlSingle := false
+    emitHtmlSingle := true -- for proofreading
   }

Manual.lean

@@ -3,6 +3,9 @@ import VersoManual
 import Manual.Intro
 import Manual.Elaboration
 import Manual.Language
+import Manual.Terms
+import Manual.Tactics
+import Manual.Simp
 import Manual.BuiltInTypes
 
 open Verso.Genre Manual
@@ -21,14 +24,42 @@ authors := ["Lean Developers"]
 
 {include Manual.Language}
 
-{include Manual.BuiltInTypes}
+{include Manual.Terms}
+
+# Monads and `do`-Notation
+
+# IO
+
+{include 0 Manual.Tactics}
+
+{include 0 Manual.Simp}
+
+{include 0 Manual.BuiltInTypes}
+
+# Notations and Macros
+
+:::planned
+A presentation of macros, covering
+ * `notation`
+ * Definition of {deftech}_macro_
+ * Syntax extension and syntax categories
+   * Precedence
+ * `macro_rules`
+   * Syntax patterns
+   * Backtracking on expansion failure
+ * {deftech}[Hygiene] and quotation
+ * The `macro` command
+:::
+
+# Lake and Reservoir
+
 
 
 # Progress
 
 :::progress
 ```namespace
-String Char Nat
+String Char Nat Lean.Elab.Tactic
 ```
 ```exceptions
 String.revFindAux String.extract.go₂ String.substrEq.loop String.casesOn
@@ -98,6 +129,136 @@ Nat.le.below.refl
 Nat.le.below.casesOn
 ```
 
+```exceptions
+Lean.Elab.Tactic.evalUnfold.go
+Lean.Elab.Tactic.dsimpLocation.go
+Lean.Elab.Tactic.withCollectingNewGoalsFrom.go
+Lean.Elab.Tactic.evalRunTac.unsafe_impl_1
+Lean.Elab.Tactic.evalRunTac.unsafe_1
+Lean.Elab.Tactic.evalTactic.handleEx
+Lean.Elab.Tactic.simpLocation.go
+Lean.Elab.Tactic.instToSnapshotTreeTacticParsedSnapshot.go
+Lean.Elab.Tactic.dsimpLocation'.go
+Lean.Elab.Tactic.withRWRulesSeq.go
+Lean.Elab.Tactic.runTermElab.go
+Lean.Elab.Tactic.getMainGoal.loop
+Lean.Elab.Tactic.elabSimpArgs.isSimproc?
+Lean.Elab.Tactic.elabSimpArgs.resolveSimpIdTheorem?
+Lean.Elab.Tactic.tactic.dbg_cache
+Lean.Elab.Tactic.tactic.simp.trace
+Lean.Elab.Tactic.liftMetaTacticAux
+```
+
+```exceptions
+
+Lean.Elab.Tactic.elabSetOption
+Lean.Elab.Tactic.evalSeq1
+Lean.Elab.Tactic.evalSimp
+Lean.Elab.Tactic.evalSpecialize
+Lean.Elab.Tactic.evalTacticAt
+Lean.Elab.Tactic.evalSimpAll
+Lean.Elab.Tactic.evalIntro.introStep
+Lean.Elab.Tactic.evalDone
+Lean.Elab.Tactic.evalRevert
+Lean.Elab.Tactic.evalRight
+Lean.Elab.Tactic.evalUnfold
+Lean.Elab.Tactic.evalConstructor
+Lean.Elab.Tactic.evalTacticCDot
+Lean.Elab.Tactic.evalTraceMessage
+Lean.Elab.Tactic.evalClear
+Lean.Elab.Tactic.evalIntroMatch
+Lean.Elab.Tactic.evalInduction
+Lean.Elab.Tactic.evalApply
+Lean.Elab.Tactic.evalUnknown
+Lean.Elab.Tactic.evalRefl
+Lean.Elab.Tactic.evalTactic.throwExs
+Lean.Elab.Tactic.evalDSimp
+Lean.Elab.Tactic.evalSepTactics.goEven
+Lean.Elab.Tactic.evalAllGoals
+Lean.Elab.Tactic.evalSplit
+Lean.Elab.Tactic.evalInjection
+Lean.Elab.Tactic.evalParen
+Lean.Elab.Tactic.evalFocus
+Lean.Elab.Tactic.evalLeft
+Lean.Elab.Tactic.evalRotateRight
+Lean.Elab.Tactic.evalWithReducible
+Lean.Elab.Tactic.evalTactic.expandEval
+Lean.Elab.Tactic.evalTraceState
+Lean.Elab.Tactic.evalCase'
+Lean.Elab.Tactic.evalSepTactics.goOdd
+Lean.Elab.Tactic.evalWithReducibleAndInstances
+Lean.Elab.Tactic.evalTacticSeqBracketed
+Lean.Elab.Tactic.evalTactic.eval
+Lean.Elab.Tactic.evalAlt
+Lean.Elab.Tactic.evalGeneralize
+Lean.Elab.Tactic.evalRewriteSeq
+Lean.Elab.Tactic.evalSleep
+Lean.Elab.Tactic.evalDSimpTrace
+Lean.Elab.Tactic.evalReplace
+Lean.Elab.Tactic.evalOpen
+Lean.Elab.Tactic.evalAssumption
+Lean.Elab.Tactic.evalSepTactics
+Lean.Elab.Tactic.evalWithUnfoldingAll
+Lean.Elab.Tactic.evalMatch
+Lean.Elab.Tactic.evalRepeat1'
+Lean.Elab.Tactic.evalFailIfSuccess
+Lean.Elab.Tactic.evalRename
+Lean.Elab.Tactic.evalFirst.loop
+Lean.Elab.Tactic.evalSimpTrace
+Lean.Elab.Tactic.evalFirst
+Lean.Elab.Tactic.evalSubstVars
+Lean.Elab.Tactic.evalRunTac
+Lean.Elab.Tactic.evalSymmSaturate
+Lean.Elab.Tactic.evalWithAnnotateState
+Lean.Elab.Tactic.evalTacticAtRaw
+Lean.Elab.Tactic.evalDbgTrace
+Lean.Elab.Tactic.evalSubst
+Lean.Elab.Tactic.evalNativeDecide
+Lean.Elab.Tactic.evalCalc
+Lean.Elab.Tactic.evalCase
+Lean.Elab.Tactic.evalRepeat'
+Lean.Elab.Tactic.evalRefine
+Lean.Elab.Tactic.evalContradiction
+Lean.Elab.Tactic.evalSymm
+Lean.Elab.Tactic.evalInjections
+Lean.Elab.Tactic.evalExact
+Lean.Elab.Tactic.evalRotateLeft
+Lean.Elab.Tactic.evalFail
+Lean.Elab.Tactic.evalTactic
+Lean.Elab.Tactic.evalSimpAllTrace
+Lean.Elab.Tactic.evalRefine'
+Lean.Elab.Tactic.evalChoice
+Lean.Elab.Tactic.evalInduction.checkTargets
+Lean.Elab.Tactic.evalIntro
+Lean.Elab.Tactic.evalAnyGoals
+Lean.Elab.Tactic.evalCases
+Lean.Elab.Tactic.evalDelta
+Lean.Elab.Tactic.evalDecide
+Lean.Elab.Tactic.evalChoiceAux
+Lean.Elab.Tactic.evalTacticSeq
+Lean.Elab.Tactic.evalCheckpoint
+Lean.Elab.Tactic.evalRenameInaccessibles
+Lean.Elab.Tactic.evalIntros
+Lean.Elab.Tactic.evalApplyLikeTactic
+Lean.Elab.Tactic.evalSkip
+Lean.Elab.Tactic.evalCalc.throwFailed
+Lean.Elab.Tactic.evalSubstEqs
+Lean.Elab.Tactic.evalTacticSeq1Indented
+```
+
+```exceptions
+List.tacticSizeOf_list_dec
+Lean.Parser.Tactic.tacticRefine_lift_
+Lean.Parser.Tactic.tacticRefine_lift'_
+Array.tacticArray_mem_dec
+Lean.Parser.Tactic.normCast0
+tacticClean_wf
+Lean.Parser.Tactic.nestedTactic
+Lean.Parser.Tactic.unknown
+Lean.Parser.Tactic.paren
+tacticDecreasing_trivial_pre_omega
+```
+
 :::
 
 

Manual/Elaboration.lean

@@ -11,7 +11,7 @@ set_option pp.rawOnError true
 :::planned
 
 
- * Describe the roles of the kernel, the interpreter, the compiler, the {deftech key:="elaborate"}[elaborator], and how they interact
+ * 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?
 

Manual/Language.lean

@@ -39,6 +39,9 @@ Topics:
 :::
 
 ## Propositions
+%%%
+tag := "propositions"
+%%%
 
 {deftech}[Propositions] are meaningful statements that admit proof. {index}[proposition]
 Nonsensical statements are not propositions, but false statements are.

Manual/Meta.lean

@@ -11,11 +11,13 @@ import SubVerso.Highlighting
 import SubVerso.Examples
 
 import Manual.Meta.Basic
+import Manual.Meta.CustomStyle
 import Manual.Meta.Example
 import Manual.Meta.Figure
 import Manual.Meta.Lean
 import Manual.Meta.Marginalia
 import Manual.Meta.Syntax
+import Manual.Meta.Tactics
 
 open Lean Elab
 open Verso ArgParse Doc Elab Genre.Manual Html Code Highlighted.WebAssets

Manual/Meta/CustomStyle.lean

@@ -0,0 +1,35 @@
+import VersoManual
+import Lean.Data.Json
+
+open Verso Doc Elab Output Html Code
+open Verso.Genre Manual
+open Verso.ArgParse
+open Lean
+
+namespace Manual
+
+
+def Block.CSS : Block where
+  name := `Manual.CSS
+
+@[code_block_expander CSS]
+def CSS : CodeBlockExpander
+  | args, str => do
+    let () ← ArgParse.done.run args
+    pure #[← `(Doc.Block.other {Block.CSS with data := ToJson.toJson (α := String) $(quote str.getString)} #[])]
+
+@[block_extension Manual.CSS]
+def CSS.descr : BlockDescr where
+  traverse _ _ _ := pure none
+  toTeX := none
+  toHtml :=
+    open Verso.Output.Html in
+    some <| fun _ _ _ data _ => do
+      match FromJson.fromJson? data with
+      | .error err =>
+        HtmlT.logError <| "Couldn't deserialize CSS while rendering HTML: " ++ err
+        pure .empty
+      | .ok (css : String) =>
+        pure {{
+          <style>{{css}}</style>
+        }}