fix: remove accidental type monomorphism in Id.run_seqLeft (#12936)

This PR fixes `Id.run_seqLeft` and `Id.run_seqRight` to apply when the
two monad results are different.

.claude/CLAUDE.md

@@ -20,9 +20,24 @@ CTEST_PARALLEL_LEVEL="$(nproc)" CTEST_OUTPUT_ON_FAILURE=1 \
 make -C build/release -j "$(nproc)" test ARGS='--rerun-failed'
 
 # Single test from tests/foo/bar/ (quick check during development)
-cd tests/foo/bar && ./run_test example_test.lean
+CTEST_PARALLEL_LEVEL="$(nproc)" CTEST_OUTPUT_ON_FAILURE=1 \
+make -C build/release -j "$(nproc)" test ARGS=-R testname'
 ```
 
+## Testing stage 2
+
+When requested to test stage 2, build it as follows:
+```
+make -C build/release stage2 -j$(nproc)
+```
+Stage 2 is *not* automatically invalidated by changes to `src/` which allows for faster iteration
+when fixing a specific file in the stage 2 build but for invalidating any files that already passed
+the stage 2 build as well as for final validation,
+```
+make -C build/release/stage2 clean-stdlib
+```
+must be run manually before building.
+
 ## New features
 
 When asked to implement new features:

CMakeLists.txt

@@ -79,7 +79,7 @@ if(NOT CMAKE_SYSTEM_NAME MATCHES "Emscripten")
   endif()
   find_program(LEANTAR leantar)
   if(NOT LEANTAR)
-    set(LEANTAR_VERSION v0.1.18)
+    set(LEANTAR_VERSION v0.1.19)
     if(CMAKE_SYSTEM_NAME MATCHES "Windows")
       set(LEANTAR_ARCHIVE_SUFFIX .zip)
       set(LEANTAR_TARGET x86_64-pc-windows-msvc)

doc/examples/compiler/run_test.sh

@@ -1,6 +1,3 @@
-#!/usr/bin/env bash
-source ../../../tests/env_test.sh
-
 leanmake --always-make bin
 
 capture ./build/bin/test hello world

doc/examples/run_test.sh

@@ -1,6 +1,3 @@
-#!/usr/bin/env bash
-source ../../tests/env_test.sh
-
 capture_only "$1" \
   lean -Dlinter.all=false "$1"
 check_exit_is_success

script/release_steps.py

@@ -492,8 +492,9 @@ def execute_release_steps(repo, version, config):
             'ROOT_REV=$(jq -r \'.packages[] | select(.name == "subverso") | .rev\' lake-manifest.json); '
             'SUBVERSO_URL=$(jq -r \'.packages[] | select(.name == "subverso") | .url\' lake-manifest.json); '
             'DEMOD_REV=$(git ls-remote "$SUBVERSO_URL" "refs/tags/no-modules/$ROOT_REV" | awk \'{print $1}\'); '
-            'find test-projects -name lake-manifest.json -print0 | '
-            'xargs -0 -I{} sh -c \'jq --arg rev "$DEMOD_REV" \'.packages |= map(if .name == "subverso" then .rev = $rev else . end)\' "{}" > /tmp/lm_tmp.json && mv /tmp/lm_tmp.json "{}"\''
+            'find test-projects -name lake-manifest.json -print0 | while IFS= read -r -d \'\' f; do '
+            'jq --arg rev "$DEMOD_REV" \'.packages |= map(if .name == "subverso" then .rev = $rev else . end)\' "$f" > /tmp/lm_tmp.json && mv /tmp/lm_tmp.json "$f"; '
+            'done'
         )
         run_command(sync_script, cwd=repo_path)
         print(green("Synced de-modulized subverso rev to all test-project sub-manifests"))

src/Init/Control/Lawful/Basic.lean

@@ -254,8 +254,8 @@ instance : LawfulMonad Id := by
 @[simp, grind =] theorem run_bind (x : Id α) (f : α → Id β) : (x >>= f).run = (f x.run).run := rfl
 @[simp, grind =] theorem run_pure (a : α) : (pure a : Id α).run = a := rfl
 @[simp, grind =] theorem pure_run (a : Id α) : pure a.run = a := rfl
-@[simp] theorem run_seqRight (x y : Id α) : (x *> y).run = y.run := rfl
-@[simp] theorem run_seqLeft (x y : Id α) : (x <* y).run = x.run := rfl
+@[simp] theorem run_seqRight (x : Id α) (y : Id β) : (x *> y).run = y.run := rfl
+@[simp] theorem run_seqLeft (x : Id α) (y : Id β) : (x <* y).run = x.run := rfl
 @[simp] theorem run_seq (f : Id (α → β)) (x : Id α) : (f <*> x).run = f.run x.run := rfl
 
 end Id

src/Init/Data/Int/Pow.lean

@@ -118,16 +118,19 @@ theorem toNat_pow_of_nonneg {x : Int} (h : 0 ≤ x) (k : Nat) : (x ^ k).toNat =
   | succ k ih =>
     rw [Int.pow_succ, Int.toNat_mul (Int.pow_nonneg h) h, ih, Nat.pow_succ]
 
-protected theorem sq_nonnneg (m : Int) : 0 ≤ m ^ 2 := by
+protected theorem sq_nonneg (m : Int) : 0 ≤ m ^ 2 := by
   rw [Int.pow_succ, Int.pow_one]
   cases m
   · apply Int.mul_nonneg <;> simp
   · apply Int.mul_nonneg_of_nonpos_of_nonpos <;> exact negSucc_le_zero _
 
+@[deprecated Int.sq_nonneg (since := "2026-03-13")]
+protected theorem sq_nonnneg (m : Int) : 0 ≤ m ^ 2 := Int.sq_nonneg m
+
 protected theorem pow_nonneg_of_even {m : Int} {n : Nat} (h : n % 2 = 0) : 0 ≤ m ^ n := by
   rw [← Nat.mod_add_div n 2, h, Nat.zero_add, Int.pow_mul]
   apply Int.pow_nonneg
-  exact Int.sq_nonnneg m
+  exact Int.sq_nonneg m
 
 protected theorem neg_pow {m : Int} {n : Nat} : (-m)^n = (-1)^(n % 2) * m^n := by
   rw [Int.neg_eq_neg_one_mul, Int.mul_pow]

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
 

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
 

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
 

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
 

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.

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)
 

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`.
 

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
 

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
 

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
 

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
 

src/Lean/Meta/Tactic/Grind/Parser.lean

@@ -138,7 +138,7 @@ example : f b = f c → a ≤ f a → f (f a) ≤ f (f (f a)) := by
 ```
 -/
 @[builtin_command_parser] def grindPattern := leading_parser
-  Term.attrKind >> "grind_pattern " >>  optional ("[" >> ident >> "]") >> ident >> darrow >> sepBy1 termParser "," >> optional grindPatternCnstrs
+  Term.attrKind >> "grind_pattern " >>  optional ("[" >> ident >> "]") >> ident >> darrow >> sepBy1 termParser ", " >> optional grindPatternCnstrs
 
 @[builtin_command_parser] def initGrindNorm := leading_parser
   "init_grind_norm " >> many ident >> "| " >> many ident

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

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.

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
 

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`

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
 

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
 

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
 

src/Std/Time/DateTime/PlainDateTime.lean

@@ -566,7 +566,7 @@ instance : HAdd PlainDateTime Millisecond.Offset PlainDateTime where
   hAdd := addMilliseconds
 
 instance : HSub PlainDateTime Millisecond.Offset PlainDateTime where
-  hSub := addMilliseconds
+  hSub := subMilliseconds
 
 instance : HAdd PlainDateTime Second.Offset PlainDateTime where
   hAdd := addSeconds

src/Std/Time/Duration.lean

@@ -384,7 +384,7 @@ instance : HAdd PlainTime Duration PlainTime where
    hAdd pt d := PlainTime.ofNanoseconds (d.toNanoseconds + pt.toNanoseconds)
 
 instance : HSub PlainTime Duration PlainTime where
-   hSub pt d := PlainTime.ofNanoseconds (d.toNanoseconds - pt.toNanoseconds)
+   hSub pt d := PlainTime.ofNanoseconds (pt.toNanoseconds - d.toNanoseconds)
 
 end Duration
 end Time

src/lake/Lake/Build/Actions.lean

@@ -87,21 +87,20 @@ public def compileO
   }
 
 public def mkArgs (basePath : FilePath) (args : Array String) : LogIO (Array String) := do
