Merge remote-tracking branch 'origin/master' into byAsSorry_fixes

.github/workflows/check-prelude.yml

@@ -14,14 +14,15 @@ jobs:
           sparse-checkout: |
             src/Lean
             src/Std
+            src/lake/Lake
       - name: Check Prelude
         run: |
           failed_files=""
           while IFS= read -r -d '' file; do
             if ! grep -q "^prelude$" "$file"; then
               failed_files="$failed_files$file\n"
             fi
-          done < <(find src/Lean src/Std -name '*.lean' -print0)
+          done < <(find src/Lean src/Std src/lake/Lake -name '*.lean' -print0)
           if [ -n "$failed_files" ]; then
             echo -e "The following files should use 'prelude':\n$failed_files"
             exit 1

.github/workflows/pr-release.yml

@@ -34,7 +34,7 @@ jobs:
       - name: Download artifact from the previous workflow.
         if: ${{ steps.workflow-info.outputs.pullRequestNumber != '' }}
         id: download-artifact
-        uses: dawidd6/action-download-artifact@v6 # https://github.com/marketplace/actions/download-workflow-artifact
+        uses: dawidd6/action-download-artifact@v7 # https://github.com/marketplace/actions/download-workflow-artifact
         with:
           run_id: ${{ github.event.workflow_run.id }}
           path: artifacts
@@ -111,7 +111,7 @@ jobs:
 
       - name: 'Setup jq'
         if: ${{ steps.workflow-info.outputs.pullRequestNumber != '' }}
-        uses: dcarbone/install-jq-action@v2.1.0
+        uses: dcarbone/install-jq-action@v3.0.1
 
       # Check that the most recently nightly coincides with 'git merge-base HEAD master'
       - name: Check merge-base and nightly-testing-YYYY-MM-DD

script/mathlib-bench

