From 2d999d762202af4128b2aca2d52e7b142e9685df Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Henrik=20B=C3=B6ving?= <hargonix@gmail.com>
Date: Mon, 16 Mar 2026 11:03:40 +0100
Subject: [PATCH] refactor: ignore borrow annotations at export/extern tricks
 (#12930)

This PR places `set_option compiler.ignoreBorrowAnnotation true in` on
to all `export`/`extern`
pairs. This is necessary because `export` forces all arguments to be
passed as owned while `extern`
respects borrow annotations. The current approach to the
`export`/`extern` trick was always broken
but never surfaced. However, with upcoming changes many
`export`/`extern` pairs are going to be
affected by borrow annotations and would've broken without this.
---
 src/Init/Data/String/Bootstrap.lean           | 27 +++++++++++++++++++
 src/Lean/Compiler/ExternAttr.lean             |  1 +
 src/Lean/Elab/Tactic/Try.lean                 |  1 +
 src/Lean/Environment.lean                     |  8 ++++++
 src/Lean/Meta/Basic.lean                      |  6 +++++
 src/Lean/Meta/Match/MatchEqsExt.lean          |  2 ++
 src/Lean/Meta/Sym/Pattern.lean                |  1 +
 src/Lean/Meta/Sym/Simp/SimpM.lean             |  1 +
 .../Meta/Tactic/Grind/Arith/Cutsat/Proof.lean |  1 +
 .../Meta/Tactic/Grind/Arith/Cutsat/Util.lean  |  3 +++
 .../Meta/Tactic/Grind/Arith/Cutsat/Var.lean   |  1 +
 src/Lean/Meta/Tactic/Grind/Types.lean         |  6 +++++
 src/Lean/Meta/Tactic/Grind/Util.lean          |  1 +
 src/Lean/Meta/Tactic/Simp/Types.lean          |  2 ++
 src/Lean/Meta/WHNF.lean                       |  1 +
 src/Lean/MonadEnv.lean                        |  1 +
 src/Lean/PrettyPrinter/Formatter.lean         |  2 ++
 src/Lean/PrettyPrinter/Parenthesizer.lean     |  2 ++
 src/lake/Lake/Load/Lean/Elab.lean             |  1 +
 19 files changed, 68 insertions(+)

diff --git a/src/Init/Data/String/Bootstrap.lean b/src/Init/Data/String/Bootstrap.lean
index 267148ce88..ba62e40a0d 100644
--- a/src/Init/Data/String/Bootstrap.lean
+++ b/src/Init/Data/String/Bootstrap.lean
@@ -55,9 +55,11 @@ end String
 
 namespace String.Internal
 
+set_option compiler.ignoreBorrowAnnotation true in
 @[extern "lean_string_posof"]
 opaque posOf (s : String) (c : Char) : Pos.Raw
 
+set_option compiler.ignoreBorrowAnnotation true in
 @[extern "lean_string_offsetofpos"]
 opaque offsetOfPos (s : String) (pos : Pos.Raw) : Nat
 
@@ -67,6 +69,7 @@ opaque extract : (@& String) → (@& Pos.Raw) → (@& Pos.Raw) → String
 @[extern "lean_string_length"]
 opaque length : (@& String) → Nat
 
+set_option compiler.ignoreBorrowAnnotation true in
 @[extern "lean_string_pushn"]
 opaque pushn (s : String) (c : Char) (n : Nat) : String
 
@@ -76,45 +79,57 @@ opaque append : String → (@& String) → String
 @[extern "lean_string_utf8_next"]
 opaque next (s : @& String) (p : @& Pos.Raw) : Pos.Raw
 
+set_option compiler.ignoreBorrowAnnotation true in
 @[extern "lean_string_isempty"]
 opaque isEmpty (s : String) : Bool
 
+set_option compiler.ignoreBorrowAnnotation true in
 @[extern "lean_string_foldl"]
 opaque foldl (f : String → Char → String) (init : String) (s : String) : String
 
+set_option compiler.ignoreBorrowAnnotation true in
 @[extern "lean_string_isprefixof"]
 opaque isPrefixOf (p : String) (s : String) : Bool
 
+set_option compiler.ignoreBorrowAnnotation true in
 @[extern "lean_string_any"]
 opaque any (s : String) (p : Char → Bool) : Bool
 
+set_option compiler.ignoreBorrowAnnotation true in
 @[extern "lean_string_contains"]
 opaque contains (s : String) (c : Char) : Bool
 
 @[extern "lean_string_utf8_get"]
 opaque get (s : @& String) (p : @& Pos.Raw) : Char
 
+set_option compiler.ignoreBorrowAnnotation true in
 @[extern "lean_string_capitalize"]
 opaque capitalize (s : String) : String
 
 @[extern "lean_string_utf8_at_end"]
 opaque atEnd : (@& String) → (@& Pos.Raw) → Bool
 
+set_option compiler.ignoreBorrowAnnotation true in
 @[extern "lean_string_nextwhile"]
 opaque nextWhile (s : String) (p : Char → Bool) (i : String.Pos.Raw) : String.Pos.Raw
 
+set_option compiler.ignoreBorrowAnnotation true in
 @[extern "lean_string_trim"]
 opaque trim (s : String) : String
 
+set_option compiler.ignoreBorrowAnnotation true in
 @[extern "lean_string_intercalate"]
 opaque intercalate (s : String) : List String → String
 
+set_option compiler.ignoreBorrowAnnotation true in
 @[extern "lean_string_front"]
 opaque front (s : String) : Char
 
+set_option compiler.ignoreBorrowAnnotation true in
 @[extern "lean_string_drop"]
 opaque drop (s : String) (n : Nat) : String
 
+set_option compiler.ignoreBorrowAnnotation true in
 @[extern "lean_string_dropright"]
 opaque dropRight (s : String) (n : Nat) : String
 
@@ -141,33 +156,43 @@ def List.asString (s : List Char) : String :=
 
 namespace Substring.Raw.Internal
 
+set_option compiler.ignoreBorrowAnnotation true in
 @[extern "lean_substring_tostring"]
 opaque toString : Substring.Raw → String
 
+set_option compiler.ignoreBorrowAnnotation true in
 @[extern "lean_substring_drop"]
 opaque drop : Substring.Raw → Nat → Substring.Raw
 
+set_option compiler.ignoreBorrowAnnotation true in
 @[extern "lean_substring_front"]
 opaque front (s : Substring.Raw) : Char
 
+set_option compiler.ignoreBorrowAnnotation true in
 @[extern "lean_substring_takewhile"]
 opaque takeWhile : Substring.Raw → (Char → Bool) → Substring.Raw
 
+set_option compiler.ignoreBorrowAnnotation true in
 @[extern "lean_substring_extract"]
 opaque extract : Substring.Raw → String.Pos.Raw → String.Pos.Raw → Substring.Raw
 
+set_option compiler.ignoreBorrowAnnotation true in
 @[extern "lean_substring_all"]
 opaque all (s : Substring.Raw) (p : Char → Bool) : Bool
 
+set_option compiler.ignoreBorrowAnnotation true in
 @[extern "lean_substring_beq"]
 opaque beq (ss1 ss2 : Substring.Raw) : Bool
 
+set_option compiler.ignoreBorrowAnnotation true in
 @[extern "lean_substring_isempty"]
 opaque isEmpty (ss : Substring.Raw) : Bool
 
+set_option compiler.ignoreBorrowAnnotation true in
 @[extern "lean_substring_get"]
 opaque get : Substring.Raw → String.Pos.Raw → Char
 
+set_option compiler.ignoreBorrowAnnotation true in
 @[extern "lean_substring_prev"]
 opaque prev : Substring.Raw → String.Pos.Raw → String.Pos.Raw
 
@@ -175,9 +200,11 @@ end Substring.Raw.Internal
 
 namespace String.Pos.Raw.Internal
 
+set_option compiler.ignoreBorrowAnnotation true in
 @[extern "lean_string_pos_sub"]
 opaque sub : String.Pos.Raw → String.Pos.Raw → String.Pos.Raw
 
+set_option compiler.ignoreBorrowAnnotation true in
 @[extern "lean_string_pos_min"]
 opaque min (p₁ p₂ : Pos.Raw) : Pos.Raw
 
diff --git a/src/Lean/Compiler/ExternAttr.lean b/src/Lean/Compiler/ExternAttr.lean
index 3902260a2e..511766bfa8 100644
--- a/src/Lean/Compiler/ExternAttr.lean
+++ b/src/Lean/Compiler/ExternAttr.lean
@@ -56,6 +56,7 @@ private def syntaxToExternAttrData (stx : Syntax) : AttrM ExternAttrData := do
   return { entries := entries.toList }
 
 -- Forward declaration
+set_option compiler.ignoreBorrowAnnotation true in
 @[extern "lean_add_extern"]
 opaque addExtern (declName : Name) (externAttrData : ExternAttrData) : CoreM Unit
 
diff --git a/src/Lean/Elab/Tactic/Try.lean b/src/Lean/Elab/Tactic/Try.lean
index 9def9b0367..efd87b21e3 100644
--- a/src/Lean/Elab/Tactic/Try.lean
+++ b/src/Lean/Elab/Tactic/Try.lean
@@ -623,6 +623,7 @@ private def evalSuggestSimpAllTrace : TryTactic := fun tac => do
   | _ => throwUnsupportedSyntax
 
 
+set_option compiler.ignoreBorrowAnnotation true in
 @[extern "lean_eval_suggest_tactic"] -- forward definition to avoid mutual block
 opaque evalSuggest : TryTactic
 
diff --git a/src/Lean/Environment.lean b/src/Lean/Environment.lean
index 8309ea90cf..727c54787c 100644
--- a/src/Lean/Environment.lean
+++ b/src/Lean/Environment.lean
@@ -752,6 +752,7 @@ private def lakeAdd (env : Environment) (cinfo : ConstantInfo) : Environment :=
   }
 
 -- forward reference due to too many cyclic dependencies
