chore: minor module system fixes from batteries port (#10496)

Author: Kha

src/Lean/Compiler/LCNF/Visibility.lean

@@ -60,12 +60,14 @@ partial def markDeclPublicRec (phase : Phase) (decl : Decl) : CompilerM Unit :=
 partial def checkMeta (origDecl : Decl) : CompilerM Unit := do
   if !(← getEnv).header.isModule then
     return
-  let isMeta := isMeta (← getEnv) origDecl.name
+  let irPhases := getIRPhases (← getEnv) origDecl.name
+  if irPhases == .all then
+    return
   -- If the meta decl is public, we want to ensure it can only refer to public meta imports so that
   -- references to private imports cannot escape the current module. In particular, we check that
   -- decls with relevant global attrs are public (`Lean.ensureAttrDeclIsMeta`).
   let isPublic := !isPrivateName origDecl.name
-  go isMeta isPublic origDecl |>.run' {}
+  go (irPhases == .comptime) isPublic origDecl |>.run' {}
 where go (isMeta isPublic : Bool) (decl : Decl) : StateT NameSet CompilerM Unit := do
   decl.value.forCodeM fun code =>
     for ref in collectUsedDecls code do
@@ -129,9 +131,9 @@ partial def checkTemplateVisibility : Pass where
         -- indirectly via a public template-like, we do a recursive check when checking the latter.
         if !isPrivateName decl.name && (← decl.isTemplateLike) then
           let isMeta := isMeta (← getEnv) decl.name
-          go isMeta decl decl |>.run' {}
+          go decl decl |>.run' {}
     return decls
-where go (isMeta : Bool) (origDecl decl : Decl) : StateT NameSet CompilerM Unit := do
+where go (origDecl decl : Decl) : StateT NameSet CompilerM Unit := do
   decl.value.forCodeM fun code =>
     for ref in collectUsedDecls code do
       if (← get).contains ref then
@@ -140,7 +142,7 @@ where go (isMeta : Bool) (origDecl decl : Decl) : StateT NameSet CompilerM Unit
       if let some localDecl := baseExt.getState (← getEnv) |>.find? ref then
         -- check transitively through local decls
         if isPrivateName localDecl.name && (← localDecl.isTemplateLike) then
-          go isMeta origDecl localDecl
+          go origDecl localDecl
       else if let some modIdx := (← getEnv).getModuleIdxFor? ref then
         if (← getEnv).header.modules[modIdx]?.any (!·.isExported) then
           throwError "Cannot compile inline/specializing declaration `{.ofConstName origDecl.name}` as \

src/Lean/DocString/Formatter.lean

@@ -7,7 +7,7 @@ Authors: David Thrane Christiansen
 module
 prelude
 public import Lean.PrettyPrinter.Formatter
-import Lean.DocString.Syntax
+import Lean.DocString.Parser
 
 
 namespace Lean.Doc.Parser
@@ -204,7 +204,7 @@ def formatMetadata : Formatter := do
     pushLine
     visitAtom .anonymous
     pushLine
-    metadataContents.formatter
+    Parser.metadataContents.formatter
     pushLine
     visitAtom .anonymous
 

src/Lean/DocString/Parser.lean

@@ -804,7 +804,9 @@ Parses a line of text (that is, one or more inline elements).
 def textLine (allowNewlines := true) : ParserFn := many1Fn (inline { allowNewlines })
 
 open Lean.Parser.Term in
-def metadataContents : Parser :=
+/-- A non-`meta` copy of `Lean.Doc.Syntax.metadataContents`. -/
+@[run_builtin_parser_attribute_hooks]
+public def metadataContents : Parser :=
   structInstFields (sepByIndent structInstField ", " (allowTrailingSep := true))
 
 def withPercents : ParserFn → ParserFn := fun p =>

src/Lean/Elab/BuiltinCommand.lean

@@ -39,30 +39,31 @@ namespace Lean.Elab.Command
   | _ => throwErrorAt stx "unexpected module doc string{indentD <| stx}"
 
 private def addScope (isNewNamespace : Bool) (header : String) (newNamespace : Name)
-    (isNoncomputable isPublic : Bool := false) (attrs : List (TSyntax ``Parser.Term.attrInstance) := []) :
+    (isNoncomputable isPublic isMeta : Bool := false) (attrs : List (TSyntax ``Parser.Term.attrInstance) := []) :
     CommandElabM Unit := do
   modify fun s => { s with
     env    := s.env.registerNamespace newNamespace,
     scopes := { s.scopes.head! with
       header := header, currNamespace := newNamespace
       isNoncomputable := s.scopes.head!.isNoncomputable || isNoncomputable
       isPublic := s.scopes.head!.isPublic || isPublic
+      isMeta := s.scopes.head!.isMeta || isMeta
       attrs := s.scopes.head!.attrs ++ attrs
     } :: s.scopes
   }
   pushScope
   if isNewNamespace then
     activateScoped newNamespace
 
-private def addScopes (header : Name) (isNewNamespace : Bool) (isNoncomputable isPublic : Bool := false)
+private def addScopes (header : Name) (isNewNamespace : Bool) (isNoncomputable isPublic isMeta : Bool := false)
     (attrs : List (TSyntax ``Parser.Term.attrInstance) := []) : CommandElabM Unit :=
   go header
 where go
   | .anonymous => pure ()
   | .str p header => do
     go p
     let currNamespace ← getCurrNamespace
-    addScope isNewNamespace header (if isNewNamespace then Name.mkStr currNamespace header else currNamespace) isNoncomputable isPublic attrs
+    addScope isNewNamespace header (if isNewNamespace then Name.mkStr currNamespace header else currNamespace) isNoncomputable isPublic isMeta attrs
   | _ => throwError "invalid scope"
 
 private def addNamespace (header : Name) : CommandElabM Unit :=
@@ -99,16 +100,16 @@ private def checkEndHeader : Name → List Scope → Option Name
 
 @[builtin_command_elab «section»] def elabSection : CommandElab := fun stx => do
   match stx with
-  | `(Parser.Command.section| $[@[expose%$expTk]]? $[public%$publicTk]? $[noncomputable%$ncTk]? section $(header?)?) =>
+  | `(Parser.Command.section| $[@[expose%$expTk]]? $[public%$publicTk]? $[noncomputable%$ncTk]? $[meta%$metaTk]? section $(header?)?) =>
     -- TODO: allow more attributes?
     let attrs ← if expTk.isSome then
       pure [← `(Parser.Term.attrInstance| expose)]
     else
       pure []
     if let some header := header? then
-      addScopes (isNewNamespace := false) (isNoncomputable := ncTk.isSome) (isPublic := publicTk.isSome) (attrs := attrs) header.getId
+      addScopes (isNewNamespace := false) (isNoncomputable := ncTk.isSome) (isPublic := publicTk.isSome) (isMeta := metaTk.isSome) (attrs := attrs) header.getId
     else
-      addScope (isNewNamespace := false) (isNoncomputable := ncTk.isSome) (isPublic := publicTk.isSome) (attrs := attrs) "" (← getCurrNamespace)
+      addScope (isNewNamespace := false) (isNoncomputable := ncTk.isSome) (isPublic := publicTk.isSome) (isMeta := metaTk.isSome) (attrs := attrs) "" (← getCurrNamespace)
   | _                        => throwUnsupportedSyntax
 
 @[builtin_command_elab InternalSyntax.end_local_scope] def elabEndLocalScope : CommandElab := fun _ => do

src/Lean/Elab/Deriving/Basic.lean

@@ -164,9 +164,10 @@ def processDefDeriving (view : DerivingClassView) (decl : Expr) : TermElabM Unit
   let decl ← whnfCore decl
   let .const declName _ := decl.getAppFn
     | throwError "Failed to delta derive instance, expecting a term of the form `C ...` where `C` is a constant, given{indentExpr decl}"
-  -- When the definition is private, the deriving handler will need access to the private scope,
-  -- and we make sure to put the instance in the private scope.
-  withoutExporting (when := isPrivateName declName) do
+  let unexposed := (← getEnv).setExporting true |>.find? declName |>.all (!·.hasValue)
+  -- When the definition body is private, the deriving handler will need access to the private scope,
+  -- and the instance body will automatically be private as well.
+  withoutExporting (when := unexposed) do
   let ConstantInfo.defnInfo info ← getConstInfo declName
     | throwError "Failed to delta derive instance, `{.ofConstName declName}` is not a definition."
   let value := info.value.beta decl.getAppArgs
@@ -264,7 +265,7 @@ def getOptDerivingClasses (optDeriving : Syntax) : CoreM (Array DerivingClassVie
 
 def DerivingClassView.applyHandlers (view : DerivingClassView) (declNames : Array Name) : CommandElabM Unit := do
   let env ← getEnv
-  withScope (fun sc => { sc with isMeta := declNames.all (isMeta env) }) do
+  withScope (fun sc => { sc with isMeta := sc.isMeta || declNames.all (isMeta env) }) do
   withRef view.ref do
     applyDerivingHandlers (setExpose := view.hasExpose) (← liftCoreM <| view.getClassName) declNames
 

src/Lean/Elab/MutualDef.lean

@@ -1293,7 +1293,7 @@ where
 
     withoutExporting (when :=
       headers.all (fun header =>
-        header.modifiers.isMeta ||
+        header.modifiers.isMeta && !header.modifiers.attrs.any (·.name == `expose) ||
         header.modifiers.attrs.any (·.name == `no_expose) ||
         (!(header.kind == .def && sc.attrs.any (· matches `(attrInstance| expose))) &&
          !header.modifiers.attrs.any (·.name == `expose) &&
@@ -1368,7 +1368,7 @@ where
             and the parameters in the declaration, so for now we do not allow `classStx`
             to refer to section variables that were not included.
             -/
-            let info ← getConstInfo header.declName
+            let info ← withoutExporting <| getConstInfo header.declName
             lambdaTelescope info.value! fun xs _ => do
               let decl := mkAppN (.const header.declName (info.levelParams.map mkLevelParam)) xs
               processDefDeriving view decl

src/Lean/Parser/Command.lean

@@ -264,7 +264,8 @@ def «structure»          := leading_parser
 def sectionHeader := leading_parser
   optional ("@[" >> nonReservedSymbol "expose" >> "] ") >>
   optional ("public ") >>
-  optional ("noncomputable ")
+  optional ("noncomputable ") >>
+  optional ("meta ")
 /--
 A `section`/`end` pair delimits the scope of `variable`, `include`, `open`, `set_option`, and `local`
 commands. Sections can be nested. `section <id>` provides a label to the section that has to appear

src/Lean/ParserCompiler.lean

@@ -107,6 +107,10 @@ partial def compileParserExpr (e : Expr) : MetaM Expr := do
           name := c', levelParams := []
           type := ty, value := value, hints := ReducibilityHints.opaque, safety := DefinitionSafety.safe
         }
+        -- usually `meta` is infered during compilation for auxiliary definitions, but as
+        -- `ctx.combinatorAttr` may enforce correct use of the modifier, infer now.
+        if isMeta (← getEnv) c then
+          modifyEnv (addMeta · c')
         addAndCompile decl
         modifyEnv (ctx.combinatorAttr.setDeclFor · c c')
         if cinfo.type.isConst then

tests/lean/StxQuot.lean.expected.out

@@ -34,8 +34,8 @@ StxQuot.lean:19:15-19:16: error: unexpected token ']'; expected term
 "#[(Term.matchAlt \"|\" [[`[email protected]._hyg.1]] \"=>\" (num \"1\")), (Term.matchAlt \"|\" [[(Term.hole \"_\")]] \"=>\" (num \"2\"))]"
 "(Term.structInst\n \"{\"\n []\n (Term.structInstFields\n  [(Term.structInstField\n    (Term.structInstLVal `[email protected]._hyg.1 [])\n    [[] [] (Term.structInstFieldDef \":=\" [] `[email protected]._hyg.1)])])\n (Term.optEllipsis [])\n [\":\" `[email protected]._hyg.1]\n \"}\")"
 "(Term.structInst\n \"{\"\n []\n (Term.structInstFields\n  [(Term.structInstField\n    (Term.structInstLVal `[email protected]._hyg.1 [])\n    [[] [] (Term.structInstFieldDef \":=\" [] `[email protected]._hyg.1)])])\n (Term.optEllipsis [])\n []\n \"}\")"
