move

CMakeLists.txt

@@ -129,7 +129,6 @@ 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

@@ -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/Init/Data/Array/QSort/Basic.lean

@@ -33,7 +33,6 @@ 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
@@ -45,7 +44,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 @[specialize] loop (as : Vector α n) (i k : Nat)
+  let rec 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/Compiler/LCNF/ExpandResetReuse.lean

@@ -90,22 +90,6 @@ partial def eraseProjIncFor (nFields : Nat) (targetId : FVarId) (ds : Array (Cod
         | break
       if !(w == z && targetId == x) then
         break
-      if mask[i]!.isSome then
-        /-
-        Suppose we encounter a situation like
-        ```
-        let x.1 := proj[0] y
-        inc x.1
-        let x.2 := proj[0] y
-        inc x.2
-        ```
-        The `inc x.2` will already have been removed. If we don't perform this check we will also
-        remove `inc x.1` and have effectively removed two refcounts while only one was legal.
-        -/
-        keep := keep.push d
-        keep := keep.push d'
-        ds := ds.pop.pop
-        continue
       /-
       Found
       ```

src/Lean/Elab/Inductive.lean

@@ -73,8 +73,6 @@ private def inductiveSyntaxToView (modifiers : Modifiers) (decl : Syntax) (isCoi
         throwError "Constructor cannot be `protected` because it is in a `private` inductive datatype"
       checkValidCtorModifier ctorModifiers
       let ctorName := ctor.getIdAt 3
-      if ctorName.hasMacroScopes && isCoinductive then
-        throwError "Coinductive predicates are not allowed inside of macro scopes"
       let ctorName := declName ++ ctorName
       let ctorName ← withRef ctor[3] <| applyVisibility ctorModifiers ctorName
       let (binders, type?) := expandOptDeclSig ctor[4]

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/Lean/Parser/Do.lean

@@ -66,14 +66,6 @@ def notFollowedByRedefinedTermToken :=
       "do" <|> "dbg_trace" <|> "idbg" <|> "assert!" <|> "debug_assert!" <|> "for" <|> "unless" <|> "return" <|> symbol "try")
     "token at 'do' element"
 
-namespace InternalSyntax
-/--
-Internal syntax used in the `if` and `unless` elaborators. Behaves like `pure PUnit.unit` but
-uses `()` if possible and gives better error messages.
--/
-scoped syntax (name := doSkip) "skip" : doElem
-end InternalSyntax
-
 @[builtin_doElem_parser] def doLet      := leading_parser
   "let " >> optional "mut " >> letConfig >> letDecl
 @[builtin_doElem_parser] def doLetElse  := leading_parser withPosition <|

src/Lean/Server/Completion/SyntheticCompletion.lean

@@ -117,13 +117,12 @@ private partial def isSyntheticTacticCompletion
     (cmdStx   : Syntax)
     : Bool := Id.run do
   let hoverFilePos := fileMap.toPosition hoverPos
-  go hoverFilePos cmdStx 0 none
+  go hoverFilePos cmdStx 0
 where
   go
-      (hoverFilePos         : Position)
-      (stx                  : Syntax)
-      (leadingWs            : Nat)
-      (leadingTokenTailPos? : Option String.Pos.Raw)
+      (hoverFilePos : Position)
+      (stx : Syntax)
+      (leadingWs : Nat)
       : Bool := Id.run do
     match stx.getPos?, stx.getTailPos? with
     | some startPos, some endPos =>
@@ -133,9 +132,8 @@ where
       if ! isCursorInCompletionRange then
         return false
       let mut wsBeforeArg := leadingWs
-      let mut lastArgTailPos? := leadingTokenTailPos?
       for arg in stx.getArgs do
-        if go hoverFilePos arg wsBeforeArg lastArgTailPos? then
+        if go hoverFilePos arg wsBeforeArg then
           return true
         -- We must account for the whitespace before an argument because the syntax nodes we use
         -- to identify tactic blocks only start *after* the whitespace following a `by`, and we
@@ -143,12 +141,7 @@ where
         -- This method of computing whitespace assumes that there are no syntax nodes without tokens
         -- after `by` and before the first proper tactic syntax.
         wsBeforeArg := arg.getTrailingSize
-        -- Track the tail position of the most recent preceding sibling that has a position so
-        -- that empty tactic blocks (which lack positions) can locate their opening token (e.g.
-        -- the `by` keyword) for indentation checking. The tail position lets us distinguish
-        -- cursors before and after the opener on the opener's line.
-        lastArgTailPos? := arg.getTailPos? <|> lastArgTailPos?
-      return isCompletionInEmptyTacticBlock stx lastArgTailPos?
+      return isCompletionInEmptyTacticBlock stx
         || isCompletionAfterSemicolon stx
         || isCompletionOnTacticBlockIndentation hoverFilePos stx
     | _, _ =>
@@ -157,7 +150,7 @@ where
       -- tactic blocks always occur within other syntax with ranges that let us narrow down the
       -- search to the degree that we can be sure that the cursor is indeed in this empty tactic
       -- block.
-      return isCompletionInEmptyTacticBlock stx leadingTokenTailPos?
+      return isCompletionInEmptyTacticBlock stx
 
   isCompletionOnTacticBlockIndentation
       (hoverFilePos : Position)
@@ -197,47 +190,8 @@ where
     else
       none
 
-  isCompletionInEmptyTacticBlock (stx : Syntax) (leadingTokenTailPos? : Option String.Pos.Raw) : Bool := Id.run do
-    if ! isCursorInProperWhitespace fileMap hoverPos then
-      return false
-    if ! isEmptyTacticBlock stx then
-      return false
-    -- Bracketed tactic blocks `{ ... }` are delimited by the braces themselves, so tactics
-    -- inserted in an empty bracketed block can appear at any column between the braces
-    -- (`withoutPosition` disables indentation constraints inside `tacticSeqBracketed`).
-    if stx.getKind == ``Parser.Tactic.tacticSeqBracketed then
-      let some openEndPos := stx[0].getTailPos?
-        | return false
-      let some closeStartPos := stx[2].getPos?
-        | return false
-      return openEndPos.byteIdx <= hoverPos.byteIdx && hoverPos.byteIdx <= closeStartPos.byteIdx
-    return isAtExpectedTacticIndentation leadingTokenTailPos?
-
-  -- After an empty tactic opener like `by`, tactics on a subsequent line must be inserted at an
-  -- increased indentation level (two spaces past the indentation of the line containing the
-  -- opener token). We mirror that here so that tactic completions are not offered in positions
-  -- where a tactic could not actually be inserted. On the same line as the opener, completions
-  -- are allowed only in the trailing whitespace past the opener — cursors earlier on the line
-  -- belong to the surrounding term, not to the tactic block.
-  isAtExpectedTacticIndentation (leadingTokenTailPos? : Option String.Pos.Raw) : Bool := Id.run do
-    let some tokenTailPos := leadingTokenTailPos?
-      | return true
-    let hoverFilePos := fileMap.toPosition hoverPos
-    let tokenTailFilePos := fileMap.toPosition tokenTailPos
-    if hoverFilePos.line == tokenTailFilePos.line then
-      return hoverPos.byteIdx >= tokenTailPos.byteIdx
-    let expectedColumn := countLeadingSpaces (fileMap.lineStart tokenTailFilePos.line) + 2
-    return hoverFilePos.column == expectedColumn
-
-  countLeadingSpaces (pos : String.Pos.Raw) : Nat := Id.run do
-    let mut p := pos
-    let mut n : Nat := 0
-    while ! p.atEnd fileMap.source do
-      if p.get fileMap.source != ' ' then
-        break
-      p := p.next fileMap.source
-      n := n + 1
-    return n
+  isCompletionInEmptyTacticBlock (stx : Syntax) : Bool :=
+    isCursorInProperWhitespace fileMap hoverPos && isEmptyTacticBlock stx
 
   isEmptyTacticBlock (stx : Syntax) : Bool :=
     stx.getKind == ``Parser.Tactic.tacticSeq && isEmpty stx

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