Merge branch 'nightly' of github.com:leanprover/lean4 into joachim/ze…

…ta-unused-impl

CMakePresets.json

@@ -26,7 +26,7 @@
       "displayName": "Sanitize build config",
       "cacheVariables": {
         "LEAN_EXTRA_CXX_FLAGS": "-fsanitize=address,undefined",
-        "LEANC_EXTRA_FLAGS": "-fsanitize=address,undefined -fsanitize-link-c++-runtime",
+        "LEANC_EXTRA_CC_FLAGS": "-fsanitize=address,undefined -fsanitize-link-c++-runtime",
         "SMALL_ALLOCATOR": "OFF",
         "BSYMBOLIC": "OFF"
       },

src/Init/Core.lean

@@ -516,8 +516,17 @@ The tasks have an overridden representation in the runtime.
 structure Task (α : Type u) : Type u where
   /-- `Task.pure (a : α)` constructs a task that is already resolved with value `a`. -/
   pure ::
-  /-- If `task : Task α` then `task.get : α` blocks the current thread until the
-  value is available, and then returns the result of the task. -/
+  /--
+  Blocks the current thread until the given task has finished execution, and then returns the result
+  of the task. If the current thread is itself executing a (non-dedicated) task, the maximum
+  threadpool size is temporarily increased by one while waiting so as to ensure the process cannot
+  be deadlocked by threadpool starvation. Note that when the current thread is unblocked, more tasks
+  than the configured threadpool size may temporarily be running at the same time until sufficiently
+  many tasks have finished.
+
+  `Task.map` and `Task.bind` should be preferred over `Task.get` for setting up task dependencies
+  where possible as they do not require temporarily growing the threadpool in this way.
+  -/
   get : α
   deriving Inhabited, Nonempty
 

src/Lean/AddDecl.lean

@@ -50,18 +50,49 @@ where go env
   | _        => env
 
 def addDecl (decl : Declaration) : CoreM Unit := do
-  profileitM Exception "type checking" (← getOptions) do
-    let mut env ← withTraceNode `Kernel (fun _ => return m!"typechecking declaration") do
-      if !(← MonadLog.hasErrors) && decl.hasSorry then
-        logWarning "declaration uses 'sorry'"
-      (← getEnv).addDeclAux (← getOptions) decl (← read).cancelTk? |> ofExceptKernelException
+  let mut env ← getEnv
+  -- register namespaces for newly added constants; this used to be done by the kernel itself
+  -- but that is incompatible with moving it to a separate task
+  env := decl.getNames.foldl registerNamePrefixes env
+  if let .inductDecl _ _ types _ := decl then
+    env := types.foldl (registerNamePrefixes · <| ·.name ++ `rec) env
 
