doc: port mvcgen documentation to vcgen and Std.WP

Manual.lean

@@ -31,6 +31,7 @@ import Manual.Namespaces
 import Manual.Runtime
 import Manual.SupportedPlatforms
 import Manual.VCGen
+import Manual.MVCGen
 
 open Verso.Genre Manual
 open Verso.Genre.Manual.InlineLean
@@ -100,6 +101,8 @@ Thus, this reference manual does not draw a barrier between the two aspects, but
 
 {include 0 Manual.VCGen}
 
+{include 0 Manual.MVCGen}
+
 {include 0 Manual.Monads}
 
 {include 0 Manual.BasicProps}

Manual/BuildTools/Lake.lean

@@ -763,6 +763,7 @@ root = "Tests"
       libPrefixOnWindows := false,
       allowImportAll := false,
       builtinLint? := none,
+      checks := #[],
       fixedToolchain := false},
   configFile := FilePath.mk "lakefile",
   relConfigFile := FilePath.mk "lakefile",
@@ -927,6 +928,7 @@ lean_exe «my-package-tests» where
       libPrefixOnWindows := false,
       allowImportAll := false,
       builtinLint? := none,
+      checks := #[],
       fixedToolchain := false},
   configFile := FilePath.mk "lakefile.lean",
   relConfigFile := FilePath.mk "lakefile.lean",
@@ -1131,6 +1133,7 @@ root = "Lint"
       libPrefixOnWindows := false,
       allowImportAll := false,
       builtinLint? := none,
+      checks := #[],
       fixedToolchain := false},
   configFile := FilePath.mk "lakefile",
   relConfigFile := FilePath.mk "lakefile",
@@ -1296,6 +1299,7 @@ lean_exe «my-package-lint» where
       libPrefixOnWindows := false,
       allowImportAll := false,
       builtinLint? := none,
+      checks := #[],
       fixedToolchain := false},
   configFile := FilePath.mk "lakefile.lean",
   relConfigFile := FilePath.mk "lakefile.lean",

Manual/BuildTools/Lake/CLI.lean

@@ -895,6 +895,9 @@ OPTIONS:
   --code-quality        records each linter warning as a code quality check result
                         and runs the registered code quality checks.
                         Setting this flag will skip lint driver.
+  --checks <mods>       comma-separated list of workspace modules providing
+                        package code quality checks; they are imported
+                        alongside each linted module (implies --code-quality)
 
 A lint driver can be configured by either setting the `lintDriver` package
 configuration option or by tagging a script or executable `@[lint_driver]`.

Manual/BuildTools/Lake/Config.lean

@@ -193,6 +193,7 @@ name = "example-package"
       libPrefixOnWindows := false,
       allowImportAll := false,
       builtinLint? := none,
+      checks := #[],
       fixedToolchain := false},
   configFile := FilePath.mk "lakefile",
   relConfigFile := FilePath.mk "lakefile",
@@ -284,6 +285,7 @@ name = "Sorting"
       libPrefixOnWindows := false,
       allowImportAll := false,
       builtinLint? := none,
+      checks := #[],
       fixedToolchain := false},
   configFile := FilePath.mk "lakefile",
   relConfigFile := FilePath.mk "lakefile",