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.

src/CMakeLists.txt

@@ -118,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`")
 
@@ -127,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/Lean/Elab/BuiltinDo/Basic.lean

@@ -21,8 +21,7 @@ def elabDoIdDecl (x : Ident) (xType? : Option Term) (rhs : TSyntax `doElem) (k :
   let xType ← Term.elabType (xType?.getD (mkHole x))
   let lctx ← getLCtx
   let ctx ← read
-  let ref ← getRef -- store the surrounding reference for error messages in `k`
-  elabDoElem rhs <| .mk (kind := kind) x.getId xType do withRef ref do
+  elabDoElem rhs <| .mk (kind := kind) x.getId xType do
     withLCtxKeepingMutVarDefs lctx ctx x.getId do
       Term.addLocalVarInfo x (← getFVarFromUserName x.getId)
       k

src/Lean/Elab/Do/Basic.lean

@@ -416,18 +416,14 @@ def DoElemCont.mkBindUnlessPure (dec : DoElemCont) (e : Expr) : DoElabM Expr :=
     let k ← mkLambdaFVars #[xFVar] body
     mkBindApp eResultTy kResultTy e k
 
-def checkMonadicResultTypeMatches (resultType : Expr) (expectedType : Expr) : DoElabM Unit := do
-  unless ← isDefEqGuarded resultType expectedType do
-    throwError "Type mismatch. The rest of the `do` block has monadic result type{indentExpr resultType}\n\
-      but is expected to have monadic result type{indentExpr expectedType}"
-
 /--
 Return `let $k.resultName : PUnit := PUnit.unit; $(← k.k)`, ensuring that the result type of `k.k`
 is `PUnit` and then immediately zeta-reduce the `let`.
 -/
 def DoElemCont.continueWithUnit (dec : DoElemCont) : DoElabM Expr := do
-  checkMonadicResultTypeMatches dec.resultType (← mkPUnit)
-  mapLetDeclZeta dec.resultName (← mkPUnit) (← mkPUnitUnit) (nondep := true) (kind := .ofBinderName dec.resultName) fun _ =>
+  let unit ← mkPUnitUnit
+  discard <| Term.ensureHasType dec.resultType unit
+  mapLetDeclZeta dec.resultName (← mkPUnit) unit (nondep := true) (kind := .ofBinderName dec.resultName) fun _ =>
     dec.k
 
 /-- Elaborate the `DoElemCont` with the `deadCode` flag set to `deadSyntactically` to emit warnings. -/

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/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/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/issue12846.lean

@@ -1,23 +0,0 @@
-module
-
-set_option backward.do.legacy false
-
-/--
-error: Type mismatch. The rest of the `do` block has monadic result type
-  Bool
-but is expected to have monadic result type
-  Unit
--/
-#guard_msgs in
-def test : IO Bool := do
-  let a ← pure 25
-
-/--
-error: Type mismatch. The rest of the `do` block has monadic result type
-  Bool
-but is expected to have monadic result type
-  Unit
--/
-#guard_msgs in
-def test2 : IO Bool := do
-  let a := 25

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
@@ -58,7 +58,9 @@ but is expected to have type
   List (Nat × Nat)
 in the application
   pure ()
-doNotation1.lean:82:0-83:9: error: Type mismatch. The rest of the `do` block has monadic result type
+doNotation1.lean:82:0-83:9: error: Type mismatch
+  ()
+has type
+  Unit
+but is expected to have type
   List (Nat × Nat)
-but is expected to have monadic result type
-  PUnit