+set_option compiler.ignoreBorrowAnnotation true in
 @[extern "lean_is_reserved_name"]
 private opaque isReservedName (env : Environment) (name : Name) : Bool
 
@@ -1768,6 +1769,7 @@ private def looksLikeOldCodegenName : Name → Bool
   | .str _ s => s.startsWith "_cstage" || s.startsWith "_spec_" || s.startsWith "_elambda"
   | _        => false
 
+set_option compiler.ignoreBorrowAnnotation true in
 @[extern "lean_get_ir_extra_const_names"]
 private opaque getIRExtraConstNames (env : Environment) (level : OLeanLevel) (includeDecls := false) : Array Name
 
@@ -1804,6 +1806,7 @@ def mkModuleData (env : Environment) (level : OLeanLevel := .private) : IO Modul
     constNames, constants, entries
   }
 
+set_option compiler.ignoreBorrowAnnotation true in
 @[extern "lean_ir_export_entries"]
 private opaque exportIREntries (env : Environment) : Array (Name × Array EnvExtensionEntry)
 
@@ -1862,6 +1865,7 @@ private def setImportedEntries (states : Array EnvExtensionState) (mods : Array
           { s with importedEntries := s.importedEntries.set! modIdx entries }
   return states
 
+set_option compiler.ignoreBorrowAnnotation true in
 /--
   "Forward declaration" needed for updating the attribute table with user-defined attributes.
   User-defined attributes are declared using the `initialize` command. The `initialize` command is just syntax sugar for the `init` attribute.
@@ -1872,9 +1876,12 @@ private def setImportedEntries (states : Array EnvExtensionState) (mods : Array
   Later, we set this method with code that adds the user-defined attributes that were imported after we initialized `attributeExtension`.
 -/
 @[extern "lean_update_env_attributes"] opaque updateEnvAttributes : Environment → IO Environment
+
+set_option compiler.ignoreBorrowAnnotation true in
 /-- "Forward declaration" for retrieving the number of builtin attributes. -/
 @[extern "lean_get_num_attributes"] opaque getNumBuiltinAttributes : IO Nat
 
+set_option compiler.ignoreBorrowAnnotation true in
 @[extern "lean_run_init_attrs"]
 private opaque runInitAttrs (env : Environment) (opts : Options) : IO Unit
 
@@ -2399,6 +2406,7 @@ def displayStats (env : Environment) : IO Unit := do
 @[extern "lean_eval_const"]
 private unsafe opaque evalConstCore (α) (env : @& Environment) (opts : @& Options) (constName : @& Name) : Except String α
 
+set_option compiler.ignoreBorrowAnnotation true in
 @[extern "lean_eval_check_meta"]
 private opaque evalCheckMeta (env : Environment) (constName : Name) : Except String Unit
 
diff --git a/src/Lean/Meta/Basic.lean b/src/Lean/Meta/Basic.lean
index a78a0c4a29..7eba5c394f 100644
--- a/src/Lean/Meta/Basic.lean
+++ b/src/Lean/Meta/Basic.lean
@@ -760,6 +760,7 @@ have to hard-code the true arity of these definitions here, and make sure the C
 We have used another hack based on `IO.Ref`s in the past, it was safer but less efficient.
 -/
 
+set_option compiler.ignoreBorrowAnnotation true in
 /--
 Reduces an expression to its *weak head normal form*.
 This is when the "head" of the top-level expression has been fully reduced.
@@ -768,6 +769,7 @@ The result may contain subexpressions that have not been reduced.
 See `Lean.Meta.whnfImp` for the implementation.
 -/
 @[extern "lean_whnf"] opaque whnf : Expr → MetaM Expr
+set_option compiler.ignoreBorrowAnnotation true in
 /--
 Returns the inferred type of the given expression. Assumes the expression is type-correct.
 
@@ -822,8 +824,11 @@ def e3 : Expr := .app (.const ``Nat.zero []) (.const ``Nat.zero [])
 See `Lean.Meta.inferTypeImp` for the implementation of `inferType`.
 -/
 @[extern "lean_infer_type"] opaque inferType : Expr → MetaM Expr
+set_option compiler.ignoreBorrowAnnotation true in
 @[extern "lean_is_expr_def_eq"] opaque isExprDefEqAux : Expr → Expr → MetaM Bool
+set_option compiler.ignoreBorrowAnnotation true in
 @[extern "lean_is_level_def_eq"] opaque isLevelDefEqAux : Level → Level → MetaM Bool
+set_option compiler.ignoreBorrowAnnotation true in
 @[extern "lean_synth_pending"] protected opaque synthPending : MVarId → MetaM Bool
 
 def whnfForall (e : Expr) : MetaM Expr := do
@@ -2498,6 +2503,7 @@ def isDefEqD (t s : Expr) : MetaM Bool :=
 def isDefEqI (t s : Expr) : MetaM Bool :=
   withReducibleAndInstances <| isDefEq t s
 
+set_option compiler.ignoreBorrowAnnotation true in
 /--
 Returns `true` if `mvarId := val` was successfully assigned.
 This method uses the same assignment validation performed by `isDefEq`, but it does not check whether the types match.
diff --git a/src/Lean/Meta/Match/MatchEqsExt.lean b/src/Lean/Meta/Match/MatchEqsExt.lean
index 4e65b38c3a..07d1f07a16 100644
--- a/src/Lean/Meta/Match/MatchEqsExt.lean
+++ b/src/Lean/Meta/Match/MatchEqsExt.lean
@@ -46,12 +46,14 @@ Forward definition of `getEquationsForImpl`.
 We want to use `getEquationsFor` in the simplifier,
 getEquationsFor` depends on `mkEquationsFor` which uses the simplifier.
 -/
+set_option compiler.ignoreBorrowAnnotation true in
 @[extern "lean_get_match_equations_for"]
 opaque getEquationsFor (matchDeclName : Name) : MetaM MatchEqns
 
 /-
 Forward definition of `genMatchCongrEqnsImpl`.
 -/
+set_option compiler.ignoreBorrowAnnotation true in
 @[extern "lean_get_congr_match_equations_for"]
 opaque genMatchCongrEqns (matchDeclName : Name) : MetaM (Array Name)
 
diff --git a/src/Lean/Meta/Sym/Pattern.lean b/src/Lean/Meta/Sym/Pattern.lean
index ec9d24d691..d7a4ae0fe9 100644
--- a/src/Lean/Meta/Sym/Pattern.lean
+++ b/src/Lean/Meta/Sym/Pattern.lean
@@ -573,6 +573,7 @@ structure DefEqM.Context where
 
 abbrev DefEqM := ReaderT DefEqM.Context SymM
 
+set_option compiler.ignoreBorrowAnnotation true in
 /--
 Structural definitional equality. It is much cheaper than `isDefEq`.
 
diff --git a/src/Lean/Meta/Sym/Simp/SimpM.lean b/src/Lean/Meta/Sym/Simp/SimpM.lean
index e87e55ad3a..e7ec647bf1 100644
--- a/src/Lean/Meta/Sym/Simp/SimpM.lean
+++ b/src/Lean/Meta/Sym/Simp/SimpM.lean
@@ -227,6 +227,7 @@ def SimpM.run' (x : SimpM α) (methods : Methods := {}) (config : Config := {})
   let initialLCtxSize := (← getLCtx).decls.size
   x methods.toMethodsRef { initialLCtxSize, config } |>.run' {}
 
+set_option compiler.ignoreBorrowAnnotation true in
 @[extern "lean_sym_simp"] -- Forward declaration
 opaque simp : Simproc
 
diff --git a/src/Lean/Meta/Tactic/Grind/Arith/Cutsat/Proof.lean b/src/Lean/Meta/Tactic/Grind/Arith/Cutsat/Proof.lean
index 7829d2cd31..b8a1fa3771 100644
--- a/src/Lean/Meta/Tactic/Grind/Arith/Cutsat/Proof.lean
+++ b/src/Lean/Meta/Tactic/Grind/Arith/Cutsat/Proof.lean
@@ -229,6 +229,7 @@ private inductive MulEqProof where
   | mulVar (k : Int) (a : Expr) (h : Expr)
   | none
 
+set_option compiler.ignoreBorrowAnnotation true in
 @[extern "lean_cutsat_eq_cnstr_to_proof"] -- forward definition
 private opaque EqCnstr.toExprProof (c' : EqCnstr) : ProofM Expr
 
diff --git a/src/Lean/Meta/Tactic/Grind/Arith/Cutsat/Util.lean b/src/Lean/Meta/Tactic/Grind/Arith/Cutsat/Util.lean
index c1f9bc9ae7..8acc30b280 100644
--- a/src/Lean/Meta/Tactic/Grind/Arith/Cutsat/Util.lean
+++ b/src/Lean/Meta/Tactic/Grind/Arith/Cutsat/Util.lean
@@ -41,6 +41,7 @@ def inconsistent : GoalM Bool := do
   if (← isInconsistent) then return true
   return (← get').conflict?.isSome
 
+set_option compiler.ignoreBorrowAnnotation true in
 /-- Creates a new variable in the cutsat module. -/
 @[extern "lean_grind_cutsat_mk_var"] -- forward definition
 opaque mkVar (e : Expr) : GoalM Var
@@ -62,6 +63,7 @@ def isIntTerm (e : Expr) : GoalM Bool :=
 def eliminated (x : Var) : GoalM Bool :=
   return (← get').elimEqs[x]!.isSome
 
+set_option compiler.ignoreBorrowAnnotation true in
 @[extern "lean_grind_cutsat_assert_eq"] -- forward definition
 opaque EqCnstr.assert (c : EqCnstr) : GoalM Unit
 
@@ -114,6 +116,7 @@ def DiseqCnstr.throwUnexpected (c : DiseqCnstr) : GoalM α := do
 def DiseqCnstr.denoteExpr (c : DiseqCnstr) : GoalM Expr := do
   return mkNot (mkIntEq (← c.p.denoteExpr') (mkIntLit 0))
 
+set_option compiler.ignoreBorrowAnnotation true in
 @[extern "lean_grind_cutsat_assert_le"] -- forward definition
 opaque LeCnstr.assert (c : LeCnstr) : GoalM Unit
 
diff --git a/src/Lean/Meta/Tactic/Grind/Arith/Cutsat/Var.lean b/src/Lean/Meta/Tactic/Grind/Arith/Cutsat/Var.lean
index ba1bc102e3..b963dcdda3 100644
--- a/src/Lean/Meta/Tactic/Grind/Arith/Cutsat/Var.lean
+++ b/src/Lean/Meta/Tactic/Grind/Arith/Cutsat/Var.lean
@@ -12,6 +12,7 @@ import Lean.Meta.IntInstTesters
 public section
 namespace Lean.Meta.Grind.Arith.Cutsat
 
+set_option compiler.ignoreBorrowAnnotation true in
 @[extern "lean_cutsat_propagate_nonlinear"]
 opaque propagateNonlinearTerm (y : Var) (x : Var) : GoalM Bool
 
diff --git a/src/Lean/Meta/Tactic/Grind/Types.lean b/src/Lean/Meta/Tactic/Grind/Types.lean
index 1c5426de2b..5866646c69 100644
--- a/src/Lean/Meta/Tactic/Grind/Types.lean
+++ b/src/Lean/Meta/Tactic/Grind/Types.lean
@@ -1359,6 +1359,7 @@ partial def getCongrRoot (e : Expr) : GoalM Expr := do
 def isInconsistent : GoalM Bool :=
   return (← get).inconsistent
 
+set_option compiler.ignoreBorrowAnnotation true in
 /--
 Returns a proof that `a = b`.
 It assumes `a` and `b` are in the same equivalence class, and have the same type.
@@ -1367,6 +1368,7 @@ It assumes `a` and `b` are in the same equivalence class, and have the same type
 @[extern "lean_grind_mk_eq_proof"]
 opaque mkEqProof (a b : Expr) : GoalM Expr
 
+set_option compiler.ignoreBorrowAnnotation true in
 /--
 Returns a proof that `a ≍ b`.
 It assumes `a` and `b` are in the same equivalence class.
@@ -1376,14 +1378,17 @@ It assumes `a` and `b` are in the same equivalence class.
 opaque mkHEqProof (a b : Expr) : GoalM Expr
 
 -- Forward definition
+set_option compiler.ignoreBorrowAnnotation true in
 @[extern "lean_grind_process_new_facts"]
 opaque processNewFacts : GoalM Unit
 
 -- Forward definition
+set_option compiler.ignoreBorrowAnnotation true in
 @[extern "lean_grind_internalize"]
 opaque internalize (e : Expr) (generation : Nat) (parent? : Option Expr := none) : GoalM Unit
 
 -- Forward definition
+set_option compiler.ignoreBorrowAnnotation true in
 @[extern "lean_grind_preprocess"]
 opaque preprocess : Expr → GoalM Simp.Result
 
@@ -1729,6 +1734,7 @@ def withoutModifyingState (x : GoalM α) : GoalM α := do
   finally
     set saved
 
+set_option compiler.ignoreBorrowAnnotation true in
 /-- Canonicalizes nested types, type formers, and instances in `e`. -/
 @[extern "lean_grind_canon"] -- Forward definition
 opaque canon (e : Expr) : GoalM Expr
diff --git a/src/Lean/Meta/Tactic/Grind/Util.lean b/src/Lean/Meta/Tactic/Grind/Util.lean
index 04b4f59041..a73d3cfc0f 100644
--- a/src/Lean/Meta/Tactic/Grind/Util.lean
+++ b/src/Lean/Meta/Tactic/Grind/Util.lean
@@ -153,6 +153,7 @@ def foldProjs (e : Expr) : MetaM Expr := do
       return .done e
   Meta.transform e (post := post)
 
+set_option compiler.ignoreBorrowAnnotation true in
 /--
 Normalizes the given expression using the `grind` simplification theorems and simprocs.
 This function is used for normalizing E-matching patterns. Note that it does not return a proof.
diff --git a/src/Lean/Meta/Tactic/Simp/Types.lean b/src/Lean/Meta/Tactic/Simp/Types.lean
index e277d665ac..3751d4c714 100644
--- a/src/Lean/Meta/Tactic/Simp/Types.lean
+++ b/src/Lean/Meta/Tactic/Simp/Types.lean
@@ -295,9 +295,11 @@ Executes `x` using a `MetaM` configuration for inferred from `Simp.Config`.
 @[inline] def withSimpMetaConfig (x : SimpM α) : SimpM α := do
   withConfigWithKey (← readThe Simp.Context).metaConfig x
 
+set_option compiler.ignoreBorrowAnnotation true in
 @[extern "lean_simp"]
 opaque simp (e : Expr) : SimpM Result
 
+set_option compiler.ignoreBorrowAnnotation true in
 @[extern "lean_dsimp"]
 opaque dsimp (e : Expr) : SimpM Expr
 
diff --git a/src/Lean/Meta/WHNF.lean b/src/Lean/Meta/WHNF.lean
index c2924e0cda..471e43b4fa 100644
--- a/src/Lean/Meta/WHNF.lean
+++ b/src/Lean/Meta/WHNF.lean
@@ -36,6 +36,7 @@ namespace Lean.Meta
 /-! # Smart unfolding support -/
 -- ===========================
 
+set_option compiler.ignoreBorrowAnnotation true in
 /--
 Forward declaration. It is defined in the module `src/Lean/Elab/PreDefinition/Structural/Eqns.lean`.
 It is possible to avoid this hack if we move `Structural.EqnInfo` and `Structural.eqnInfoExt`
diff --git a/src/Lean/MonadEnv.lean b/src/Lean/MonadEnv.lean
index 2a145f737f..e8d664d380 100644
--- a/src/Lean/MonadEnv.lean
+++ b/src/Lean/MonadEnv.lean
@@ -174,6 +174,7 @@ See also `Lean.matchConstStructure` for a less restrictive version.
         | _ => failK ()
       | _ => failK ()
 
+set_option compiler.ignoreBorrowAnnotation true in
 @[extern "lean_has_compile_error"]
 opaque hasCompileError (env : Environment) (constName : Name) : Bool
 
diff --git a/src/Lean/PrettyPrinter/Formatter.lean b/src/Lean/PrettyPrinter/Formatter.lean
index 3217c15430..2067634ee5 100644
--- a/src/Lean/PrettyPrinter/Formatter.lean
+++ b/src/Lean/PrettyPrinter/Formatter.lean
@@ -234,10 +234,12 @@ def recover'.formatter (fmt : PrettyPrinter.Formatter) := fmt
 -- Note that there is a mutual recursion
 -- `categoryParser -> mkAntiquot -> termParser -> categoryParser`, so we need to introduce an indirection somewhere
 -- anyway.
+set_option compiler.ignoreBorrowAnnotation true in
 @[extern "lean_mk_antiquot_formatter"]
 opaque mkAntiquot.formatter' (name : String) (kind : SyntaxNodeKind) (anonymous := true) (isPseudoKind := false) : Formatter
 
 -- break up big mutual recursion
+set_option compiler.ignoreBorrowAnnotation true in
 @[extern "lean_pretty_printer_formatter_interpret_parser_descr"]
 opaque interpretParserDescr' : ParserDescr → CoreM Formatter
 
diff --git a/src/Lean/PrettyPrinter/Parenthesizer.lean b/src/Lean/PrettyPrinter/Parenthesizer.lean
index 10ee54fb38..c364e827a7 100644
--- a/src/Lean/PrettyPrinter/Parenthesizer.lean
+++ b/src/Lean/PrettyPrinter/Parenthesizer.lean
@@ -307,6 +307,7 @@ def recover'.parenthesizer (p : PrettyPrinter.Parenthesizer) : PrettyPrinter.Par
 -- Note that there is a mutual recursion
 -- `categoryParser -> mkAntiquot -> termParser -> categoryParser`, so we need to introduce an indirection somewhere
 -- anyway.
+set_option compiler.ignoreBorrowAnnotation true in
 @[extern "lean_mk_antiquot_parenthesizer"]
 opaque mkAntiquot.parenthesizer' (name : String) (kind : SyntaxNodeKind) (anonymous := true) (isPseudoKind := false) : Parenthesizer
 
@@ -314,6 +315,7 @@ opaque mkAntiquot.parenthesizer' (name : String) (kind : SyntaxNodeKind) (anonym
   liftM x
 
 -- break up big mutual recursion
+set_option compiler.ignoreBorrowAnnotation true in
 @[extern "lean_pretty_printer_parenthesizer_interpret_parser_descr"]
 opaque interpretParserDescr' : ParserDescr → CoreM Parenthesizer
 
diff --git a/src/lake/Lake/Load/Lean/Elab.lean b/src/lake/Lake/Load/Lean/Elab.lean
index 17086b358f..c72b295cb0 100644
--- a/src/lake/Lake/Load/Lean/Elab.lean
+++ b/src/lake/Lake/Load/Lean/Elab.lean
@@ -88,6 +88,7 @@ def elabConfigFile
   else
     return s.commandState.env
 
+set_option compiler.ignoreBorrowAnnotation true in
 /--
 `Lean.Kernel.Environment.add` is now private, this is an exported helper wrapping it for
 `Lean.Environment`.