doc: meta modifier (#10554)

Author: Kha

src/Lean/Parser/Command.lean

@@ -72,6 +72,26 @@ def visibility       :=
   withAntiquot (mkAntiquot "visibility" decl_name% (isPseudoKind := true)) <|
     «private» <|> «public»
 def «protected»      := leading_parser "protected "
+/--
+(module system) The `meta` modifier can be applied to a `def` in order to make it available for
+compile-time execution, e.g. as part of a macro or tactic. Specifically, attributes such as
+`@[macro]` require the annotated declaration to be `meta`, and recursively a `meta` definition may
+only refer to other `meta` definitions unless the reference is irrelevant for compilation purposes.
+However, imported definitions not originally marked `meta`, such as most parts of the standard
+library, can be retroactively be marked so during importing to allow their use in `meta`
+definitions. If the metaprogramming use is local to the current module, such as through
+`local macro`, this can be done by `meta import`; if the metaprogram is available to other modules
+as well, `public meta import` is required.
+
+Conversely, `meta def` makes the definition unavailable for run-time use, e.g. as part of a
+`lean_exe` executable generated by Lake. Thus `def`s that are not marked `meta` (nor
+`noncomputable`) may not refer to `meta def`s either in compilation-relevant ways. There is no way
+to remove the `meta` modifier retroactively. For any potential mixed use of a definition, it should
+be defined without `meta` and then imported with the correct modifier as needed. In particular,
+the same module can be `import`ed and `meta import`ed at once in order to make such regular `def`s
+available in both `meta` and non-`meta` `def`s.
+-/
+@[builtin_doc]
 def «meta»           := leading_parser "meta "
 def «noncomputable»  := leading_parser "noncomputable "
 def «unsafe»         := leading_parser "unsafe "
@@ -92,7 +112,7 @@ All modifiers are optional, and have to come in the listed order.
 `nestedDeclModifiers` is the same as `declModifiers`, but attributes are printed
 on the same line as the declaration. It is used for declarations nested inside other syntax,
 such as inductive constructors, structure projections, and `let rec` / `where` definitions. -/
-@[builtin_doc] def declModifiers (inline : Bool) := leading_parser
+def declModifiers (inline : Bool) := leading_parser
   optional docComment >>
   optional (Term.«attributes» >> if inline then skip else ppDedent ppLine) >>
   optional visibility >>