fix: pass CMake Lake args to the Lake make build (#13410)

This PR fixes a bug in #13294 where the Lake arguments were not actually
passed to the Lake make build.

CMakeLists.txt

@@ -129,6 +129,7 @@ if(USE_MIMALLOC)
     # cadical, it might be worth reorganizing the directory structure.
     SOURCE_DIR
     "${CMAKE_BINARY_DIR}/mimalloc/src/mimalloc"
+    EXCLUDE_FROM_ALL
   )
   FetchContent_MakeAvailable(mimalloc)
 endif()

src/CMakeLists.txt

@@ -110,6 +110,7 @@ option(RUNTIME_STATS "RUNTIME_STATS" OFF)
 option(BSYMBOLIC "Link with -Bsymbolic to reduce call overhead in shared libraries (Linux)" ON)
 option(USE_GMP "USE_GMP" ON)
 option(USE_MIMALLOC "use mimalloc" ON)
+set(LEAN_MI_SECURE 0 CACHE STRING "Configure mimalloc memory safety mitigations (https://github.com/microsoft/mimalloc/blob/v2.2.7/include/mimalloc/types.h#L56-L60)")
 
 # development-specific options
 option(CHECK_OLEAN_VERSION "Only load .olean files compiled with the current version of Lean" OFF)
