From 334d9bd4f3dabe81738e74d455ffb4139f84c8e5 Mon Sep 17 00:00:00 2001
From: Kim Morrison <477956+kim-em@users.noreply.github.com>
Date: Wed, 8 Apr 2026 19:09:01 +1000
Subject: [PATCH] feat: add `markMeta` parameter to `addAndCompile` (#13311)
MIME-Version: 1.0
Content-Type: text/plain; charset=UTF-8
Content-Transfer-Encoding: 8bit

This PR adds an optional `markMeta : Bool := false` parameter to
`addAndCompile`, so that callers can propagate the `meta` marking
without manually splitting into `addDecl` + `markMeta` + `compileDecl`.

Also updates `ParserCompiler` to use the new parameter.

🤖 Prepared with Claude Code

---------

Co-authored-by: Claude Opus 4.6 (1M context) <noreply@anthropic.com>
---
 src/Lean/AddDecl.lean        | 7 ++++++-
 src/Lean/ParserCompiler.lean | 4 +---
 2 files changed, 7 insertions(+), 4 deletions(-)

diff --git a/src/Lean/AddDecl.lean b/src/Lean/AddDecl.lean
index c67a1152e8..d56aec5aa4 100644
--- a/src/Lean/AddDecl.lean
+++ b/src/Lean/AddDecl.lean
@@ -9,6 +9,7 @@ prelude
 public import Lean.Meta.Sorry
 public import Lean.Util.CollectAxioms
 public import Lean.OriginalConstKind
+import Lean.Compiler.MetaAttr
 import all Lean.OriginalConstKind  -- for accessing `privateConstKindsExt`
 
 public section
@@ -208,8 +209,12 @@ where
       catch _ => pure ()
 
 
-def addAndCompile (decl : Declaration) (logCompileErrors : Bool := true) : CoreM Unit := do
+def addAndCompile (decl : Declaration) (logCompileErrors : Bool := true)
+    (markMeta : Bool := false) : CoreM Unit := do
   addDecl decl
+  if markMeta then
+    for n in decl.getNames do
+      modifyEnv (Lean.markMeta · n)
   compileDecl decl (logErrors := logCompileErrors)
 
 end Lean
diff --git a/src/Lean/ParserCompiler.lean b/src/Lean/ParserCompiler.lean
index 01f647bedb..8c80c6a996 100644
--- a/src/Lean/ParserCompiler.lean
+++ b/src/Lean/ParserCompiler.lean
@@ -110,9 +110,7 @@ partial def compileParserExpr (e : Expr) : MetaM Expr := do
         }
         -- usually `meta` is inferred during compilation for auxiliary definitions, but as
         -- `ctx.combinatorAttr` may enforce correct use of the modifier, infer now.
-        if isMarkedMeta (← getEnv) c then
-          modifyEnv (markMeta · c')
-        addAndCompile decl
+        addAndCompile decl (markMeta := isMarkedMeta (← getEnv) c)
         modifyEnv (ctx.combinatorAttr.setDeclFor · c c')
         if cinfo.type.isConst then
           if let some kind ← parserNodeKind? cinfo.value! then