diff --git a/src/Init/Meta.lean b/src/Init/Meta.lean
index a705407396..a238409b44 100644
--- a/src/Init/Meta.lean
+++ b/src/Init/Meta.lean
@@ -60,6 +60,9 @@ def toolchain :=
   else
     ""
 
+@[extern c inline "LEAN_IS_STAGE0"]
+constant Internal.isStage0 (u : Unit) : Bool
+
 /- Valid identifier names -/
 def isGreek (c : Char) : Bool :=
   0x391 ≤ c.val && c.val ≤ 0x3dd
diff --git a/src/Lean/Parser/Extension.lean b/src/Lean/Parser/Extension.lean
index a9822f421d..a5809eaee1 100644
--- a/src/Lean/Parser/Extension.lean
+++ b/src/Lean/Parser/Extension.lean
@@ -404,7 +404,9 @@ def addSyntaxNodeKind (env : Environment) (k : SyntaxNodeKind) : Environment :=
 
 def isValidSyntaxNodeKind (env : Environment) (k : SyntaxNodeKind) : Bool :=
   let kinds := (parserExtension.getState env).kinds
-  kinds.contains k
+  -- accept any constant in stage 1 (i.e. when compiled by stage 0) so that
+  -- we can add a built-in parser and its elaborator in the same stage
+  kinds.contains k || (Internal.isStage0 () && env.contains k)
 
 def getSyntaxNodeKinds (env : Environment) : List SyntaxNodeKind :=
   let kinds := (parserExtension.getState env).kinds
diff --git a/src/Lean/Util/Path.lean b/src/Lean/Util/Path.lean
index f5c08c1e24..01b1b5781b 100644
--- a/src/Lean/Util/Path.lean
+++ b/src/Lean/Util/Path.lean
@@ -56,9 +56,6 @@ end SearchPath
 
 builtin_initialize searchPathRef : IO.Ref SearchPath ← IO.mkRef {}
 
-@[extern c inline "LEAN_IS_STAGE0"]
-private constant isStage0 (u : Unit) : Bool
-
 @[export lean_get_prefix]
 def getBuildDir : IO FilePath := do
   return (← IO.appDir).parent |>.get!
@@ -67,7 +64,7 @@ def getBuildDir : IO FilePath := do
 def getLibDir (leanSysroot : FilePath) : IO FilePath := do
   let mut buildDir := leanSysroot
   -- use stage1 stdlib with stage0 executable (which should never be distributed outside of the build directory)
-  if isStage0 () then
+  if Internal.isStage0 () then
     buildDir := buildDir / ".." / "stage1"
   return buildDir / "lib" / "lean"