-  if Platform.isWindows then
-    -- Use response file to avoid potentially exceeding CLI length limits.
-    let rspFile := basePath.addExtension "rsp"
-    let h ← IO.FS.Handle.mk rspFile .write
-    args.forM fun arg =>
-      -- Escape special characters
-      let arg := arg.foldl (init := "") fun s c =>
-        if c == '\\' || c == '"' then
-          s.push '\\' |>.push c
-        else
-          s.push c
-      h.putStr s!"\"{arg}\"\n"
-    return #[s!"@{rspFile}"]
-  else
-    return args
+  -- Use response file to avoid potentially exceeding CLI length limits.
+  -- On Windows this is always needed; on macOS/Linux this is needed for large
+  -- projects like Mathlib where the number of object files exceeds ARG_MAX.
+  let rspFile := basePath.addExtension "rsp"
+  let h ← IO.FS.Handle.mk rspFile .write
+  args.forM fun arg =>
+    -- Escape special characters
+    let arg := arg.foldl (init := "") fun s c =>
+      if c == '\\' || c == '"' then
+        s.push '\\' |>.push c
+      else
+        s.push c
+    h.putStr s!"\"{arg}\"\n"
+  return #[s!"@{rspFile}"]
 
 public def compileStaticLib
   (libFile : FilePath) (oFiles : Array FilePath)