@@ -117,6 +118,7 @@ option(USE_LAKE "Use Lake instead of lean.mk for building core libs from languag
 option(USE_LAKE_CACHE "Use the Lake artifact cache for stage 1 builds (requires USE_LAKE)" OFF)
 
 set(LEAN_EXTRA_OPTS "" CACHE STRING "extra options to lean (via lake or make)")
+set(LEAN_EXTRA_LAKE_OPTS "" CACHE STRING "extra options to lake")
 set(LEAN_EXTRA_MAKE_OPTS "" CACHE STRING "extra options to leanmake")
 set(LEANC_CC ${CMAKE_C_COMPILER} CACHE STRING "C compiler to use in `leanc`")
 
@@ -126,7 +128,7 @@ string(APPEND LEAN_EXTRA_OPTS " -Dbackward.do.legacy=false")
 # option used by the CI to fail on warnings
 option(WFAIL "Fail build if warnings are emitted by Lean" ON)
 if(WFAIL MATCHES "ON")
-  string(APPEND LAKE_EXTRA_ARGS " --wfail")
+  string(APPEND LEAN_EXTRA_LAKE_OPTS " --wfail")
   string(APPEND LEAN_EXTRA_MAKE_OPTS " -DwarningAsError=true")
 endif()
 

src/Init/Data/Array/QSort/Basic.lean

@@ -33,6 +33,7 @@ if necessary so that the middle (pivot) element is at index `hi`.
 We then iterate from `k = lo` to `k = hi`, with a pointer `i` starting at `lo`, and
 swapping each element which is less than the pivot to position `i`, and then incrementing `i`.
 -/
+@[inline]
 def qpartition {n} (as : Vector α n) (lt : α → α → Bool) (lo hi : Nat) (w : lo ≤ hi := by omega)
     (hlo : lo < n := by omega) (hhi : hi < n := by omega) : {m : Nat // lo ≤ m ∧ m ≤ hi} × Vector α n :=
   let mid := (lo + hi) / 2
@@ -44,7 +45,7 @@ def qpartition {n} (as : Vector α n) (lt : α → α → Bool) (lo hi : Nat) (w
   -- elements in `[i, k)` are greater than or equal to `pivot`,
   -- elements in `[k, hi)` are unexamined,
   -- while `as[hi]` is (by definition) the pivot.
-  let rec loop (as : Vector α n) (i k : Nat)
+  let rec @[specialize] loop (as : Vector α n) (i k : Nat)
       (ilo : lo ≤ i := by omega) (ik : i ≤ k := by omega) (w : k ≤ hi := by omega) :=
     if h : k < hi then
       if lt as[k] pivot then

src/Init/Data/String/Lemmas/Pattern/TakeDrop/Basic.lean

@@ -909,7 +909,7 @@ theorem Slice.Pos.skipWhile_copy {ρ : Type} {pat : ρ} [ForwardPattern pat] [Pa
   simp
 
 @[simp]
-theorem Pos.skipWhile_le {ρ : Type} {pat : ρ} [ForwardPattern pat] [PatternModel pat]
+theorem Pos.le_skipWhile {ρ : Type} {pat : ρ} [ForwardPattern pat] [PatternModel pat]
     [LawfulForwardPatternModel pat] {s : String} {pos : s.Pos} : pos ≤ pos.skipWhile pat := by
   simp [skipWhile_eq_skipWhile_toSlice, Pos.le_ofToSlice_iff]
 

src/Lean/Elab/BuiltinDo/For.lean

@@ -153,6 +153,9 @@ open Lean.Meta
 
   let body ←
     withLocalDeclsD xh fun xh => do
+    Term.addLocalVarInfo x xh[0]!
+    if let some h := h? then
+      Term.addLocalVarInfo h xh[1]!
     withLocalDecl s .default σ (kind := .implDetail) fun loopS => do
     mkLambdaFVars (xh.push loopS) <| ← do
     bindMutVarsFromTuple loopMutVarNames loopS.fvarId! do

src/Lean/Elab/Deriving/Inhabited.lean

@@ -89,7 +89,7 @@ where
       let val ←
         if isStructure (← getEnv) inductiveTypeName then
           withTraceNode `Elab.Deriving.inhabited (fun _ => return m!"using structure instance elaborator") do
-            let stx ← `(structInst| {..})
+            let stx ← `(structInstDefault| struct_inst_default%)
             withoutErrToSorry <| elabTermAndSynthesize stx type
         else
           withTraceNode `Elab.Deriving.inhabited (fun _ => return m!"using constructor `{.ofConstName ctorName}`") do

src/Lean/Elab/Do/Basic.lean

@@ -384,6 +384,7 @@ def DoElemCont.mkBindUnlessPure (dec : DoElemCont) (e : Expr) : DoElabM Expr :=
   let k := dec.k
   -- The .ofBinderName below is mainly to interpret `__do_lift` binders as implementation details.
   let declKind := .ofBinderName x
+  let kResultTy ← mkFreshResultType `kResultTy
   withLocalDecl x .default eResultTy (kind := declKind) fun xFVar => do
     let body ← k
     let body' := body.consumeMData
@@ -411,7 +412,6 @@ def DoElemCont.mkBindUnlessPure (dec : DoElemCont) (e : Expr) : DoElabM Expr :=
         -- else -- would be too aggressive
         --   return ← mapLetDecl (nondep := true) (kind := declKind) x eResultTy eRes fun _ => k ref
 
-    let kResultTy ← mkFreshResultType `kResultTy
     let body ← Term.ensureHasType (← mkMonadicType kResultTy) body
     let k ← mkLambdaFVars #[xFVar] body
     mkBindApp eResultTy kResultTy e k
@@ -545,7 +545,10 @@ def DoElemCont.withDuplicableCont (nondupDec : DoElemCont) (callerInfo : Control
     withDeadCode (if callerInfo.numRegularExits > 0 then .alive else .deadSemantically) do
     let e ← nondupDec.k
     mkLambdaFVars (#[r] ++ muts) e
-  discard <| joinRhsMVar.mvarId!.checkedAssign joinRhs
+  unless ← joinRhsMVar.mvarId!.checkedAssign joinRhs do
+    joinRhsMVar.mvarId!.withContext do
+      throwError "Bug in a `do` elaborator. Failed to assign join point RHS{indentExpr joinRhs}\n\
+        to metavariable\n{joinRhsMVar.mvarId!}"
 
   let body ← body?.getDM do
     -- Here we unconditionally add a pending MVar.

src/Lean/Elab/StructInst.lean

@@ -150,6 +150,8 @@ structure SourcesView where
   explicit : Array ExplicitSourceView
   /-- The syntax for a trailing `..`. This is "ellipsis mode" for missing fields, similar to ellipsis mode for applications. -/
   implicit : Option Syntax
+  /-- Use `Inhabited` instances inherited from parent structures, and use `default` instances for missing fields. -/
+  useInhabited : Bool
   deriving Inhabited
 
 /--
@@ -179,7 +181,7 @@ private def getStructSources (structStx : Syntax) : TermElabM SourcesView :=
         let structName ← getStructureName srcType
         return { stx, fvar := src, structName }
     let implicit := if implicitSource[0].isNone then none else implicitSource
-    return { explicit, implicit }
+    return { explicit, implicit, useInhabited := false }
 
 /--
 We say a structure instance notation is a "modifyOp" if it contains only a single array update.
@@ -579,6 +581,9 @@ private structure StructInstContext where
   /-- If true, then try using default values or autoParams for missing fields.
   (Considered after `useParentInstanceFields`.) -/
   useDefaults : Bool
+  /-- If true, then tries `Inhabited` instances as an alternative to parent instances,
+  and when default values are missing. -/
+  useInhabited : Bool
   /-- If true, then missing fields after default value synthesis remain as metavariables rather than yielding an error.
   Only applies if `useDefaults` is true. -/
   unsynthesizedAsMVars : Bool
@@ -735,14 +740,27 @@ The arguments for the `_default` auxiliary function are provided by `fieldMap`.
 After default values are resolved, then the one that is added to the environment
 as an `_inherited_default` auxiliary function is normalized; we don't do those normalizations here.
 -/
-private partial def getFieldDefaultValue? (fieldName : Name) : StructInstM (NameSet × Option Expr) := do
+private def getFieldDefaultValue? (fieldName : Name) : StructInstM (Option (NameSet × Expr)) := do
   let some defFn := getEffectiveDefaultFnForField? (← getEnv) (← read).structName fieldName
-    | return ({}, none)
+    | return none
   let fieldMap := (← get).fieldMap
   let some (fields, val) ← instantiateStructDefaultValueFn? defFn (← read).levels (← read).params (pure ∘ fieldMap.find?)
     | logError m!"default value for field `{fieldName}` of structure `{.ofConstName (← read).structName}` could not be instantiated, ignoring"
-      return ({}, none)
-  return (fields, val)
+      return none
+  return some (fields, val)
+
+/--
+If `useInhabited` is enabled, tries synthesizing an `Inhabited` instance for the field.
+-/
+private def getFieldDefaultValueUsingInhabited (fieldType : Expr) : StructInstM (Option (NameSet × Expr)) := do
+  if (← read).useInhabited then
+    try
+      let val ← mkDefault fieldType
+      return some ({}, val)
+    catch _ =>
+      return none
+  else
+    return none
 
 /--
 Auxiliary type for `synthDefaultFields`
@@ -751,8 +769,16 @@ private structure PendingField where
   fieldName : Name
   fieldType : Expr
   required : Bool
-  deps : NameSet
-  val? : Option Expr
+  /-- If present, field dependencies and the default value. -/
+  val? : Option (NameSet × Expr)
+
+private def PendingField.isReady (pendingField : PendingField) (hasDep : Name → Bool) : Bool :=
+  pendingField.val?.any fun (deps, _) => deps.all hasDep
+
+private def PendingField.val! (pendingField : PendingField) : Expr :=
+  match pendingField.val? with
+  | some (_, val) => val
+  | none          => panic! "PendingField has no value"
 
 private def registerFieldMVarError (e : Expr) (ref : Syntax) (fieldName : Name) : StructInstM Unit :=
   registerCustomErrorIfMVar e ref m!"Cannot synthesize placeholder for field `{fieldName}`"
@@ -786,12 +812,15 @@ private def synthOptParamFields : StructInstM Unit := do
   -- Process default values for pending optParam fields.
   let mut pendingFields : Array PendingField ← optParamFields.filterMapM fun (fieldName, fieldType, required) => do
     if required || (← isFieldNotSolved? fieldName).isSome then
-      let (deps, val?) ← if (← read).useDefaults then getFieldDefaultValue? fieldName else pure ({}, none)
-      if let some val := val? then
-        trace[Elab.struct] "default value for {fieldName}:{indentExpr val}"
-      else
-        trace[Elab.struct] "no default value for {fieldName}"
-      pure <| some { fieldName, fieldType, required, deps, val? }
+      let val? ← if (← read).useDefaults then getFieldDefaultValue? fieldName else pure none
+      let val? ← pure val? <||> if (← read).useInhabited then getFieldDefaultValueUsingInhabited fieldType else pure none
+      trace[Elab.struct]
+        if let some (deps, val) := val? then
+          m!"default value for {fieldName}:{inlineExpr val}" ++
+          if deps.isEmpty then m!"" else m!"(depends on fields {deps.toArray})"
+        else
+          m!"no default value for {fieldName}"
+      pure <| some { fieldName, fieldType, required, val? }
     else
       pure none
   -- We then iteratively look for pending fields that do not depend on unsolved-for fields.
@@ -799,12 +828,11 @@ private def synthOptParamFields : StructInstM Unit := do
   -- so we need to keep trying until no more progress is made.
   let mut pendingSet : NameSet := pendingFields.foldl (init := {}) fun set pending => set.insert pending.fieldName
   while !pendingSet.isEmpty do
-    let selectedFields := pendingFields.filter fun pendingField =>
-      pendingField.val?.isSome && pendingField.deps.all (fun dep => !pendingSet.contains dep)
+    let selectedFields := pendingFields.filter (·.isReady (!pendingSet.contains ·))
     let mut toRemove : Array Name := #[]
     let mut assignErrors : Array MessageData := #[]
     for selected in selectedFields do
-      let some selectedVal := selected.val? | unreachable!
+      let selectedVal := selected.val!
       if let some mvarId ← isFieldNotSolved? selected.fieldName then
         let fieldType := selected.fieldType
         let selectedType ← inferType selectedVal
@@ -1084,6 +1112,7 @@ private def processNoField (loop : StructInstM α) (fieldName : Name) (binfo : B
         addStructFieldAux fieldName mvar
         return ← loop
   -- Default case: natural metavariable, register it for optParams
+  let fieldType := fieldType.consumeTypeAnnotations
   discard <| addStructFieldMVar fieldName fieldType
   modify fun s => { s with optParamFields := s.optParamFields.push (fieldName, fieldType, binfo.isExplicit) }
   loop
@@ -1111,29 +1140,44 @@ private partial def loop : StructInstM Expr := withViewRef do
 For each parent class, see if it can be used to synthesize the fields that haven't been provided.
 -/
 private partial def addParentInstanceFields : StructInstM Unit := do
-  let env ← getEnv
   let structName := (← read).structName
-  let fieldNames := getStructureFieldsFlattened env structName (includeSubobjectFields := false)
+  let fieldNames := getStructureFieldsFlattened (← getEnv) structName (includeSubobjectFields := false)
   let fieldViews := (← read).fieldViews
   if fieldNames.all fieldViews.contains then
     -- Every field is accounted for already
     return
 
-  -- We look at class parents in resolution order
+  -- We look at parents in resolution order
   let parents ← getAllParentStructures structName
-  let classParents := parents.filter (isClass env)
-  if classParents.isEmpty then return
+  let env ← getEnv
+  let parentsToVisit := if (← read).useInhabited then parents else parents.filter (isClass env)
+  if parentsToVisit.isEmpty then return
 
   let allowedFields := fieldNames.filter (!fieldViews.contains ·)
   let mut remainingFields := allowedFields
 
   -- Worklist of parent/fields pairs. If fields is empty, then it will be computed later.
-  let mut worklist : List (Name × Array Name) := classParents |>.map (·, #[]) |>.toList
+  let mut worklist : List (Name × Array Name) := parentsToVisit |>.map (·, #[]) |>.toList
   let mut deferred : List (Name × Array Name) := []
 
+  let trySynthParent (parentName : Name) (parentTy : Expr) : StructInstM (LOption Expr) := do
+    if isClass (← getEnv) parentName then
+      match ← trySynthInstance parentTy with
+      | .none => pure ()
+      | r     => return r
+    if (← read).useInhabited then
+      let u ← getLevel parentTy
+      let cls := Expr.app (Expr.const ``Inhabited [u]) parentTy
+      match ← trySynthInstance cls with
+      | .none      => pure ()
+      | .undef     => return .undef
+      | .some inst => return .some <| mkApp2 (Expr.const ``Inhabited.default [u]) parentTy inst
+    return .none
+
   while !worklist.isEmpty do
     let (parentName, parentFields) :: worklist' := worklist | unreachable!
     worklist := worklist'
+    let env ← getEnv
     let parentFields := if parentFields.isEmpty then getStructureFieldsFlattened env parentName (includeSubobjectFields := false) else parentFields
     -- We only try synthesizing if the parent contains one of the remaining fields
     -- and if every parent field is an allowed field.
@@ -1145,7 +1189,7 @@ private partial def addParentInstanceFields : StructInstM Unit := do
         trace[Elab.struct] "could not calculate type for parent `{.ofConstName parentName}`"
         deferred := (parentName, parentFields) :: deferred
       | some (parentTy, _) =>
-        match ← trySynthInstance parentTy with
+        match ← trySynthParent parentName parentTy with
         | .none => trace[Elab.struct] "failed to synthesize instance for parent {parentTy}"
         | .undef =>
           trace[Elab.struct] "instance synthesis stuck for parent {parentTy}"
@@ -1199,17 +1243,19 @@ private def elabStructInstView (s : StructInstView) (structName : Name) (structT
   let fields ← addSourceFields structName s.sources.explicit fields
   trace[Elab.struct] "expanded fields:\n{MessageData.joinSep (fields.toList.map (fun (_, field) => m!"- {MessageData.nestD (toMessageData field)}")) "\n"}"
   let ellipsis := s.sources.implicit.isSome
+  let useInhabited := s.sources.useInhabited
   let (val, _) ← main
     |>.run { view := s, structName, structType, levels, params, fieldViews := fields, val := ctorFn
              -- See the note in `ElabAppArgs.processExplicitArg`
              -- For structure instances though, there's a sense in which app-style ellipsis mode is always enabled,
              -- so we do not specifically check for it to disable defaults.
              -- An effect of this is that if a user forgets `..` they'll be reminded with a "Fields missing" error.
-             useDefaults := !(← readThe Term.Context).inPattern
+             useDefaults := !(← readThe Term.Context).inPattern || useInhabited
              -- Similarly, for patterns we disable using parent instances to fill in fields
-             useParentInstanceFields := !(← readThe Term.Context).inPattern
+             useParentInstanceFields := !(← readThe Term.Context).inPattern || useInhabited
              -- In ellipsis mode, unsynthesized missing fields become metavariables, rather than being an error
              unsynthesizedAsMVars := ellipsis
+             useInhabited := useInhabited
      }
     |>.run { type := ctorFnType }
   return val
@@ -1333,6 +1379,15 @@ where
       trace[Elab.struct] "result:{indentExpr r}"
       return r
 
+@[builtin_term_elab structInstDefault] def elabStructInstDefault : TermElab := fun stx expectedType? => do
+  let sourcesView : SourcesView := { explicit := #[], implicit := none, useInhabited := true }
+  let (structName, structType?) ← getStructName expectedType? sourcesView
+  withTraceNode `Elab.struct (fun _ => return m!"elaborating default value for `{structName}`") do
+    let struct : StructInstView := { ref := stx, fields := #[], sources := sourcesView }
+    let r ← withSynthesize (postpone := .yes) <| elabStructInstView struct structName structType?
+    trace[Elab.struct] "result:{indentExpr r}"
+    return r
+
 builtin_initialize
   registerTraceClass `Elab.struct
   registerTraceClass `Elab.struct.modifyOp

src/Lean/Meta/DecLevel.lean

@@ -69,12 +69,16 @@ def decLevel (u : Level) : MetaM Level := do
 
 /-- This method is useful for inferring universe level parameters for function that take arguments such as `{α : Type u}`.
    Recall that `Type u` is `Sort (u+1)` in Lean. Thus, given `α`, we must infer its universe level,
-   and then decrement 1 to obtain `u`. -/
+   instantiate and normalize it, and then decrement 1 to obtain `u`. -/
 def getDecLevel (type : Expr) : MetaM Level := do
-  decLevel (← getLevel type)
+  let l ← getLevel type
+  let l ← normalizeLevel l
+  decLevel l
 
 def getDecLevel? (type : Expr) : MetaM (Option Level) := do
-  decLevel? (← getLevel type)
+  let l ← getLevel type
+  let l ← normalizeLevel l
+  decLevel? l
 
 builtin_initialize
   registerTraceClass `Meta.isLevelDefEq.step

src/Lean/Parser/Term.lean

@@ -354,6 +354,13 @@ def structInstFieldDef := leading_parser
 def structInstFieldEqns := leading_parser
   optional "private" >> matchAlts
 
+/--
+Synthesizes a default value for a structure, making use of `Inhabited` instances for
+missing fields, as well as `Inhabited` instances for parent structures.
+-/
+@[builtin_term_parser] def structInstDefault := leading_parser
+  "struct_inst_default%"
+
 def funImplicitBinder := withAntiquot (mkAntiquot "implicitBinder" ``implicitBinder) <|
   atomic (lookahead ("{" >> many1 binderIdent >> (symbol " : " <|> "}"))) >> implicitBinder
 def funStrictImplicitBinder :=

src/Std/Internal/Http/Protocol/H1/Parser.lean

@@ -260,7 +260,7 @@ and returns the `RequestTarget` together with the raw major/minor version number
 Both `parseRequestLine` and `parseRequestLineRawVersion` call this after consuming
 the method token, keeping URI validation and version parsing in one place.
 -/
-private def parseRequestLineBody (limits : H1.Config) : Parser (RequestTarget × Nat × Nat) := do
+def parseRequestLineBody (limits : H1.Config) : Parser (RequestTarget × Nat × Nat) := do
   let rawUri ← parseURI limits <* sp
   let uri ← match (Std.Http.URI.Parser.parseRequestTarget <* eof).run rawUri with
   | .ok res => pure res
@@ -446,7 +446,7 @@ Returns `true` if `name` (compared case-insensitively) is a field that MUST NOT
 trailer sections per RFC 9112 §6.5. Forbidden fields are those required for message framing
 (`content-length`, `transfer-encoding`), routing (`host`), or connection management (`connection`).
 -/
-private def isForbiddenTrailerField (name : String) : Bool :=
+def isForbiddenTrailerField (name : String) : Bool :=
   let n := name.toLower
   n == "content-length" || n == "transfer-encoding" || n == "host" ||
   n == "connection" || n == "expect" || n == "te" ||

src/runtime/CMakeLists.txt

@@ -39,7 +39,7 @@ if(USE_MIMALLOC)
   # Lean code includes it as `lean/mimalloc.h` but for compiling `static.c` itself, add original dir
   include_directories(${LEAN_BINARY_DIR}/../mimalloc/src/mimalloc/include)
   # make all symbols visible, always build with optimizations as otherwise Lean becomes too slow
-  set(MIMALLOC_FLAGS "-DMI_SHARED_LIB -DMI_SHARED_LIB_EXPORT -O3 -DNDEBUG -DMI_WIN_NOREDIRECT -Wno-unused-function")
+  set(MIMALLOC_FLAGS "-DMI_SHARED_LIB -DMI_SHARED_LIB_EXPORT -O3 -DNDEBUG -DMI_WIN_NOREDIRECT -DMI_SECURE=${LEAN_MI_SECURE} -Wno-unused-function")
   if(CMAKE_CXX_COMPILER_ID MATCHES "AppleClang|Clang")
     string(APPEND MIMALLOC_FLAGS " -Wno-deprecated")
   endif()

src/stdlib.make.in

@@ -54,7 +54,7 @@ ifeq "${USE_LAKE}" "ON"
 
 # build in parallel
 Init:
-	${PREV_STAGE}/bin/lake build -f ${CMAKE_BINARY_DIR}/lakefile.toml $(LAKE_EXTRA_ARGS)
+	${PREV_STAGE}/bin/lake build -f ${CMAKE_BINARY_DIR}/lakefile.toml ${LEAN_EXTRA_LAKE_OPTS} $(LAKE_EXTRA_ARGS)
 
 Std Lean Lake Leanc LeanChecker LeanIR: Init
 

tests/compile_bench/io_compute.lean

@@ -0,0 +1,82 @@
+/-! Mixing basic IO actions and heavy unboxed compute -/
+
+def N : Nat := 12500000 / 2 -- ~50 MB
+
+-- xorshift64* PRNG (same algorithm as Rust version)
+@[inline] def xorshift64 (state : UInt64) : UInt64 × UInt64 :=
+  let x := state ^^^ (state >>> 12)
+  let x := x ^^^ (x <<< 25)
+  let x := x ^^^ (x >>> 27)
+  (x, x * 0x2545F4914F6CDD1D)
+
+-- Push UInt64 as 8 little-endian bytes
+@[inline] def pushLE (ba : ByteArray) (v : UInt64) : ByteArray :=
+  let ba := ba.push (v &&& 0xFF).toUInt8
+  let ba := ba.push ((v >>> 8) &&& 0xFF).toUInt8
+  let ba := ba.push ((v >>> 16) &&& 0xFF).toUInt8
+  let ba := ba.push ((v >>> 24) &&& 0xFF).toUInt8
+  let ba := ba.push ((v >>> 32) &&& 0xFF).toUInt8
+  let ba := ba.push ((v >>> 40) &&& 0xFF).toUInt8
+  let ba := ba.push ((v >>> 48) &&& 0xFF).toUInt8
+  ba.push ((v >>> 56) &&& 0xFF).toUInt8
+
+-- Read UInt64 from 8 little-endian bytes at offset
+@[inline] def readLE (ba : ByteArray) (off : Nat) : UInt64 :=
+  (ba.get! off).toUInt64 +
+  ((ba.get! (off + 1)).toUInt64 <<< 8) +
+  ((ba.get! (off + 2)).toUInt64 <<< 16) +
+  ((ba.get! (off + 3)).toUInt64 <<< 24) +
+  ((ba.get! (off + 4)).toUInt64 <<< 32) +
+  ((ba.get! (off + 5)).toUInt64 <<< 40) +
+  ((ba.get! (off + 6)).toUInt64 <<< 48) +
+  ((ba.get! (off + 7)).toUInt64 <<< 56)
+
+def timeS {α : Type} (act : IO α) : IO (α × Float) := do
+  let t0 ← IO.monoMsNow
+  let r ← act
+  let t1 ← IO.monoMsNow
+  return (r, (t1 - t0).toFloat / 1000.0)
+
+def main : IO Unit := do
+  -- Phase 1: Generate & Sort
+  let (data, elapsed) ← timeS do
+    let mut state : UInt64 := 42
+    let mut arr : Array UInt64 := Array.mkEmpty N
+    for _ in [:N] do
+      let (s, v) := xorshift64 state
+      state := s
+      arr := arr.push v
+    return arr.qsortOrd
+  IO.println s!"measurement: generate_sort {elapsed} s"
+
+  let (_, file) ← IO.FS.createTempFile
+  -- Phase 2: Write
+  let (_, elapsed) ← timeS do
+    let mut ba := ByteArray.emptyWithCapacity (N * 8)
+    for i in [:data.size] do
+      ba := pushLE ba data[i]!
+    IO.FS.writeBinFile file ba
+  IO.println s!"measurement: write {elapsed} s"
+
+  -- Phase 3: Read
+  let (data, elapsed) ← timeS do
+    let ba ← IO.FS.readBinFile file
+    let mut arr : Array UInt64 := Array.mkEmpty N
+    for i in [:N] do
+      arr := arr.push (readLE ba (i * 8))
+    return arr
+  IO.println s!"measurement: read {elapsed} s"
+
+  -- Phase 4: Fisher-Yates shuffle
+  let (_, elapsed) ← timeS do
+    let mut arr := data
+    let mut state : UInt64 := 42
+    for i' in [:N - 1] do
+      let i := N - 1 - i'
+      let (s, v) := xorshift64 state
+      state := s
+      let j := (v % (i + 1).toUInt64).toNat
+      arr := arr.swapIfInBounds i j
+    return arr
+  IO.println s!"measurement: shuffle {elapsed} s"
+

tests/compile_bench/io_compute.lean.out.expected

@@ -0,0 +1,4 @@
+measurement: generate_sort ...
+measurement: write ...
+measurement: read ...
+measurement: shuffle ...

tests/elab/9463.lean

@@ -123,3 +123,34 @@ structure MyNS.MyStruct where
 #guard_msgs in #check MyNS.instInhabitedMyStruct.default
 /-- info: MyNS.instInhabitedMyStruct : Inhabited MyNS.MyStruct -/
 #guard_msgs in #check MyNS.instInhabitedMyStruct
+
+/-!
+Fix for https://github.com/leanprover/lean4/issues/13372
+Should inherit parent structures' Inhabited instances.
+-/
+
+structure Foo where
+  n : Nat
+  m : Nat
+  h : n ≤ m
+
+instance : Inhabited Foo where
+  default := ⟨5, 5, Nat.le.refl⟩
+
+-- Was: "failed to generate Inhabited instance for Bar"
+structure Bar extends Foo where
+  extra : Bool := true
+  a : Nat
+  deriving Inhabited
+
+/-- info: 5 -/
+#guard_msgs in #eval (default : Bar).n
+/-- info: true -/
+#guard_msgs in #eval (default : Bar).extra
+/-- info: 0 -/
+#guard_msgs in #eval (default : Bar).a
+
+/-- info: Bar.mk default true default : Bar -/
+#guard_msgs in
+set_option pp.structureInstances false in
+#check (struct_inst_default% : Bar)

tests/elab/doForMutSortPoly.lean

@@ -0,0 +1,11 @@
+/-!
+Test that `for` loops with `mut` variables of sort-polymorphic type (e.g. `PProd`) work correctly.
+`PProd Nat True : Sort (max 1 0)` has a `Prop` component, so `getDecLevel` must see the fully
+instantiated and normalized level `1` rather than `max ?u ?v` with unresolved metavariables.
+-/
+
+def foo : Unit := Id.run do
+  let mut x : PProd Nat True := ⟨0, trivial⟩
+  for _ in [true] do
+    x := ⟨0, trivial⟩
+    break

tests/elab/due_to_metavariables.lean

@@ -101,7 +101,7 @@ would also work here.
 error: Application type mismatch: The argument
   isDigitEven? n
 has type
-  ?m.2 Bool
+  ?m.3 Bool
 but is expected to have type
   Prop
 in the application

tests/elab/issue12768.lean

@@ -0,0 +1,13 @@
+module
+
+set_option backward.do.legacy false
+
+set_option linter.unusedVariables.funArgs false in
+def Quoted (x : Nat) := Nat
+
+def withStuff (x : Nat) (f : IO (Quoted x)) : IO (Quoted x) := f
+
+def myFunc : IO Nat := do
+  let val : Nat ← pure 3
+  withStuff val do
+    return (3 : Nat)

tests/elab/issue12826.lean

@@ -0,0 +1,27 @@
+import Lean
+
+syntax (name := testElem) "test" : doElem
+
+open Lean Elab Do
+@[doElem_elab testElem]
+def elabTestElem : DoElab := fun _stx _dec => do
+  return .fvar ⟨`bad_fvar⟩
+
+@[doElem_control_info testElem]
+def controlInfoTestElem : ControlInfoHandler := fun _stx => do
+  return .pure
+
+set_option backward.do.legacy false
+
+/--
+error: Bug in a `do` elaborator. Failed to assign join point RHS
+  fun __r => bad_fvar
+to metavariable
+⊢ Unit → IO Unit
+-/
+#guard_msgs in
+def testFn : IO Unit := do
+  if true then pure () else pure () -- uses `withDuplicableCont`
+  test -- produces a term that `checkedAssign` will reject
+
+set_option pp.mvars false

tests/elab/newdo.lean

@@ -108,7 +108,7 @@ Hint: Adding type annotations and supplying implicit arguments to functions can
 example := do return 42
 /--
 error: typeclass instance problem is stuck
-  Bind ?m.23
+  Bind ?m.22
 
 Note: Lean will not try to resolve this typeclass instance problem because the type argument to `Bind` is a metavariable. This argument must be fully determined before Lean will try to resolve the typeclass.
 
@@ -211,8 +211,8 @@ trace: [Elab.do] let x := 42;
               else
                 let x := x + i;
                 pure (ForInStep.yield (none, x))
-    let __r : Option ?m.182 := __s.fst
-    let x : ?m.182 := __s.snd
+    let __r : Option ?m.185 := __s.fst
+    let x : ?m.185 := __s.snd
     match __r with
       | some r => pure r
       | none =>

tests/elab_fail/doNotation1.lean.out.expected

@@ -49,7 +49,7 @@ doNotation1.lean:78:21-78:31: error: typeclass instance problem is stuck
 Note: Lean will not try to resolve this typeclass instance problem because the type argument to `ToString` is a metavariable. This argument must be fully determined before Lean will try to resolve the typeclass.
 
 Hint: Adding type annotations and supplying implicit arguments to functions can give Lean more information for typeclass resolution. For example, if you have a variable `x` that you intend to be a `Nat`, but Lean reports it as having an unresolved type like `?m`, replacing `x` with `(x : Nat)` can get typeclass resolution un-stuck.
-doNotation1.lean:82:0-83:9: error: Type mismatch. `for` loops have result type PUnit, but the rest of the `do` sequence expected List (Nat × Nat).
+doNotation1.lean:82:0-83:9: error: Type mismatch. `for` loops have result type Unit, but the rest of the `do` sequence expected List (Nat × Nat).
 doNotation1.lean:83:7-83:9: error: Application type mismatch: The argument
   ()
 has type
@@ -59,8 +59,8 @@ but is expected to have type
 in the application
   pure ()
 doNotation1.lean:82:0-83:9: error: Type mismatch
-  PUnit.unit
+  ()
 has type
-  PUnit
+  Unit
 but is expected to have type
   List (Nat × Nat)

tests/server_interactive/hoverDoForIn.lean

@@ -0,0 +1,7 @@
+set_option backward.do.legacy false
+
+def test : IO Unit := do
+  for h : i in [1, 2, 3] do
+    --^ textDocument/hover
+        --^ textDocument/hover
+    pure ()

tests/server_interactive/hoverDoForIn.lean.out.expected

@@ -0,0 +1,10 @@
+{"textDocument": {"uri": "file:///hoverDoForIn.lean"},
+ "position": {"line": 3, "character": 6}}
+{"range":
+ {"start": {"line": 3, "character": 6}, "end": {"line": 3, "character": 7}},
+ "contents": {"value": "```lean\nh : i ∈ [1, 2, 3]\n```", "kind": "markdown"}}
+{"textDocument": {"uri": "file:///hoverDoForIn.lean"},
+ "position": {"line": 3, "character": 10}}
+{"range":
+ {"start": {"line": 3, "character": 10}, "end": {"line": 3, "character": 11}},
+ "contents": {"value": "```lean\ni : Nat\n```", "kind": "markdown"}}