-    -- register namespaces for newly added constants; this used to be done by the kernel itself
-    -- but that is incompatible with moving it to a separate task
-    env := decl.getNames.foldl registerNamePrefixes env
-    if let .inductDecl _ _ types _ := decl then
-      env := types.foldl (registerNamePrefixes · <| ·.name ++ `rec) env
+  if !Elab.async.get (← getOptions) then
     setEnv env
+    return (← doAdd)
+
+  -- convert `Declaration` to `ConstantInfo` to use as a preliminary value in the environment until
+  -- kernel checking has finished; not all cases are supported yet
+  let (name, info, kind) ← match decl with
+    | .thmDecl thm => pure (thm.name, .thmInfo thm, .thm)
+    | .defnDecl defn => pure (defn.name, .defnInfo defn, .defn)
+    | .mutualDefnDecl [defn] => pure (defn.name, .defnInfo defn, .defn)
+    | _ => return (← doAdd)
+
+  -- no environment extension changes to report after kernel checking; ensures we do not
+  -- accidentally wait for this snapshot when querying extension states
+  let async ← env.addConstAsync (reportExts := false) name kind
+  -- report preliminary constant info immediately
+  async.commitConst async.asyncEnv (some info)
+  setEnv async.mainEnv
+  let checkAct ← Core.wrapAsyncAsSnapshot fun _ => do
+    try
+      setEnv async.asyncEnv
+      doAdd
+      async.commitCheckEnv (← getEnv)
+    finally
+      async.commitFailure
+  let t ← BaseIO.mapTask (fun _ => checkAct) env.checked
+  let endRange? := (← getRef).getTailPos?.map fun pos => ⟨pos, pos⟩
+  Core.logSnapshotTask { range? := endRange?, task := t }
+where doAdd := do
+  profileitM Exception "type checking" (← getOptions) do
+    withTraceNode `Kernel (fun _ => return m!"typechecking declarations {decl.getNames}") do
+      if !(← MonadLog.hasErrors) && decl.hasSorry then
+        logWarning m!"declaration uses 'sorry'"
+      let env ← (← getEnv).addDeclAux (← getOptions) decl (← read).cancelTk?
+        |> ofExceptKernelException
+      setEnv env
 
 def addAndCompile (decl : Declaration) : CoreM Unit := do
   addDecl decl

src/Lean/CoreM.lean

@@ -423,7 +423,11 @@ 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 fun st => { st with messages := st.messages.markAllReported, traceState := { tid } }
+      modify fun st => { st with
+        messages := st.messages.markAllReported
+        traceState := { tid }
+        snapshotTasks := #[]
+      }
       try
         withTraceNode `Elab.async (fun _ => return desc) do
           act ()
@@ -518,6 +522,10 @@ opaque compileDeclsNew (declNames : List Name) : CoreM Unit
 opaque compileDeclsOld (env : Environment) (opt : @& Options) (decls : @& List Name) : Except Kernel.Exception Environment
 
 def compileDecl (decl : Declaration) : CoreM Unit := do
+  -- don't compile if kernel errored; should be converted into a task dependency when compilation
+  -- is made async as well
+  if !decl.getNames.all (← getEnv).constants.contains then
+    return
   let opts ← getOptions
   let decls := Compiler.getDeclNamesForCodeGen decl
   if compiler.enableNew.get opts then
@@ -533,6 +541,10 @@ def compileDecl (decl : Declaration) : CoreM Unit := do
     throwKernelException ex
 
 def compileDecls (decls : List Name) : CoreM Unit := do
+  -- don't compile if kernel errored; should be converted into a task dependency when compilation
+  -- is made async as well
+  if !decls.all (← getEnv).constants.contains then
+    return
   let opts ← getOptions
   if compiler.enableNew.get opts then
     compileDeclsNew decls

src/Lean/Elab/Command.lean

@@ -313,7 +313,11 @@ 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 fun st => { st with messages := st.messages.markAllReported, traceState := { tid } }
+      modify fun st => { st with
+        messages := st.messages.markAllReported
+        traceState := { tid }
+        snapshotTasks := #[]
+      }
       try
         withTraceNode `Elab.async (fun _ => return desc) do
           act ()

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

@@ -308,7 +308,7 @@ def bvDecide (g : MVarId) (ctx : TacticContext) : MetaM Result := do
       throwError (← addMessageContextFull errorMessage)
 
 @[builtin_tactic Lean.Parser.Tactic.bvDecide]
-def evalBvTrace : Tactic := fun
+def evalBvDecide : Tactic := fun
   | `(tactic| bv_decide $cfg:optConfig) => do
     let cfg ← elabBVDecideConfig cfg
     IO.FS.withTempFile fun _ lratFile => do
@@ -319,4 +319,3 @@ def evalBvTrace : Tactic := fun
 
 end Frontend
 end Lean.Elab.Tactic.BVDecide
-

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

@@ -197,8 +197,10 @@ def LratCert.toReflectionProof [ToExpr α] (cert : LratCert) (cfg : TacticContex
       (← mkEqRefl (toExpr true))
   try
     let auxLemma ←
-      withTraceNode `sat (fun _ => return "Verifying LRAT certificate") do
-        mkAuxLemma [] auxType auxProof
+      -- disable async TC so we can catch its exceptions
+      withOptions (Elab.async.set · false) do
+        withTraceNode `sat (fun _ => return "Verifying LRAT certificate") do
+          mkAuxLemma [] auxType auxProof
     return mkApp3 (mkConst unsat_of_verifier_eq_true) reflectedExpr certExpr (mkConst auxLemma)
   catch e =>
     throwError m!"Failed to check the LRAT certificate in the kernel:\n{e.toMessageData}"

src/Lean/Elab/Tactic/ElabTerm.lean

@@ -407,8 +407,10 @@ private unsafe def elabNativeDecideCoreUnsafe (tacticName : Name) (expectedType
   let pf := mkApp3 (mkConst ``of_decide_eq_true) expectedType s <|
     mkApp3 (mkConst ``Lean.ofReduceBool) (mkConst auxDeclName levelParams) (toExpr true) rflPrf
   try
-    let lemmaName ← mkAuxLemma levels expectedType pf
-    return .const lemmaName levelParams
+    -- disable async TC so we can catch its exceptions
+    withOptions (Elab.async.set · false) do
+      let lemmaName ← mkAuxLemma levels expectedType pf
+      return .const lemmaName levelParams
   catch ex =>
     -- Diagnose error
     throwError MessageData.ofLazyM (es := #[expectedType]) do
@@ -473,7 +475,8 @@ where
     -- Level variables occurring in `expectedType`, in ambient order
     let lemmaLevels := (← Term.getLevelNames).reverse.filter levelsInType.contains
     try
-      let lemmaName ← mkAuxLemma lemmaLevels expectedType pf
+      let lemmaName ← withOptions (Elab.async.set · false) do
+        mkAuxLemma lemmaLevels expectedType pf
       return mkConst lemmaName (lemmaLevels.map .param)
     catch _ =>
       diagnose expectedType s none

src/Lean/Environment.lean

@@ -451,7 +451,9 @@ def ofKernelEnv (env : Kernel.Environment) : Environment :=
 
 @[export lean_elab_environment_to_kernel_env]
 def toKernelEnv (env : Environment) : Kernel.Environment :=
-  env.checked.get
+  -- TODO: should just be the following when we store extension data in `checked`
+  --env.checked.get
+  { env.checked.get with extensions := env.checkedWithoutAsync.extensions }
 
 /-- Consistently updates synchronous and asynchronous parts of the environment without blocking. -/
 private def modifyCheckedAsync (env : Environment) (f : Kernel.Environment → Kernel.Environment) : Environment :=
@@ -498,7 +500,7 @@ def const2ModIdx (env : Environment) : Std.HashMap Name ModuleIdx :=
 -- only needed for the lakefile.lean cache
 @[export lake_environment_add]
 private def lakeAdd (env : Environment) (cinfo : ConstantInfo) : Environment :=
-  { env with checked := .pure <| env.checked.get.add cinfo }
+  env.setCheckedSync <| env.checked.get.add cinfo
 
 /--
 Save an extra constant name that is used to populate `const2ModIdx` when we import
@@ -867,22 +869,22 @@ opaque EnvExtensionInterfaceImp : EnvExtensionInterface
 def EnvExtension (σ : Type) : Type := EnvExtensionInterfaceImp.ext σ
 
 private def ensureExtensionsArraySize (env : Environment) : IO Environment := do
-  let exts ← EnvExtensionInterfaceImp.ensureExtensionsSize env.checked.get.extensions
+  let exts ← EnvExtensionInterfaceImp.ensureExtensionsSize env.checkedWithoutAsync.extensions
   return env.modifyCheckedAsync ({ · with extensions := exts })
 
 namespace EnvExtension
 instance {σ} [s : Inhabited σ] : Inhabited (EnvExtension σ) := EnvExtensionInterfaceImp.inhabitedExt s
 
+-- TODO: store extension state in `checked`
+
 def setState {σ : Type} (ext : EnvExtension σ) (env : Environment) (s : σ) : Environment :=
-  let checked := env.checked.get
-  env.setCheckedSync { checked with extensions := EnvExtensionInterfaceImp.setState ext checked.extensions s }
+  { env with checkedWithoutAsync.extensions := EnvExtensionInterfaceImp.setState ext env.checkedWithoutAsync.extensions s }
 
 def modifyState {σ : Type} (ext : EnvExtension σ) (env : Environment) (f : σ → σ) : Environment :=
-  let checked := env.checked.get
-  env.setCheckedSync { checked with extensions := EnvExtensionInterfaceImp.modifyState ext checked.extensions f }
+  { env with checkedWithoutAsync.extensions := EnvExtensionInterfaceImp.modifyState ext env.checkedWithoutAsync.extensions f }
 
 def getState {σ : Type} [Inhabited σ] (ext : EnvExtension σ) (env : Environment) : σ :=
-  EnvExtensionInterfaceImp.getState ext env.checked.get.extensions
+  EnvExtensionInterfaceImp.getState ext env.checkedWithoutAsync.extensions
 
 end EnvExtension
 
@@ -1469,7 +1471,7 @@ def getNamespaceSet (env : Environment) : NameSSet :=
 
 @[export lean_elab_environment_update_base_after_kernel_add]
 private def updateBaseAfterKernelAdd (env : Environment) (kernel : Kernel.Environment) : Environment :=
-  env.setCheckedSync kernel
+  env.setCheckedSync { kernel with extensions := env.checkedWithoutAsync.extensions }
 
 @[export lean_display_stats]
 def displayStats (env : Environment) : IO Unit := do

src/Lean/Meta/IndPredBelow.lean

@@ -594,7 +594,9 @@ def mkBelow (declName : Name) : MetaM Unit := do
       for i in [:ctx.typeInfos.size] do
         try
           let decl ← IndPredBelow.mkBrecOnDecl ctx i
-          addDecl decl
+          -- disable async TC so we can catch its exceptions
+          withOptions (Elab.async.set · false) do
+            addDecl decl
         catch e => trace[Meta.IndPredBelow] "failed to prove brecOn for {ctx.belowNames[i]!}\n{e.toMessageData}"
     else trace[Meta.IndPredBelow] "Nested or not recursive"
   else trace[Meta.IndPredBelow] "Not inductive predicate"

src/Lean/Meta/Tactic/Grind/Internalize.lean

@@ -134,6 +134,7 @@ private partial def internalizeMatchCond (matchCond : Expr) (generation : Nat) :
   propagateUp matchCond
   internalize e' generation
   trace[grind.debug.matchCond.lambda] "(idx := {(← getENode e'.getAppFn).idx}) {e'.getAppFn}"
+  trace[grind.debug.matchCond.lambda] "auxiliary application{indentExpr e'}"
   pushEq matchCond e' (← mkEqRefl matchCond)
 
 partial def activateTheorem (thm : EMatchTheorem) (generation : Nat) : GoalM Unit := do