refactor: move import validation to parser & Lake (#9716)

This PR moves the validation of cross-package `import all` to Lake and
the syntax validation of import keywords (`public`, `meta`, and `all`)
to the two import parsers.

It also fixes the error reporting of the fast import parser
(`Lean.parseImports`) and adds positions to its errors.

src/Lean/Elab/Import.lean

@@ -56,11 +56,6 @@ def processHeaderCore
   else
     .private
   let (env, messages) ← try
-    for i in imports do
-      if !isModule && i.importAll then
-        throw <| .userError "cannot use `import all` without `module`"
-      if i.importAll && mainModule.getRoot != i.module.getRoot then
-        throw <| .userError "cannot use `import all` across module path roots"
     let env ←
       importModules (leakEnv := leakEnv) (loadExts := true) (level := level)
         imports opts trustLevel plugins arts

src/Lean/Elab/ParseImportsFast.lean

@@ -1,7 +1,7 @@
 /-
 Copyright (c) 2022 Microsoft Corporation. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
-Authors: Leonardo de Moura
+Authors: Leonardo de Moura, Sebastian Ullrich, Mac Malone
 -/
 module
 
@@ -16,6 +16,7 @@ namespace ParseImports
 structure State where
   imports       : Array Import := #[]
   pos           : String.Pos := 0
+  badModifier   : Bool := false
   error?        : Option String := none
   isModule      : Bool := false
   -- per-import fields to be consumed by `moduleIdent`
@@ -26,8 +27,9 @@ structure State where
 
 @[expose] def Parser := String → State → State
 
-instance : Inhabited Parser where
-  default := fun _ s => s
+@[inline] def skip : Parser := fun _ s => s
+
+instance : Inhabited Parser := ⟨skip⟩
 
 @[inline] def State.setPos (s : State) (pos : String.Pos) : State :=
   { s with pos := pos }
@@ -38,6 +40,9 @@ instance : Inhabited Parser where
 def State.mkEOIError (s : State) : State :=
   s.mkError "unexpected end of input"
 
+@[inline] def State.clearError (s : State) : State :=
+  { s with error? := none, badModifier := false  }
+
 @[inline] def State.next (s : State) (input : String) (pos : String.Pos) : State :=
   { s with pos := input.next pos }
 
@@ -125,8 +130,8 @@ partial def whitespace : Parser := fun input s =>
         go (k.next' i h₁) (input.next' j h₂)
   go 0 s.pos
 
-@[inline] partial def keyword (k : String) : Parser :=
-  keywordCore k (fun _ s => s.mkError s!"`{k}` expected") (fun _ s => s)
+@[inline] def keyword (k : String) : Parser :=
+  keywordCore k (fun _ s => s.mkError s!"`{k}` expected") skip
 
 @[inline] def isIdCont : String → State → Bool := fun input s =>
   let i := s.pos
@@ -152,7 +157,9 @@ def State.pushImport (i : Import) (s : State) : State :=
 
 partial def moduleIdent : Parser := fun input s =>
   let finalize (module : Name) : Parser := fun input s =>
-    whitespace input (s.pushImport { module, isMeta := s.isMeta, importAll := s.importAll, isExported := s.isExported })
+    let imp := { module, isMeta := s.isMeta, importAll := s.importAll, isExported := s.isExported }
+    let s := whitespace input (s.pushImport imp)
+    {s with isMeta := false, importAll := false, isExported := !s.isModule}
   let rec parse (module : Name) (s : State) :=
     let i := s.pos
     if h : input.atEnd i then
@@ -187,30 +194,50 @@ partial def moduleIdent : Parser := fun input s =>
         s.mkError "expected identifier"
   parse .anonymous s
 
-@[specialize] partial def many (p : Parser) : Parser := fun input s =>
+@[inline] def atomic (p : Parser) : Parser := fun input s =>
   let pos := s.pos
-  let size := s.imports.size
   let s := p input s
-  match s.error? with
-  | none => many p input s
-  | some _ => { s with pos, error? := none, imports := s.imports.shrink size }
+  if s.error? matches some .. then {s with pos} else s
 
-def setIsMeta (isMeta : Bool) : Parser := fun _ s =>
-  { s with isMeta }
+@[specialize] partial def manyImports (p : Parser) : Parser := fun input s =>
+  let pos := s.pos
+  let s := p input s
+  if s.error? matches some .. then
+    if s.pos == pos then s.clearError else s
+  else if s.badModifier then
+    let err := "cannot use 'public', 'meta', or 'all' without 'module'"
+    {s with pos, badModifier := false, error? := some err}
+  else
+    manyImports p input s
 
-def setIsExported (isExported : Bool) : Parser := fun _ s =>
-  { s with isExported := isExported || !s.isModule }
+def setIsModule (isModule : Bool) : Parser := fun _ s =>
+  { s with isModule, isExported := !isModule }
 
-def setImportAll (importAll : Bool) : Parser := fun _ s =>
-  { s with importAll }
+def setMeta : Parser := fun _ s =>
+  if s.isModule then
+    { s with isMeta := true }
+  else
+    { s with badModifier := true }
+
+def setExported : Parser := fun _ s =>
+  if s.isModule then
+    { s with isExported := true }
+  else
+    { s with badModifier := true }
+
+def setImportAll : Parser := fun _ s =>
+  if s.isModule then
+    { s with importAll := true }
+  else
+    { s with badModifier := true }
 
 def main : Parser :=
-  keywordCore "module" (fun _ s => s) (fun _ s => { s with isModule := true }) >>
-  keywordCore "prelude" (fun _ s => s.pushImport `Init) (fun _ s => s) >>
-  many (keywordCore "public" (setIsExported false) (setIsExported true) >>
-    keywordCore "meta" (setIsMeta false) (setIsMeta true) >>
-    keyword "import" >>
-    keywordCore "all" (setImportAll false) (setImportAll true) >>
+  keywordCore "module" (setIsModule false) (setIsModule true) >>
+  keywordCore "prelude" (fun _ s => s.pushImport `Init) skip >>
+  manyImports (atomic (keywordCore "public" skip setExported >>
+    keywordCore "meta" skip setMeta >>
+    keyword "import") >>
+    keywordCore "all" skip setImportAll >>
     moduleIdent)
 
 end ParseImports
@@ -220,9 +247,11 @@ Simpler and faster version of `parseImports`. We use it to implement Lake.
 -/
 def parseImports' (input : String) (fileName : String) : IO ModuleHeader := do
   let s := ParseImports.main input (ParseImports.whitespace input {})
-  match s.error? with
-  | none => return { s with }
-  | some err => throw <| IO.userError s!"{fileName}: {err}"
+  let some err := s.error?
+    | return { s with }
+  let fileMap := input.toFileMap
+  let pos := fileMap.toPosition s.pos
+  throw <| .userError s!"{fileName}:{pos.line}:{pos.column}: {err}"
 
 structure PrintImportResult where
   result?  : Option ModuleHeader := none

src/Lean/Parser/Module.lean

@@ -88,6 +88,25 @@ def parseHeader (inputCtx : InputContext) : IO (TSyntax ``Module.header × Modul
   let mut messages : MessageLog := {}
   for (pos, stk, err) in s.allErrors do
     messages := messages.add <| mkErrorMessage inputCtx pos stk err
+  if let `(Module.header| $[module%$moduleTk?]? $[prelude]? $importsStx*) := stx then
+    if moduleTk?.isNone then
+      let mkError ref msg : Message :=
+        let pos := ref.getPos?.getD 0
+        {
+          fileName := inputCtx.fileName
+          pos := inputCtx.fileMap.toPosition pos
+          endPos := inputCtx.fileMap.toPosition <| ref.getTailPos?.getD pos
+          keepFullRange := true
+          data := msg
+        }
+      for stx in importsStx do
+        if let `(Module.import| $[public%$pubTk?]? $[meta%$metaTk?]? import $[all%$allTk?]? $_) := stx then
+          if let some tk := pubTk? then
+            messages := messages.add <| mkError tk "cannot use 'public import' without 'module'"
+          if let some tk := metaTk? then
+            messages := messages.add <| mkError tk "cannot use 'meta import' without 'module'"
+          if let some tk := allTk? then
+            messages := messages.add <| mkError tk "cannot use 'import all' without 'module'"
   pure (⟨stx⟩, {pos := s.pos, recovering := s.hasError}, messages)
 
 private def mkEOI (pos : String.Pos) : Syntax :=

src/lake/Lake/Build/Module.lean

@@ -344,7 +344,7 @@ private def ModuleImportInfo.addImport
     info
 
 private def fetchImportInfo
-  (fileName : String) (modName : Name) (header : ModuleHeader)
+  (fileName : String) (pkgName modName : Name) (header : ModuleHeader)
 : FetchM (Job ModuleImportInfo) := do
   let nonModule := !header.isModule
   let info := ModuleImportInfo.nil modName
@@ -355,6 +355,9 @@ private def fetchImportInfo
       return .error
     let some mod ← findModule? imp.module
       | return s
+    if imp.importAll && pkgName != mod.pkg.name then
+      logError s!"{fileName}: cannot 'import all' across packages"
+      return .error
     let importJob ← mod.exportInfo.fetch
     return s.zipWith (·.addImport nonModule mod imp ·) importJob
 
@@ -362,7 +365,7 @@ private def fetchImportInfo
 def Module.importInfoFacetConfig : ModuleFacetConfig importInfoFacet :=
   mkFacetJobConfig fun mod => do
     let header ← (← mod.header.fetch).await
-    fetchImportInfo mod.relLeanFile.toString mod.name header
+    fetchImportInfo mod.relLeanFile.toString mod.pkg.name mod.name header
 
 private def noServerOLeanError :=
   "No server olean generated. Ensure the module system is enabled."
@@ -906,7 +909,7 @@ private def setupEditedModule
     return ⟨imp, ← findModule? imp.module⟩
   let fileName := mod.relLeanFile.toString
   let localImports := directImports.filterMap (·.module?)
-  let impInfoJob ← fetchImportInfo fileName mod.name header
+  let impInfoJob ← fetchImportInfo fileName mod.pkg.name mod.name header
   let precompileImports ←
     if mod.shouldPrecompile then
       (← computeTransImportsAux fileName localImports).await
@@ -953,7 +956,7 @@ private def setupExternalModule
   let imports ← header.imports.mapM fun imp => do
     return ⟨imp, ← findModule? imp.module⟩
   let localImports := imports.filterMap (·.module?)
-  let impInfoJob ← fetchImportInfo fileName .anonymous header
+  let impInfoJob ← fetchImportInfo fileName .anonymous .anonymous header
   let precompileImports ← (← computePrecompileImportsAux fileName localImports).await
   let impLibsJob ← fetchImportLibs precompileImports
   let externLibsJob ← Job.collectArray <$>

src/lake/tests/module/ErrorTest/CrossPackageImportAll.lean

@@ -0,0 +1,2 @@
+module
+import all Dep.Module

src/lake/tests/module/clean.sh

@@ -1,2 +1,3 @@
 rm -f produced*
+rm -rf dep/.lake dep/lake-manifest.json
 rm -rf .lake lake-manifest.json Test/Generated

src/lake/tests/module/dep/Dep/Module.lean

@@ -0,0 +1 @@
+module

src/lake/tests/module/dep/lakefile.toml

@@ -0,0 +1,5 @@
+name = "dep"
+
+[[lean_lib]]
+name = "Dep"
+leanOptions.experimental.module = true

src/lake/tests/module/lakefile.toml

@@ -1,7 +1,14 @@
 name = "test"
 defaultTargets = ["Test"]
+leanOptions.experimental.module = true
 
 [[lean_lib]]
 name = "Test"
 globs = "Test.+"
-leanOptions.experimental.module = true
+
+[[lean_lib]]
+name = "ErrorTest"
+
+[[require]]
+name = "dep"
+path = "dep"

src/lake/tests/module/test.sh

@@ -17,6 +17,9 @@ module
 public def foo := "bar"
 EOF
 
+# Test cross-package `import all``
+test_err "cannot 'import all' across packages" build ErrorTest.CrossPackageImportAll
+
 # Tests importing of a module's private segment
 # should not not be imported by a plain `import` in a module
 test_run build Test.ModuleImport

tests/lean/moduleKeywords.lean

@@ -0,0 +1,2 @@
+public meta import Init
+import all Init

tests/lean/moduleKeywords.lean.expected.out

@@ -0,0 +1,3 @@
+moduleKeywords.lean:1:0-1:6: error: cannot use 'public import' without 'module'
+moduleKeywords.lean:1:7-1:11: error: cannot use 'meta import' without 'module'
+moduleKeywords.lean:2:7-2:10: error: cannot use 'import all' without 'module'

tests/pkg/module/Module.lean

@@ -1,11 +1,11 @@
-public import Lean
-public import Module.Basic
-public import Module.Imported
-public import Module.ImportedAll
-public import Module.ImportedPrivateImported
-public import Module.PrivateImported
-public import Module.ImportedAllPrivateImported
-public import Module.NonModule
+import Lean
+import Module.Basic
+import Module.Imported
+import Module.ImportedAll
+import Module.ImportedPrivateImported
+import Module.PrivateImported
+import Module.ImportedAllPrivateImported
+import Module.NonModule
 
 /-! # Module system basic tests -/
 

tests/pkg/module/Module/NonModule.lean

@@ -1,5 +1,5 @@
-public import Module.Basic
-public import Lean
+import Module.Basic
+import Lean
 
 /-- info: @[defeq] theorem f.eq_def : f = 1 -/
 #guard_msgs in #print sig f.eq_def