@@ -0,0 +1,12 @@
+#! /bin/env bash
+# Open a Mathlib4 PR for benchmarking a given Lean 4 PR
+
+set -euo pipefail
+
+[ $# -eq 1 ] || (echo "usage: $0 <lean4 PR #>"; exit 1)
+
+LEAN_PR=$1
+PR_RESPONSE=$(gh api repos/leanprover-community/mathlib4/pulls -X POST -f head=lean-pr-testing-$LEAN_PR -f base=nightly-testing -f title="leanprover/lean4#$LEAN_PR benchmarking" -f draft=true -f body="ignore me")
+PR_NUMBER=$(echo "$PR_RESPONSE" | jq '.number')
+echo "opened https://github.com/leanprover-community/mathlib4/pull/$PR_NUMBER"
+gh api repos/leanprover-community/mathlib4/issues/$PR_NUMBER/comments -X POST -f body="!bench" > /dev/null

src/Init/Data/Array/Lemmas.lean

@@ -59,6 +59,14 @@ namespace List
 
 open Array
 
+theorem toArray_inj {a b : List α} (h : a.toArray = b.toArray) : a = b := by
+  cases a with
+  | nil => simpa using h
+  | cons a as =>
+    cases b with
+    | nil => simp at h
+    | cons b bs => simpa using h
+
 @[simp] theorem size_toArrayAux {a : List α} {b : Array α} :
     (a.toArrayAux b).size = b.size + a.length := by
   simp [size]
@@ -396,6 +404,11 @@ namespace Array
 
 /-! ## Preliminaries -/
 
+/-! ### toList -/
+
+theorem toList_inj {a b : Array α} (h : a.toList = b.toList) : a = b := by
+  cases a; cases b; simpa using h
+
 /-! ### empty -/
 
 @[simp] theorem empty_eq {xs : Array α} : #[] = xs ↔ xs = #[] := by

src/Init/Data/Vector/Lemmas.lean

@@ -11,6 +11,15 @@ import Init.Data.Vector.Basic
 Lemmas about `Vector α n`
 -/
 
+namespace Array
+
+theorem toVector_inj {a b : Array α} (h₁ : a.size = b.size) (h₂ : a.toVector.cast h₁ = b.toVector) : a = b := by
+  ext i ih₁ ih₂
+  · exact h₁
+  · simpa using congrArg (fun a => a[i]) h₂
+
+end Array
+
 namespace Vector
 
 @[simp] theorem getElem_mk {data : Array α} {size : data.size = n} {i : Nat} (h : i < n) :
@@ -239,6 +248,11 @@ theorem length_toList {α n} (xs : Vector α n) : xs.toList.length = n := by sim
 theorem getElem_toList {α n} (xs : Vector α n) (i : Nat) (h : i < xs.toList.length) :
     xs.toList[i] = xs[i]'(by simpa using h) := by simp
 
+theorem toList_inj {a b : Vector α n} (h : a.toList = b.toList) : a = b := by
+  rcases a with ⟨⟨a⟩, ha⟩
+  rcases b with ⟨⟨b⟩, hb⟩
+  simpa using h
+
 /-! ### Decidable quantifiers. -/
 
 theorem forall_zero_iff {P : Vector α 0 → Prop} :

src/Init/System/IO.lean

@@ -981,3 +981,14 @@ not used concurrently or which are already persistent.
 -/
 @[extern "lean_runtime_mark_persistent"]
 unsafe def Runtime.markPersistent (a : α) : BaseIO α := return a
+
+set_option linter.unusedVariables false in
+/--
+Discards the passed owned reference. This leads to `a` any any object reachable from it never being
+freed. This can be a useful optimization for eliding deallocation time of big object graphs that are
+kept alive close to the end of the process anyway (in which case calling `Runtime.markPersistent`
+would be similarly costly to deallocation). It is still considered a safe operation as it cannot
+lead to undefined behavior.
+-/
+@[extern "lean_runtime_forget"]
+def Runtime.forget (a : α) : BaseIO Unit := return

src/Lean/CoreM.lean

@@ -32,7 +32,7 @@ register_builtin_option maxHeartbeats : Nat := {
 }
 
 register_builtin_option Elab.async : Bool := {
-  defValue := false
+  defValue := true
   descr := "perform elaboration using multiple threads where possible"
 }
 
@@ -356,9 +356,7 @@ Returns the current log and then resets its messages while adjusting `MessageLog
 for incremental reporting during elaboration of a single command.
 -/
 def getAndEmptyMessageLog : CoreM MessageLog :=
-  modifyGet fun s => (s.messages, { s with
-    messages.unreported := {}
-    messages.hadErrors  := s.messages.hasErrors })
+  modifyGet fun s => (s.messages, { s with messages := s.messages.markAllReported })
 
 instance : MonadLog CoreM where
   getRef      := getRef
@@ -417,7 +415,7 @@ def wrapAsyncAsSnapshot (act : Unit → CoreM Unit) (desc : String := by exact d
     IO.FS.withIsolatedStreams (isolateStderr := stderrAsMessages.get (← getOptions)) do
       let tid ← IO.getTID
       -- reset trace state and message log so as not to report them twice
-      modify ({ · with messages := {}, traceState := { tid } })
+      modify fun st => { st with messages := st.messages.markAllReported, traceState := { tid } }
       try
         withTraceNode `Elab.async (fun _ => return desc) do
           act ()

src/Lean/Elab/BuiltinCommand.lean

@@ -488,6 +488,9 @@ where
     let mut lines : Array MessageData := #[]
     let decls ← getOptionDecls
     for (name, val) in opts do
+      -- `#guard_msgs` sets this option internally, we don't want it to end up in its output
+      if name == `Elab.async then
+        continue
       let (isSet, isUnknown) :=
         match decls.find? name with
         | some decl => (decl.defValue != val, false)

src/Lean/Elab/Command.lean

@@ -287,7 +287,9 @@ def runLinters (stx : Syntax) : CommandElabM Unit := do
               | Exception.internal _ _ =>
                 logException ex
             finally
-              modify fun s => { savedState with messages := s.messages }
+              -- TODO: it would be good to preserve even more state (#4363) but preserving info
+              -- trees currently breaks from linters adding context-less info nodes
+              modify fun s => { savedState with messages := s.messages, traceState := s.traceState }
 
 /--
 Catches and logs exceptions occurring in `x`. Unlike `try catch` in `CommandElabM`, this function
@@ -311,7 +313,7 @@ def wrapAsyncAsSnapshot (act : Unit → CommandElabM Unit)
     IO.FS.withIsolatedStreams (isolateStderr := Core.stderrAsMessages.get (← getOptions)) do
       let tid ← IO.getTID
       -- reset trace state and message log so as not to report them twice
-      modify ({ · with messages := {}, traceState := { tid } })
+      modify fun st => { st with messages := st.messages.markAllReported, traceState := { tid } }
       try
         withTraceNode `Elab.async (fun _ => return desc) do
           act ()
@@ -344,6 +346,17 @@ def wrapAsyncAsSnapshot (act : Unit → CommandElabM Unit)
 def logSnapshotTask (task : Language.SnapshotTask Language.SnapshotTree) : CommandElabM Unit :=
   modify fun s => { s with snapshotTasks := s.snapshotTasks.push task }
 
+def runLintersAsync (stx : Syntax) : CommandElabM Unit := do
+  if !Elab.async.get (← getOptions) then
+    withoutModifyingEnv do
+      runLinters stx
+    return
+
+  -- We only start one task for all linters for now as most linters are fast and we simply want
+  -- to unblock elaboration of the next command
+  let lintAct ← wrapAsyncAsSnapshot fun _ => runLinters stx
+  logSnapshotTask { range? := none, task := (← BaseIO.asTask lintAct) }
+
 protected def getCurrMacroScope : CommandElabM Nat  := do pure (← read).currMacroScope
 protected def getMainModule     : CommandElabM Name := do pure (← getEnv).mainModule
 
@@ -547,7 +560,7 @@ def elabCommandTopLevel (stx : Syntax) : CommandElabM Unit := withRef stx do pro
     -- rather than engineer a general solution.
     unless (stx.find? (·.isOfKind ``Lean.guardMsgsCmd)).isSome do
       withLogging do
-        runLinters stx
+        runLintersAsync stx
   finally
     -- note the order: first process current messages & info trees, then add back old messages & trees,
     -- then convert new traces to messages

src/Lean/Elab/Frontend.lean

@@ -169,6 +169,8 @@ def runFrontend
     IO.FS.writeFile ⟨out⟩ <| Json.compress <| toJson profile
 
   let hasErrors := snaps.getAll.any (·.diagnostics.msgLog.hasErrors)
+  -- no point in freeing the snapshot graph and all referenced data this close to process exit
+  Runtime.forget snaps
   pure (cmdState.env, !hasErrors)
 
 

src/Lean/Elab/GuardMsgs.lean

@@ -140,8 +140,12 @@ def MessageOrdering.apply (mode : MessageOrdering) (msgs : List String) : List S
         |>.trim |> removeTrailingWhitespaceMarker
     let (whitespace, ordering, specFn) ← parseGuardMsgsSpec spec?
     let initMsgs ← modifyGet fun st => (st.messages, { st with messages := {} })
+    -- disable async elaboration for `cmd` so `msgs` will contain all messages
+    let async := Elab.async.get (← getOptions)
+    modifyScope fun scope => { scope with opts := Elab.async.set scope.opts false }
     -- The `#guard_msgs` command is special-cased in `elabCommandTopLevel` to ensure linters only run once.
     elabCommandTopLevel cmd
+    modifyScope fun scope => { scope with opts := Elab.async.set scope.opts async }
     let msgs := (← get).messages
     let mut toCheck : MessageLog := .empty
     let mut toPassthrough : MessageLog := .empty

src/Lean/Elab/Tactic/BVDecide/Frontend/BVDecide/Reflect.lean

@@ -8,6 +8,7 @@ import Std.Data.HashMap
 import Std.Tactic.BVDecide.Bitblast.BVExpr.Basic
 import Lean.Meta.AppBuilder
 import Lean.ToExpr
+import Lean.Data.RArray
 
 /-!
 This module contains the implementation of the reflection monad, used by all other components of this
@@ -138,9 +139,11 @@ structure State where
   -/
   atoms : Std.HashMap Expr Atom := {}
   /--
-  A cache for `atomsAssignment`.
+  A cache for `atomsAssignment`. We maintain the invariant that this value is only used if
+  `atoms` is non empty. The reason for not using an `Option` is that it would pollute a lot of code
+  with error handling that is never hit as this invariant is enforced before all of this code.
   -/
-  atomsAssignmentCache : Expr := mkConst ``List.nil [.zero]
+  atomsAssignmentCache : Expr := mkConst `illegal
 
 /--
 The reflection monad, used to track `BitVec` variables that we see as we traverse the context.
@@ -157,9 +160,9 @@ structure ReifiedBVExpr where
   -/
   bvExpr : BVExpr width
   /--
-  A proof that `bvExpr.eval atomsAssignment = originalBVExpr`.
+  A proof that `bvExpr.eval atomsAssignment = originalBVExpr`, none if it holds by `rfl`.
   -/
-  evalsAtAtoms : M Expr
+  evalsAtAtoms : M (Option Expr)
   /--
   A cache for `toExpr bvExpr`.
   -/
@@ -174,9 +177,9 @@ structure ReifiedBVPred where
   -/
   bvPred : BVPred
   /--
-  A proof that `bvPred.eval atomsAssignment = originalBVPredExpr`.
+  A proof that `bvPred.eval atomsAssignment = originalBVPredExpr`, none if it holds by `rfl`.
   -/
-  evalsAtAtoms : M Expr
+  evalsAtAtoms : M (Option Expr)
   /--
   A cache for `toExpr bvPred`
   -/
@@ -191,9 +194,9 @@ structure ReifiedBVLogical where
   -/
   bvExpr : BVLogicalExpr
   /--
-  A proof that `bvExpr.eval atomsAssignment = originalBVLogicalExpr`.
+  A proof that `bvExpr.eval atomsAssignment = originalBVLogicalExpr`, none if it holds by `rfl`.
   -/
-  evalsAtAtoms : M Expr
+  evalsAtAtoms : M (Option Expr)
   /--
   A cache for `toExpr bvExpr`
   -/
@@ -228,9 +231,9 @@ def run (m : M α) : MetaM α :=
 /--
 Retrieve the atoms as pairs of their width and expression.
 -/
-def atoms : M (List (Nat × Expr)) := do
+def atoms : M (Array (Nat × Expr)) := do
   let sortedAtoms := (← getThe State).atoms.toArray.qsort (·.2.atomNumber < ·.2.atomNumber)
-  return sortedAtoms.map (fun (expr, {width, ..}) => (width, expr)) |>.toList
+  return sortedAtoms.map (fun (expr, {width, ..}) => (width, expr))
 
 /--
 Retrieve a `BitVec.Assignment` representing the atoms we found so far.
@@ -257,11 +260,37 @@ def lookup (e : Expr) (width : Nat) (synthetic : Bool) : M Nat := do
 where
   updateAtomsAssignment : M Unit := do
     let as ← atoms
-    let packed :=
-      as.map (fun (width, expr) => mkApp2 (mkConst ``BVExpr.PackedBitVec.mk) (toExpr width) expr)
-    let packedType := mkConst ``BVExpr.PackedBitVec
-    let newAtomsAssignment ← mkListLit packedType packed
-    modify fun s => { s with atomsAssignmentCache := newAtomsAssignment }
+    if h : 0 < as.size then
+      let ras := Lean.RArray.ofArray as h
+      let packedType := mkConst ``BVExpr.PackedBitVec
+      let pack := fun (width, expr) => mkApp2 (mkConst ``BVExpr.PackedBitVec.mk) (toExpr width) expr
+      let newAtomsAssignment := ras.toExpr packedType pack
+      modify fun s => { s with atomsAssignmentCache := newAtomsAssignment }
+    else
+      throwError "updateAtomsAssignment should only be called when there is an atom"
+
+@[specialize]
+def simplifyBinaryProof' (mkFRefl : Expr → Expr) (fst : Expr) (fproof : Option Expr)
+    (mkSRefl : Expr → Expr) (snd : Expr) (sproof : Option Expr) : Option (Expr × Expr) := do
+  match fproof, sproof with
+  | some fproof, some sproof => some (fproof, sproof)
+  | some fproof, none => some (fproof, mkSRefl snd)
+  | none, some sproof => some (mkFRefl fst, sproof)
+  | none, none => none
+
+@[specialize]
+def simplifyBinaryProof (mkRefl : Expr → Expr) (fst : Expr) (fproof : Option Expr) (snd : Expr)
+    (sproof : Option Expr) : Option (Expr × Expr) := do
+  simplifyBinaryProof' mkRefl fst fproof mkRefl snd sproof
+
+@[specialize]
+def simplifyTernaryProof (mkRefl : Expr → Expr) (fst : Expr) (fproof : Option Expr) (snd : Expr)
+    (sproof : Option Expr) (thd : Expr) (tproof : Option Expr) : Option (Expr × Expr × Expr) := do
+  match fproof, simplifyBinaryProof mkRefl snd sproof thd tproof with
+  | some fproof, some stproof => some (fproof, stproof)
+  | some fproof, none => some (fproof, mkRefl snd, mkRefl thd)
+  | none, some stproof => some (mkRefl fst, stproof)
+  | none, none => none
 
 end M
 

src/Lean/Elab/Tactic/BVDecide/Frontend/BVDecide/ReifiedBVExpr.lean

@@ -37,9 +37,8 @@ Register `e` as an atom of `width` that might potentially be `synthetic`.
 def mkAtom (e : Expr) (width : Nat) (synthetic : Bool) : M ReifiedBVExpr := do
   let ident ← M.lookup e width synthetic
   let expr := mkApp2 (mkConst ``BVExpr.var) (toExpr width) (toExpr ident)
-  let proof := do
-    let evalExpr ← mkEvalExpr width expr
-    return mkBVRefl width evalExpr
+  -- This is safe because this proof always holds definitionally.
+  let proof := pure none
   return ⟨width, .var ident, proof, expr⟩
 
 /--
@@ -70,9 +69,8 @@ Build a reified version of the constant `val`.
 def mkBVConst (val : BitVec w) : M ReifiedBVExpr := do
   let bvExpr : BVExpr w := .const val
   let expr := mkApp2 (mkConst ``BVExpr.const) (toExpr w) (toExpr val)
-  let proof := do
-    let evalExpr ← ReifiedBVExpr.mkEvalExpr w expr
-    return ReifiedBVExpr.mkBVRefl w evalExpr
+  -- This is safe because this proof always holds definitionally.
+  let proof := pure none
   return ⟨w, bvExpr, proof, expr⟩
 
 end ReifiedBVExpr