chore: fix core after rebootstrap

src/Lean/Elab/Command.lean

@@ -880,4 +880,22 @@ partial def withSetOptionIn (cmd : CommandElab) : CommandElab := fun stx => do
 
 export Elab.Command (Linter addLinter)
 
+namespace Parser.Command
+
+/--
+Returns syntax for `private` or `public` visibility depending on `isPublic`. This function should be
+used to generate visibility syntax for declarations that is independent of the presence of
+`public section`s.
+-/
+def visibility.ofBool (isPublic : Bool) : TSyntax ``visibility :=
+  Unhygienic.run <| if isPublic then `(visibility| public) else `(visibility| private)
+
+/--
+Returns syntax for `private` if `attrKind` is `local` and `public` otherwise.
+-/
+def visibility.ofAttrKind (attrKind : TSyntax ``Term.attrKind) : TSyntax ``visibility :=
+  visibility.ofBool <| !attrKind matches `(attrKind| local)
+
+end Parser.Command
+
 end Lean

src/Lean/Elab/DocString/Builtin/Scopes.lean

@@ -19,13 +19,15 @@ inductive DocScope where
   | import (mods : Array Name)
 
 private def imports := leading_parser sepBy1 ident ", "
+set_option compiler.relaxedMetaCheck true in
+private meta def importsM := imports
 
 instance : FromDocArg DocScope where
   fromDocArg v := private
     match v with
     | .str s => do
       let stx ← withRef s <| parseQuotedStrLit (whitespace >> imports.fn) s
-      let `(imports|$modNames,*) := stx
+      let `(importsM|$modNames,*) := stx
         | throwErrorAt stx "Expected comma-separated imports list, got `{stx}`"
       let modNames : Array Ident := modNames
       return .import (modNames.map (·.getId))

src/Lean/LibrarySuggestions/Default.lean

@@ -6,8 +6,7 @@ Authors: Kim Morrison
 module
 
 prelude
-public import Lean.LibrarySuggestions.SineQuaNon
-import all Lean.LibrarySuggestions.SineQuaNon
+public meta import Lean.LibrarySuggestions.SineQuaNon
 
 /-!
 # Default library suggestions engine

src/Lean/Parser/Command.lean

@@ -965,20 +965,6 @@ Note that the error name is not relativized to the current namespace.
 @[builtin_command_parser] def registerErrorExplanationStx := leading_parser
   optional docComment >> "register_error_explanation " >> ident >> termParser
 
-/--
-Returns syntax for `private` or `public` visibility depending on `isPublic`. This function should be
-used to generate visibility syntax for declarations that is independent of the presence of
-`public section`s.
--/
-def visibility.ofBool (isPublic : Bool) : TSyntax ``visibility :=
-  Unhygienic.run <| if isPublic then `(visibility| public) else `(visibility| private)
-
-/--
-Returns syntax for `private` if `attrKind` is `local` and `public` otherwise.
--/
-def visibility.ofAttrKind (attrKind : TSyntax ``Term.attrKind) : TSyntax ``visibility :=
-  visibility.ofBool <| !attrKind matches `(attrKind| local)
-
 end Command
 
 namespace Term

src/Lean/Parser/Module.lean

@@ -6,7 +6,8 @@ Authors: Leonardo de Moura, Sebastian Ullrich
 module
 
 prelude
-public import Lean.Parser.Command
+public import Lean.Parser.Module.Syntax
+meta import Lean.Parser.Module.Syntax
 import Init.While
 
 public section
@@ -15,26 +16,6 @@ namespace Lean
 namespace Parser
 
 namespace Module
-def moduleTk   := leading_parser "module"
-def «prelude»  := leading_parser "prelude"
-def «public»   := leading_parser (withAnonymousAntiquot := false) "public"
-def «meta»     := leading_parser (withAnonymousAntiquot := false) "meta"
-def «all»      := leading_parser (withAnonymousAntiquot := false) "all"
-def «import»   := leading_parser
-  atomic (optional «public» >> optional «meta» >> "import ") >>
-  optional all >>
-  identWithPartialTrailingDot
-def header     := leading_parser optional (moduleTk >> ppLine >> ppLine) >>
-  optional («prelude» >> ppLine) >>
-  many («import» >> ppLine) >>
-  ppLine
-
-/--
-  Parser for a Lean module. We never actually run this parser but instead use the imperative definitions below that
-  return the same syntax tree structure, but add error recovery. Still, it is helpful to have a `Parser` definition
-  for it in order to auto-generate helpers such as the pretty printer. -/
-@[run_builtin_parser_attribute_hooks]
-def module     := leading_parser header >> many (commandParser >> ppLine >> ppLine)
 
 def updateTokens (tokens : TokenTable) : TokenTable :=
   match addParserTokens tokens header.info with

