diff --git a/src/Lean/Elab/Import.lean b/src/Lean/Elab/Import.lean index 06a2f65cc6..36404088a6 100644 --- a/src/Lean/Elab/Import.lean +++ b/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 diff --git a/src/Lean/Elab/ParseImportsFast.lean b/src/Lean/Elab/ParseImportsFast.lean index f7df04d0ad..8e8162a10c 100644 --- a/src/Lean/Elab/ParseImportsFast.lean +++ b/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 diff --git a/src/Lean/Parser/Module.lean b/src/Lean/Parser/Module.lean index a419945805..e4fc59cdc0 100644 --- a/src/Lean/Parser/Module.lean +++ b/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 := diff --git a/src/lake/Lake/Build/Module.lean b/src/lake/Lake/Build/Module.lean index 0fd0a83e10..5cc1000661 100644 --- a/src/lake/Lake/Build/Module.lean +++ b/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 <$> diff --git a/src/lake/tests/module/ErrorTest/CrossPackageImportAll.lean b/src/lake/tests/module/ErrorTest/CrossPackageImportAll.lean new file mode 100644 index 0000000000..d8e81ae1b9 --- /dev/null +++ b/src/lake/tests/module/ErrorTest/CrossPackageImportAll.lean @@ -0,0 +1,2 @@ +module +import all Dep.Module diff --git a/src/lake/tests/module/clean.sh b/src/lake/tests/module/clean.sh index e29e5c70f6..54c0f1f644 100755 --- a/src/lake/tests/module/clean.sh +++ b/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 diff --git a/src/lake/tests/module/dep/Dep/Module.lean b/src/lake/tests/module/dep/Dep/Module.lean new file mode 100644 index 0000000000..0cca093d7a --- /dev/null +++ b/src/lake/tests/module/dep/Dep/Module.lean @@ -0,0 +1 @@ +module diff --git a/src/lake/tests/module/dep/lakefile.toml b/src/lake/tests/module/dep/lakefile.toml new file mode 100644 index 0000000000..9bc8df4539 --- /dev/null +++ b/src/lake/tests/module/dep/lakefile.toml @@ -0,0 +1,5 @@ +name = "dep" + +[[lean_lib]] +name = "Dep" +leanOptions.experimental.module = true diff --git a/src/lake/tests/module/lakefile.toml b/src/lake/tests/module/lakefile.toml index 741c9cabed..285f1b0ccd 100644 --- a/src/lake/tests/module/lakefile.toml +++ b/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" diff --git a/src/lake/tests/module/test.sh b/src/lake/tests/module/test.sh index a906e7a4de..0090244223 100755 --- a/src/lake/tests/module/test.sh +++ b/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 diff --git a/tests/lean/moduleKeywords.lean b/tests/lean/moduleKeywords.lean new file mode 100644 index 0000000000..43bf99867c --- /dev/null +++ b/tests/lean/moduleKeywords.lean @@ -0,0 +1,2 @@ +public meta import Init +import all Init diff --git a/tests/lean/moduleKeywords.lean.expected.out b/tests/lean/moduleKeywords.lean.expected.out new file mode 100644 index 0000000000..12713c9fb0 --- /dev/null +++ b/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' diff --git a/tests/pkg/module/Module.lean b/tests/pkg/module/Module.lean index 39ee9f25b5..bfbbc7b08e 100644 --- a/tests/pkg/module/Module.lean +++ b/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 -/ diff --git a/tests/pkg/module/Module/NonModule.lean b/tests/pkg/module/Module/NonModule.lean index 8d594390c0..48bfa62e2b 100644 --- a/tests/pkg/module/Module/NonModule.lean +++ b/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