-"(Command.section (Command.sectionHeader [] [] []) \"section\" [])"
-"(Command.section (Command.sectionHeader [] [] []) \"section\" [`[email protected]._hyg.1])"
+"(Command.section (Command.sectionHeader [] [] [] []) \"section\" [])"
+"(Command.section (Command.sectionHeader [] [] [] []) \"section\" [`[email protected]._hyg.1])"
 "(Term.match\n \"match\"\n []\n []\n [(Term.matchDiscr [] `[email protected]._hyg.1)]\n \"with\"\n (Term.matchAlts\n  [(Term.matchAlt \"|\" [[`[email protected]._hyg.1]] \"=>\" `[email protected]._hyg.1)\n   (Term.matchAlt\n    \"|\"\n    [[(«term_+_» `[email protected]._hyg.1 \"+\" (num \"1\"))]]\n    \"=>\"\n    («term_+_» `[email protected]._hyg.1 \"+\" (num \"1\")))]))"
 "(Term.match\n \"match\"\n []\n []\n [(Term.matchDiscr [] `[email protected]._hyg.1)]\n \"with\"\n (Term.matchAlts\n  [(Term.matchAlt \"|\" [[`[email protected]._hyg.1]] \"=>\" `[email protected]._hyg.1)\n   (Term.matchAlt\n    \"|\"\n    [[(«term_+_» `[email protected]._hyg.1 \"+\" (num \"1\"))]]\n    \"=>\"\n    («term_+_» `[email protected]._hyg.1 \"+\" (num \"1\")))]))"
 "#[`[email protected]._hyg.1, `[email protected]._hyg.1]"