src/Lean/Parser/Module/Syntax.lean

@@ -0,0 +1,36 @@
+/-
+Copyright (c) 2019 Microsoft Corporation. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Leonardo de Moura, Sebastian Ullrich
+-/
+module
+
+prelude
+public import Lean.Parser.Command
+
+public section
+
+namespace Lean
+namespace Parser
+
+namespace Module
+def moduleTk   := leading_parser "module"
+def «prelude»  := leading_parser "prelude"
+def «public»   := leading_parser (withAnonymousAntiquot := false) "public"
+def «meta»     := leading_parser (withAnonymousAntiquot := false) "meta"
+def «all»      := leading_parser (withAnonymousAntiquot := false) "all"
+def «import»   := leading_parser
+  atomic (optional «public» >> optional «meta» >> "import ") >>
+  optional all >>
+  identWithPartialTrailingDot
+def header     := leading_parser optional (moduleTk >> ppLine >> ppLine) >>
+  optional («prelude» >> ppLine) >>
+  many («import» >> ppLine) >>
+  ppLine
+
+/--
+  Parser for a Lean module. We never actually run this parser but instead use the imperative definitions in the parent module that
+  return the same syntax tree structure, but add error recovery. Still, it is helpful to have a `Parser` definition
+  for it in order to auto-generate helpers such as the pretty printer. -/
+@[run_builtin_parser_attribute_hooks]
+def module     := leading_parser header >> many (commandParser >> ppLine >> ppLine)

src/Lean/Parser/Term/Basic.lean

@@ -184,11 +184,14 @@ def binderTactic  := leading_parser
 def binderDefault := leading_parser
   " := " >> termParser
 
+set_option compiler.relaxedMetaCheck true in
+private meta def binderDefaultM := binderDefault
+
 open Lean.PrettyPrinter Parenthesizer Syntax.MonadTraverser in
 @[combinator_parenthesizer Lean.Parser.Term.binderDefault, expose] def binderDefault.parenthesizer : Parenthesizer := do
   let prec := match (← getCur) with
     -- must parenthesize to distinguish from `binderTactic`
-    | `(binderDefault| := by $_) => maxPrec
+    | `(binderDefaultM| := by $_) => maxPrec
     | _                          => 0
   visitArgs do
     term.parenthesizer prec

src/Lean/PrettyPrinter/Delaborator/Builtins.lean

@@ -9,10 +9,9 @@ prelude
 public import Lean.PrettyPrinter.Delaborator.Basic
 public import Lean.Meta.CoeAttr
 public import Lean.Meta.Structure
-import Lean.Parser.Command
 public import Lean.PrettyPrinter.Formatter
 public import Lean.PrettyPrinter.Parenthesizer
-meta import Lean.Parser.Do
+meta import Lean.Parser.Command
 
 public section
 
@@ -1547,7 +1546,7 @@ def delabSorry : Delab := whenPPOption getPPNotation <| whenNotPPOption getPPExp
 open Parser Command Term in
 @[run_builtin_parser_attribute_hooks]
 -- use `termParser` instead of `declId` so we can reuse `delabConst`
-def declSigWithId := leading_parser termParser maxPrec >> declSig
+private meta def declSigWithId := leading_parser termParser maxPrec >> declSig
 
 private unsafe def evalSyntaxConstantUnsafe (env : Environment) (opts : Options) (constName : Name) : ExceptT String Id Syntax :=
   env.evalConstCheck Syntax opts ``Syntax constName

src/Lean/Server/Rpc/Deriving.lean

@@ -57,7 +57,7 @@ private def deriveStructureInstance (indVal : InductiveVal) (params : Array Expr
         return { $decInits:structInstField,* }
   )
 
-private def matchAltTerm := Lean.Parser.Term.matchAlt (rhsParser := Lean.Parser.termParser)
+private meta def matchAltTerm := Lean.Parser.Term.matchAlt (rhsParser := Lean.Parser.termParser)
 private instance : Coe (TSyntax ``matchAltTerm) (TSyntax ``Parser.Term.matchAlt) where coe s := ⟨s⟩
 
 private def deriveInductiveInstance (indVal : InductiveVal) (params : Array Expr)