src/lake/Lake/CLI/Main.lean

@@ -392,7 +392,7 @@ def serviceNotFound (service : String) (configuredServices : Array CacheServiceC
     configuredServices.foldl (· ++ s!"  {·.name}") msg
 
 @[inline] private def cacheToolchain (pkg : Package) (toolchain : CacheToolchain) : CacheToolchain :=
-  if pkg.bootstrap then .none else toolchain
+  if pkg.fixedToolchain || pkg.bootstrap then .none else toolchain
 
 @[inline] private def cachePlatform (pkg : Package) (platform : CachePlatform) : CachePlatform :=
   if pkg.isPlatformIndependent then .none else platform

src/lake/Lake/Config/Package.lean

@@ -45,7 +45,7 @@ public structure Package where
   /-- The path to the package's configuration file (relative to `dir`). -/
   relConfigFile : FilePath
   /-- The path to the package's JSON manifest of remote dependencies (relative to `dir`). -/
-  relManifestFile : FilePath := config.manifestFile.getD defaultManifestFile |>.normalize
+  relManifestFile : FilePath := defaultManifestFile
   /-- The package's scope (e.g., in Reservoir). -/
   scope : String
   /-- The URL to this package's Git remote. -/
@@ -244,6 +244,10 @@ public def id? (self : Package) : Option PkgId :=
 @[inline] public def isPlatformIndependent (self : Package) : Bool :=
   self.config.platformIndependent == some true
 
+/-- The package's `fixedToolchain` configuration. -/
+@[inline] public def fixedToolchain (self : Package) : Bool :=
+  self.config.fixedToolchain
+
 /-- The package's `releaseRepo`/`releaseRepo?` configuration. -/
 @[inline] public def releaseRepo? (self : Package) : Option String :=
   self.config.releaseRepo

src/lake/Lake/Config/PackageConfig.lean

@@ -29,16 +29,6 @@ public configuration PackageConfig (p : Name) (n : Name) extends WorkspaceConfig
   /-- **For internal use.** Whether this package is Lean itself. -/
   bootstrap : Bool := false
 
-  /--
-  **This field is deprecated.**
-
-  The path of a package's manifest file, which stores the exact versions
-  of its resolved dependencies.
-
-  Defaults to `defaultManifestFile` (i.e., `lake-manifest.json`).
-  -/
-  manifestFile : Option FilePath := none
-
   /-- An `Array` of target names to build whenever the package is used. -/
   extraDepTargets : Array Name := #[]
 
@@ -331,6 +321,18 @@ public configuration PackageConfig (p : Name) (n : Name) extends WorkspaceConfig
   -/
   allowImportAll : Bool := false
 
+  /--
+  Whether this package is expected to function only on a single toolchain
+  (the package's toolchain).
+
+  This informs Lake's toolchain update procedure (in `lake update`) to prioritize
+  this package's toolchain. It also avoids the need to separate input-to-output mappings
+  for this package by toolchain version in the Lake cache.
+
+  Defaults to `false`.
+  -/
+  fixedToolchain : Bool := false
+
 deriving Inhabited
 
 /-- The package's name as specified by the author. -/

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`.

src/lake/Lake/Load/Lean/Eval.lean

@@ -166,10 +166,6 @@ public def Package.loadFromEnv
     else
       pure self.config.lintDriver
 
-  -- Deprecation warnings
-  unless self.config.manifestFile.isNone do
-    logWarning s!"{self.prettyName}: package configuration option 'manifestFile' is deprecated"
-
   -- Fill in the Package
   return {self with
     depConfigs, targetDecls, targetDeclMap

src/lake/Lake/Load/Manifest.lean

@@ -50,8 +50,9 @@ That is, Lake ignores the `-` suffix.
 **v1.x.x** (versioned by a string)
 - `"1.0.0"`: Switches to a semantic versioning scheme
 - `"1.1.0"`: Add optional `scope` package entry field
+- `"1.2.0"`: Add optional `fixedToolchain` manifest field
 -/
-@[inline] public def Manifest.version : StdVer := {major := 1, minor := 1}
+@[inline] public def Manifest.version : StdVer := {major := 1, minor := 2}
 
 /-- Manifest version `0.6.0` package entry. For backwards compatibility. -/
 private inductive PackageEntryV6
@@ -84,7 +85,9 @@ public structure PackageEntry where
   name : Name
   scope : String := ""
   inherited : Bool
+  /-- The relative path within the package directory to the Lake configuration file. -/
   configFile : FilePath := defaultConfigFile
+  /-- The relative path within the package directory to the Lake manifest file. -/
   manifestFile? : Option FilePath := none
   src : PackageEntrySrc
   deriving Inhabited
@@ -139,7 +142,7 @@ public protected def fromJson? (json : Json) : Except String PackageEntry := do
       | _ =>
         throw s!"unknown package entry type '{type}'"
     return {
-      name, scope, inherited,
+      name, scope, inherited
       configFile, manifestFile? := manifestFile, src
       : PackageEntry
     }
@@ -172,6 +175,7 @@ end PackageEntry
 public structure Manifest where
   name : Name
   lakeDir : FilePath
+  fixedToolchain : Bool
   packagesDir? : Option FilePath := none
   packages : Array PackageEntry := #[]
 
@@ -184,6 +188,7 @@ public def addPackage (entry : PackageEntry) (self : Manifest) : Manifest :=
 public protected def toJson (self : Manifest) : Json :=
   Json.mkObj [
     ("version", toJson version),
+    ("fixedToolchain", toJson self.fixedToolchain),
     ("name", toJson self.name),
     ("lakeDir", toJson self.lakeDir),
     ("packagesDir", toJson self.packagesDir?),
@@ -217,11 +222,12 @@ private def getPackages (ver : StdVer) (obj : JsonObject) : Except String (Array
 public protected def fromJson? (json : Json) : Except String Manifest := do
   let obj ← JsonObject.fromJson? json
   let ver ← getVersion obj
+  let fixedToolchain ← obj.getD "fixedToolchain" false
   let name ← obj.getD "name" Name.anonymous
   let lakeDir ← obj.getD "lakeDir" defaultLakeDir
   let packagesDir? ← obj.get? "packagesDir"
   let packages ← getPackages ver obj
-  return {name, lakeDir, packagesDir?, packages}
+  return {name, lakeDir, packagesDir?, packages, fixedToolchain}
 
 public instance : FromJson Manifest := ⟨Manifest.fromJson?⟩
 

src/lake/Lake/Load/Materialize.lean

@@ -89,26 +89,33 @@ public structure MaterializedDep where
   Used as the endpoint from which to fetch cloud releases for the package.
   -/
   remoteUrl : String
+  /-- The manifest for the dependency or the error produced when trying to load it. -/
+  manifest? : Except IO.Error Manifest
   /-- The manifest entry for the dependency. -/
   manifestEntry : PackageEntry
   deriving Inhabited
 
 namespace MaterializedDep
 
-@[inline] public def name (self : MaterializedDep) :=
+@[inline] public def name (self : MaterializedDep) : Name :=
   self.manifestEntry.name
 
-@[inline] public def scope (self : MaterializedDep) :=
+@[inline] public def scope (self : MaterializedDep) : String :=
   self.manifestEntry.scope
 
 /-- Path to the dependency's configuration file (relative to `relPkgDir`). -/
-@[inline] public def manifestFile? (self : MaterializedDep) :=
+@[inline] public def manifestFile? (self : MaterializedDep) : Option FilePath :=
   self.manifestEntry.manifestFile?
 
 /-- Path to the dependency's configuration file (relative to `relPkgDir`). -/
-@[inline] public def configFile (self : MaterializedDep) :=
+@[inline] public def configFile (self : MaterializedDep) : FilePath :=
   self.manifestEntry.configFile
 
+public def fixedToolchain (self : MaterializedDep) : Bool :=
+  match self.manifest? with
+  | .ok manifest => manifest.fixedToolchain
+  | _ => false
+
 end MaterializedDep
 
 inductive InputVer
@@ -148,7 +155,7 @@ public def Dependency.materialize
     match src with
     | .path dir =>
       let relPkgDir := relParentDir / dir
-      return mkDep relPkgDir "" (.path relPkgDir)
+      mkDep (wsDir / relPkgDir) relPkgDir "" (.path relPkgDir)
     | .git url inputRev? subDir? => do
       let sname := dep.name.toString (escape := false)
       let repoUrl := Git.filterUrl? url |>.getD ""
@@ -196,16 +203,19 @@ public def Dependency.materialize
     | _ => error s!"{pkg.fullName}: Git source not found on Reservoir"
 where
   materializeGit name relPkgDir gitUrl remoteUrl inputRev? subDir? : LoggerIO MaterializedDep := do
-    let repo := GitRepo.mk (wsDir / relPkgDir)
+    let pkgDir := wsDir / relPkgDir
+    let repo := GitRepo.mk pkgDir
     let gitUrl := lakeEnv.pkgUrlMap.find? dep.name |>.getD gitUrl
     materializeGitRepo name repo gitUrl inputRev?
     let rev ← repo.getHeadRevision
     let relPkgDir := if let some subDir := subDir? then relPkgDir / subDir else relPkgDir
-    return mkDep relPkgDir remoteUrl <| .git gitUrl rev inputRev? subDir?
-  @[inline] mkDep relPkgDir remoteUrl src : MaterializedDep := {
-    relPkgDir, remoteUrl,
-    manifestEntry := {name := dep.name, scope := dep.scope, inherited, src}
-  }
+    mkDep pkgDir relPkgDir remoteUrl <| .git gitUrl rev inputRev? subDir?
+  @[inline] mkDep pkgDir relPkgDir remoteUrl src : LoggerIO MaterializedDep := do
+    return {
+      relPkgDir, remoteUrl
+      manifest? :=  ← Manifest.load (pkgDir / defaultManifestFile) |>.toBaseIO
+      manifestEntry := {name := dep.name, scope := dep.scope, inherited, src}
+    }
 
 /--
 Materializes a manifest package entry, cloning and/or checking it out as necessary.
@@ -216,7 +226,7 @@ public def PackageEntry.materialize
 : LoggerIO MaterializedDep :=
   match manifestEntry.src with
   | .path (dir := relPkgDir) .. =>
-    return mkDep relPkgDir ""
+    mkDep (wsDir / relPkgDir) relPkgDir ""
   | .git (url := url) (rev := rev) (subDir? := subDir?) .. => do
     let sname := manifestEntry.name.toString (escape := false)
     let relGitDir := relPkgsDir / sname
@@ -239,7 +249,12 @@ public def PackageEntry.materialize
       let url := lakeEnv.pkgUrlMap.find? manifestEntry.name |>.getD url
       cloneGitPkg sname repo url rev
     let relPkgDir := match subDir? with | .some subDir => relGitDir / subDir | .none => relGitDir
-    return mkDep relPkgDir (Git.filterUrl? url |>.getD "")
+    mkDep gitDir relPkgDir (Git.filterUrl? url |>.getD "")
 where
-  @[inline] mkDep relPkgDir remoteUrl : MaterializedDep :=
-    {relPkgDir, remoteUrl, manifestEntry}
+  @[inline] mkDep pkgDir relPkgDir remoteUrl : LoggerIO MaterializedDep := do
+    let manifest? ← id do
+      if let some manifestFile := manifestEntry.manifestFile? then
+        Manifest.load (pkgDir / manifestFile) |>.toBaseIO
+      else
+        return .error (.noFileOrDirectory "" 0 "")
+    return {relPkgDir, remoteUrl, manifest?, manifestEntry}

src/lake/Lake/Load/Resolve.lean

@@ -171,8 +171,8 @@ private def reuseManifest
     logWarning s!"{rootName}: ignoring previous manifest because it failed to load: {e}"
 
 /-- Add a package dependency's manifest entries to the update state. -/
-private def addDependencyEntries (pkg : Package) : UpdateT LoggerIO PUnit := do
-  match (← Manifest.load pkg.manifestFile |>.toBaseIO) with
+private def addDependencyEntries (pkg : Package) (matDep : MaterializedDep) : UpdateT LoggerIO PUnit := do
+  match matDep.manifest? with
   | .ok manifest =>
     manifest.packages.forM fun entry => do
       unless (← getThe (NameMap PackageEntry)).contains entry.name do
@@ -210,6 +210,36 @@ Used, for instance, if the toolchain is updated and no Elan is detected.
 -/
 def restartCode : ExitCode := 4
 
+/-- The toolchain information of a package. -/
+private structure ToolchainCandidate where
+  /-- The name of the package which provided the toolchain candidate. -/
+  src : Name
+  /-- The version of the toolchain candidate. -/
+  ver : ToolchainVer
+  /-- Whether the candidate toolchain been fixed to particular version. -/
+  fixed : Bool := false
+
+private structure ToolchainState where
+  /-- The name of depedency which provided the current candidate toolchain. -/
+  src : Name
+  /-- The current candidate toolchain version (if any). -/
+  tc? : Option ToolchainVer
+  /-- Incompatible candidate toolchains (if any). -/
+  clashes : Array ToolchainCandidate
+  /--
+  Whether the candidate toolchain been fixed to particular version.
+  If `false`, the search will update the toolchain further where possible.
+  -/
+  fixed : Bool
+
+@[inline] def ToolchainState.replace
+  (src : Name) (tc? : Option ToolchainVer) (fixed : Bool) (self : ToolchainState)
+: ToolchainState := {self with src, tc?, fixed}
+
+@[inline] def ToolchainState.addClash
+  (src : Name) (ver : ToolchainVer) (fixed : Bool) (self : ToolchainState)
+: ToolchainState := {self with clashes := self.clashes.push {src, ver, fixed}}
+
 /--
 Update the workspace's `lean-toolchain` if necessary.
 
@@ -222,23 +252,38 @@ def Workspace.updateToolchain
 : LoggerIO PUnit := do
   let rootToolchainFile := ws.root.dir / toolchainFileName
   let rootTc? ← ToolchainVer.ofDir? ws.dir
-  let (src, tc?, tcs) ← rootDeps.foldlM (init := (ws.root.baseName, rootTc?, #[])) fun s dep => do
+  let s : ToolchainState := ⟨ws.root.baseName, rootTc?, #[], ws.root.fixedToolchain⟩
+  let ⟨src, tc?, tcs, fixed⟩ ← rootDeps.foldlM (init := s) fun s dep => do
     let depTc? ← ToolchainVer.ofDir? (ws.dir / dep.relPkgDir)
     let some depTc := depTc?
       | return s
-    let (src, tc?, tcs) := s
-    let some tc := tc?
-      | return (dep.name, depTc?, tcs)
-    if depTc ≤ tc then
-      return (src, tc, tcs)
-    else if tc < depTc then
-      return (dep.name, depTc, tcs)
+    let some tc := s.tc?
+      | return s.replace dep.name depTc? dep.fixedToolchain
+    if dep.fixedToolchain then
+      if s.fixed then
+        if tc = depTc then
+          return s
+        else
+          return s.addClash dep.name depTc dep.fixedToolchain -- true
+      else
+        if tc ≤ depTc then
+          return s.replace dep.name depTc dep.fixedToolchain -- true
+        else
+          return s.addClash dep.name depTc dep.fixedToolchain -- true
     else
-      return (src, tc, tcs.push (dep.name, depTc))
+      if depTc ≤ tc then
+        return s
+      else if !s.fixed && tc < depTc then
+        return s.replace dep.name depTc dep.fixedToolchain -- false
+      else
+        return s.addClash dep.name depTc dep.fixedToolchain -- false
   if 0 < tcs.size then
     let s := "toolchain not updated; multiple toolchain candidates:"
-    let s := if let some tc := tc? then s!"{s}\n  {tc}\n    from {src}" else s
-    let s := tcs.foldl (init := s) fun s (d, tc) => s!"{s}\n  {tc}\n    from {d}"
+    let addEntry s tc src fixed :=
+      let fixed := if fixed then " (fixed toolchain)" else ""
+      s!"{s}\n  {tc}\n    from {src}{fixed}"
+    let s := if let some tc := tc? then addEntry s tc src fixed else s
+    let s := tcs.foldl (init := s) fun s ⟨src, tc, fixed⟩ => addEntry s tc src fixed
     logWarning s
   else if let some tc := tc? then
     if rootTc?.any (· == tc) then
@@ -333,7 +378,7 @@ where
     loadUpdatedDep wsIdx dep matDep
   @[inline] loadUpdatedDep wsIdx dep matDep : StateT Workspace (UpdateT LoggerIO) Package  := do
     let depPkg ← loadDepPackage wsIdx matDep dep.opts leanOpts true
-    addDependencyEntries depPkg
+    addDependencyEntries depPkg matDep
     return depPkg
 
 /-- Write package entries to the workspace manifest. -/
@@ -347,6 +392,7 @@ def Workspace.writeManifest
     | none => arr -- should only be the case for the root
   let manifest : Manifest := {
     name := ws.root.baseName
+    fixedToolchain := ws.root.fixedToolchain
     lakeDir := ws.relLakeDir
     packagesDir? := ws.relPkgsDir
     packages := manifestEntries

src/lake/schemas/lakefile-toml-schema.json

@@ -462,6 +462,11 @@
                     "default": false,
                     "description": "Whether downstream packages can `import all` modules of this package.\n\nIf enabled, downstream users will be able to access the `private` internals of modules, including definition bodies not marked as `@[expose]`. This may also, in the future, prevent compiler optimization which rely on `private` definitions being inaccessible outside their own package."
                 },
+                "fixedToolchain": {
+                    "type": "boolean",
+                    "default": false,
+                    "description": "Whether this package is expected to only function on a single toolchain (the package's toolchain).\n\nThis informs Lake's toolchain update procedure (in `lake update`) to prioritize this package's toolchain. It also avoids the need to separate input-to-output mappings for this package by toolchain version in the Lake cache."
+                },
                 "enableArtifactCache": {
                     "type": "boolean",
                     "description": "Whether to enables Lake's local, offline artifact cache for the package.\n\nArtifacts (i.e., build products) of packages will be shared across local copies by storing them in a cache associated with the Lean toolchain.\nThis can significantly reduce initial build times and disk space usage when working with multiple copies of large projects or large dependencies.\n\nAs a caveat, build targets which support the artifact cache will not be stored in their usual location within the build directory. Thus, projects with custom build scripts that rely on specific location of artifacts may wish to disable this feature.\n\nIf `none` (the default), this will fallback to (in order):\n* The `LAKE_ARTIFACT_CACHE` environment variable (if set).\n* The workspace root's `enableArtifactCache` configuration (if set and this package is a dependency).\n* **Lake's default**: The package can use artifacts from the cache, but cannot write to it."