From de57b77feb8ab54f52901d367eddbf651788e9fe Mon Sep 17 00:00:00 2001
From: Sebastian Ullrich <sebasti@nullri.ch>
Date: Sat, 7 Jun 2025 15:08:20 +0200
Subject: [PATCH] chore: support `meta` in `ParseImportsFast` (#8672)

---
 src/Lean/Elab/ParseImportsFast.lean | 9 +++++++--
 stage0/src/stdlib_flags.h           | 2 ++
 2 files changed, 9 insertions(+), 2 deletions(-)

diff --git a/src/Lean/Elab/ParseImportsFast.lean b/src/Lean/Elab/ParseImportsFast.lean
index 28c08da899..e0f4d3859f 100644
--- a/src/Lean/Elab/ParseImportsFast.lean
+++ b/src/Lean/Elab/ParseImportsFast.lean
@@ -15,6 +15,7 @@ structure State where
   error?        : Option String := none
   isModule      : Bool := false
   -- per-import fields to be consumed by `moduleIdent`
+  isMeta        : Bool := false
   isExported    : Bool := false
   importAll     : Bool := false
   deriving Inhabited
@@ -147,7 +148,7 @@ 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, importAll := s.importAll, isExported := s.isExported })
+    whitespace input (s.pushImport { module, isMeta := s.isMeta, importAll := s.importAll, isExported := s.isExported })
   let rec parse (module : Name) (s : State) :=
     let i := s.pos
     if h : input.atEnd i then
@@ -190,8 +191,11 @@ partial def moduleIdent : Parser := fun input s =>
   | none => many p input s
   | some _ => { pos, error? := none, imports := s.imports.shrink size }
 
+def setIsMeta (isMeta : Bool) : Parser := fun _ s =>
+  { s with isMeta }
+
 def setIsExported (isExported : Bool) : Parser := fun _ s =>
-  { s with isExported := isExported }
+  { s with isExported }
 
 def setImportAll (importAll : Bool) : Parser := fun _ s =>
   { s with importAll }
@@ -200,6 +204,7 @@ def main : Parser :=
   keywordCore "module" (fun _ s => { s with isModule := true }) (fun _ s => s) >>
   keywordCore "prelude" (fun _ s => s.pushImport `Init) (fun _ s => s) >>
   many (keywordCore "private" (setIsExported true) (setIsExported false) >>
+    keywordCore "meta" (setIsMeta true) (setIsMeta false) >>
     keyword "import" >>
     keywordCore "all" (setImportAll false) (setImportAll true) >>
     moduleIdent)
diff --git a/stage0/src/stdlib_flags.h b/stage0/src/stdlib_flags.h
index 79a0e58edd..1bbdca66f7 100644
--- a/stage0/src/stdlib_flags.h
+++ b/stage0/src/stdlib_flags.h
@@ -1,5 +1,7 @@
 #include "util/options.h"
 
+// Dear bot, please update stage 0
+
 namespace lean {
 options get_default_options() {
     options opts;