From d7e35c77ca797065ed20fcd138a162f2d6502347 Mon Sep 17 00:00:00 2001
From: Sebastian Ullrich <sebasti@nullri.ch>
Date: Sat, 28 Jun 2025 15:11:34 +0200
Subject: [PATCH] chore: reserve `public import` syntax (#9061)

This PR adds the `public import` syntax to be used by the experimental
module system
---
 src/Lean/Elab/Import.lean           | 7 +++++--
 src/Lean/Elab/ParseImportsFast.lean | 2 ++
 src/Lean/Parser/Module.lean         | 4 +++-
 3 files changed, 10 insertions(+), 3 deletions(-)

diff --git a/src/Lean/Elab/Import.lean b/src/Lean/Elab/Import.lean
index 756b1f1c3a..8369722c42 100644
--- a/src/Lean/Elab/Import.lean
+++ b/src/Lean/Elab/Import.lean
@@ -22,9 +22,14 @@ def HeaderSyntax.imports (stx : HeaderSyntax) (includeInit : Bool := true) : Arr
   | `(Parser.Module.header| $[module%$moduleTk]? $[prelude%$preludeTk]? $importsStx*) =>
     let imports := if preludeTk.isNone && includeInit then #[{ module := `Init : Import }] else #[]
     imports ++ importsStx.map fun
+      -- TODO: delete together with `private` keyword
       | `(Parser.Module.import| $[private%$privateTk]? $[meta%$metaTk]? import $[all%$allTk]? $n) =>
         { module := n.getId, importAll := allTk.isSome, isExported := privateTk.isNone
           isMeta := metaTk.isSome }
+      | `(Parser.Module.import| $[public%$publicTk]? $[meta%$metaTk]? import $[all%$allTk]? $n) =>
+        { module := n.getId, importAll := allTk.isSome
+          isExported := publicTk.isSome || moduleTk.isNone
+          isMeta := metaTk.isSome }
       | _ => unreachable!
   | _ => unreachable!
 
@@ -53,8 +58,6 @@ def processHeaderCore
         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"
-      if !isModule && !i.isExported then
-        throw <| .userError "cannot use `private import` without `module`"
     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 d7bbee7b21..ee07595cce 100644
--- a/src/Lean/Elab/ParseImportsFast.lean
+++ b/src/Lean/Elab/ParseImportsFast.lean
@@ -204,6 +204,8 @@ 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 "private" (setIsExported true) (setIsExported false) >>
+    -- TODO: unset exported when absent and remove `private`
+    keywordCore "public" (setIsExported true) (setIsExported true) >>
     keywordCore "meta" (setIsMeta false) (setIsMeta true) >>
     keyword "import" >>
     keywordCore "all" (setImportAll false) (setImportAll true) >>
diff --git a/src/Lean/Parser/Module.lean b/src/Lean/Parser/Module.lean
index 169ef45f10..8cb722001f 100644
--- a/src/Lean/Parser/Module.lean
+++ b/src/Lean/Parser/Module.lean
@@ -13,11 +13,13 @@ namespace Parser
 namespace Module
 def moduleTk   := leading_parser "module"
 def «prelude»  := leading_parser "prelude"
+-- TODO: delete
 def «private»  := leading_parser (withAnonymousAntiquot := false) "private"
+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 «private» >> optional «meta» >> "import ") >>
+  atomic (optional («private» <|> «public») >> optional «meta» >> "import ") >>
   optional all >>
   identWithPartialTrailingDot
 def header     := leading_parser optional (moduleTk >> ppLine >> ppLine) >>