perf: specialize qsort properly onto the lt function

src/CMakeLists.txt

@@ -118,7 +118,6 @@ 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`")
 
@@ -128,7 +127,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 LEAN_EXTRA_LAKE_OPTS " --wfail")
+  string(APPEND LAKE_EXTRA_ARGS " --wfail")
   string(APPEND LEAN_EXTRA_MAKE_OPTS " -DwarningAsError=true")
 endif()
 

src/Lean/Meta/DecLevel.lean

@@ -69,16 +69,12 @@ 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,
-   instantiate and normalize it, and then decrement 1 to obtain `u`. -/
+   and then decrement 1 to obtain `u`. -/
 def getDecLevel (type : Expr) : MetaM Level := do
-  let l ← getLevel type
-  let l ← normalizeLevel l
-  decLevel l
+  decLevel (← getLevel type)
 
 def getDecLevel? (type : Expr) : MetaM (Option Level) := do
-  let l ← getLevel type
-  let l ← normalizeLevel l
-  decLevel? l
+  decLevel? (← getLevel type)
 
 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 ${LEAN_EXTRA_LAKE_OPTS} $(LAKE_EXTRA_ARGS)
+	${PREV_STAGE}/bin/lake build -f ${CMAKE_BINARY_DIR}/lakefile.toml $(LAKE_EXTRA_ARGS)
 
 Std Lean Lake Leanc LeanChecker LeanIR: Init
 

tests/elab/doForMutSortPoly.lean

@@ -1,11 +0,0 @@
-/-!
-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_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 Unit, 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 PUnit, 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
-  Unit
+  PUnit
 but is expected to have type
   List (Nat × Nat)