feat: list mvcgen and stateful proof mode tactics in tactic reference (#566)

This PR lists `mvcgen` and the stateful proof mode tactics in tactic
reference.

---------

Co-authored-by: David Thrane Christiansen <[email protected]>

Author: sgraf812

.gitignore

@@ -1,4 +1,5 @@
 /.lake
+/.direnv
 /_out/
 .DS_Store
 figures/lake.trace

Manual/Meta/ErrorExplanation.lean

@@ -13,7 +13,8 @@ import Lean.ErrorExplanations
 import PreprocessedExplanations
 
 open Lean Elab
-open Verso.ArgParse
+open Verso (ArgParse)
+open Verso.ArgParse (parseThe)
 open Verso.Doc Elab
 open Verso.Genre.Manual Markdown InlineLean
 open SubVerso.Highlighting

Manual/Meta/LexedText.lean

@@ -134,13 +134,12 @@ def Inline.c (value : LexedText) : Inline where
 
 def lexedText := ()
 
-@[code_block_expander c]
-def c : CodeBlockExpander
-  | args, str => do
-    ArgParse.done.run args
+@[code_block]
+def c : CodeBlockExpanderOf Unit
+  | (), str => do
     let codeStr := str.getString
     let toks ← LexedText.highlight hlC codeStr
-    pure #[← ``(Block.other (Block.c $(quote toks)) #[Block.code $(quote codeStr)])]
+    ``(Block.other (Block.c $(quote toks)) #[Block.code $(quote codeStr)])
 
 open Verso.Output Html in
 open Verso.Doc.Html in
@@ -166,14 +165,13 @@ def c.idescr : InlineDescr where
     pure {{<code class="c">{{v.toHtml}}</code>}}
   extraCss := [c.css]
 
-@[role_expander c]
-def cInline : RoleExpander
-  | args, contents => do
-    ArgParse.done.run args
+@[role c]
+def cInline : RoleExpanderOf Unit
+  | (), contents => do
     let #[x] := contents
       | throwError "Expected exactly one parameter"
     let `(inline|code($str)) := x
       | throwError "Expected exactly one code item"
     let codeStr := str.getString
     let toks ← LexedText.highlight hlC codeStr
-    pure #[← ``(Inline.other (Inline.c $(quote toks)) #[Inline.code $(quote codeStr)])]
+    ``(Inline.other (Inline.c $(quote toks)) #[Inline.code $(quote codeStr)])

Manual/Tactics/Reference.lean

@@ -660,3 +660,104 @@ tag := "tactic-ref-other"
 
 :::tactic Lean.Parser.Tactic.runTac
 :::
+
+# Verification Condition Generation
+%%%
+tag := "tactic-ref-mvcgen"
+%%%
+
+:::tactic "mvcgen"
+:::
+
+## Tactics for Stateful Goals in `Std.Do.SPred`
+%%%
+tag := "tactic-ref-spred"
+%%%
+
+### Starting and Stopping the Proof Mode
+
+:::tactic "mstart"
+:::
+
+:::tactic "mstop"
+:::
+
+:::TODO
+Next release:
+```
+:::tactic "mleave"
+:::
+```
+:::
+
+### Proving a Stateful Goal
+
+:::tactic "mspec"
+:::
+
+:::tactic "mintro"
+:::
+
+:::tactic "mexact"
+:::
+
+:::tactic "massumption"
+:::
+
+:::tactic "mrefine"
+:::
+
+:::tactic "mconstructor"
+:::
+
+:::tactic "mleft"
+:::
+
+:::tactic "mright"
+:::
+
+:::tactic "mexists"
+:::
+
+:::tactic "mpure_intro"
+:::
+
+:::tactic "mexfalso"
+:::
+
+### Manipulating Stateful Hypotheses
+
+:::tactic "mclear"
+:::
+
+:::tactic "mdup"
+:::
+
+:::tactic "mhave"
+:::
+
+:::tactic "mreplace"
+:::
+
+:::tactic "mspecialize"
+:::
+
+:::tactic "mspecialize_pure"
+:::
+
+:::tactic "mcases"
+:::
+
+:::TODO
+Next release:
+```
+:::tactic "mrename_i"
+:::
+```
+:::
+
+:::tactic "mpure"
+:::
+
+:::tactic "mframe"
+:::

flake.nix

@@ -8,8 +8,9 @@
     { devShell.${system} = pkgs.stdenv.mkDerivation rec {
       name = "env";
       buildInputs = with pkgs; [
-        elan
+        #elan # Should be installed manually
         python3
+        poppler_utils
       ];
    };};
 }

lake-manifest.json

@@ -5,10 +5,10 @@
    "type": "git",
    "subDir": null,
    "scope": "",
-   "rev": "77828b7a94f9406083bcbb1551ce9b81bac7e4ec",
+   "rev": "78002a2a5c6012e2aee9e680b646dddbaa0a900d",
    "name": "verso",
    "manifestFile": "lake-manifest.json",
-   "inputRev": "v4.23.0-rc2",
+   "inputRev": "main",
    "inherited": false,
    "configFile": "lakefile.lean"},
   {"url": "https://github.com/acmepjz/md4lean",

lakefile.lean

@@ -8,7 +8,7 @@ import Lake
 open Lake DSL
 open System (FilePath)
 
-require verso from git "https://github.com/leanprover/verso.git"@"v4.23.0-rc2"
+require verso from git "https://github.com/leanprover/verso.git"@"main"
 
 package "verso-manual" where
   -- building the C code cost much more than the optimizations save