feat: incremental elaboration of definition headers, bodies, and tact…

…ics (leanprover#3940)

Extends Lean's incremental reporting and reuse between commands into
various steps inside declarations:
* headers and bodies of each (mutual) definition/theorem
* `theorem ... := by` for each contained tactic step, including
recursively inside supported combinators currently consisting of
  * `·` (cdot), `case`, `next`
  * `induction`, `cases`
  * macros such as `next` unfolding to the above

![Recording 2024-05-10 at 11 07
32](https://github.com/leanprover/lean4/assets/109126/c9d67b6f-c131-4bc3-a0de-7d63eaf1bfc9)

*Incremental reuse* means not recomputing any such steps if they are not
affected by a document change. *Incremental reporting* includes the
parts seen in the recording above: the progress bar and messages. Other
language server features such as hover etc. are *not yet* supported
incrementally, i.e. they are shown only when the declaration has been
fully processed as before.

---------

Co-authored-by: Scott Morrison <[email protected]>

RELEASES.md

@@ -8,6 +8,7 @@ This file contains work-in-progress notes for the upcoming release, as well as p
 Please check the [releases](https://github.com/leanprover/lean4/releases) page for the current status
 of each version.
 
+v4.8.0
 v4.9.0 (development in progress)
 ---------
 

doc/examples/test_single.sh

@@ -1,4 +1,4 @@
 #!/usr/bin/env bash
 source ../../tests/common.sh
 
-exec_check lean -j 0 -Dlinter.all=false "$f"
+exec_check lean -Dlinter.all=false "$f"

nix/bootstrap.nix

@@ -170,7 +170,7 @@ rec {
           ln -sf ${lean-all}/* .
         '';
         buildPhase = ''
-          ctest --output-junit test-results.xml --output-on-failure -E 'leancomptest_(doc_example|foreign)' -j$NIX_BUILD_CORES
+          ctest --output-junit test-results.xml --output-on-failure -E 'leancomptest_(doc_example|foreign)|leanlaketest_init' -j$NIX_BUILD_CORES
         '';
         installPhase = ''
           mkdir $out

src/CMakeLists.txt

@@ -11,7 +11,7 @@ project(LEAN CXX C)
 set(LEAN_VERSION_MAJOR 4)
 set(LEAN_VERSION_MINOR 9)
 set(LEAN_VERSION_PATCH 0)
-set(LEAN_VERSION_IS_RELEASE 0)  # This number is 1 in the release revision, and 0 otherwise.
+set(LEAN_VERSION_IS_RELEASE 1)  # This number is 1 in the release revision, and 0 otherwise.
 set(LEAN_SPECIAL_VERSION_DESC "" CACHE STRING "Additional version description like 'nightly-2018-03-11'")
 set(LEAN_VERSION_STRING "${LEAN_VERSION_MAJOR}.${LEAN_VERSION_MINOR}.${LEAN_VERSION_PATCH}")
 if (LEAN_SPECIAL_VERSION_DESC)

src/Init/Data/String/Basic.lean

@@ -951,6 +951,10 @@ def beq (ss1 ss2 : Substring) : Bool :=
 
 instance hasBeq : BEq Substring := ⟨beq⟩
 
+/-- Checks whether two substrings have the same position and content. -/
+def sameAs (ss1 ss2 : Substring) : Bool :=
+  ss1.startPos == ss2.startPos && ss1 == ss2
+
 end Substring
 
 namespace String

src/Init/Prelude.lean

@@ -3644,6 +3644,17 @@ def getPos? (info : SourceInfo) (canonicalOnly := false) : Option String.Pos :=
   | synthetic (pos := pos) .., false => some pos
   | _,                         _     => none
 
+/--
+Gets the end position information from a `SourceInfo`, if available.
+If `originalOnly` is true, then `.synthetic` syntax will also return `none`.
+-/
+def getTailPos? (info : SourceInfo) (canonicalOnly := false) : Option String.Pos :=
+  match info, canonicalOnly with
+  | original (endPos := endPos) ..,  _
+  | synthetic (endPos := endPos) (canonical := true) .., _
+  | synthetic (endPos := endPos) .., false => some endPos
+  | _,                               _     => none
+
 end SourceInfo
 
 /--

src/Init/System/IO.lean

@@ -264,6 +264,13 @@ local macro "nonempty_list" : tactic =>
 /-- Helper method for implementing "deterministic" timeouts. It is the number of "small" memory allocations performed by the current execution thread. -/
 @[extern "lean_io_get_num_heartbeats"] opaque getNumHeartbeats : BaseIO Nat
 
+/--
+Adjusts the heartbeat counter of the current thread by the given amount. This can be useful to give
+allocation-avoiding code additional "weight" and is also used to adjust the counter after resuming
+from a snapshot.
+-/
+@[extern "lean_io_add_heartbeats"] opaque addHeartbeats (count : UInt64) : BaseIO Unit
+
 /--
 The mode of a file handle (i.e., a set of `open` flags and an `fdopen` mode).
 
@@ -786,6 +793,32 @@ instance : MonadLift (ST IO.RealWorld) BaseIO := ⟨id⟩
 def mkRef (a : α) : BaseIO (IO.Ref α) :=
   ST.mkRef a
 
+/--
+Mutable cell that can be passed around for purposes of cooperative task cancellation: request
+cancellation with `CancelToken.set` and check for it with `CancelToken.isSet`.
+
+This is a more flexible alternative to `Task.cancel` as the token can be shared between multiple
+tasks.
+-/
+structure CancelToken where
+  private ref : IO.Ref Bool
+
+namespace CancelToken
+
+/-- Creates a new cancellation token. -/
+def new : BaseIO CancelToken :=
+  CancelToken.mk <$> IO.mkRef false
+
+/-- Activates a cancellation token. Idempotent. -/
+def set (tk : CancelToken) : BaseIO Unit :=
+  tk.ref.set true
+
+/-- Checks whether the cancellation token has been activated. -/
+def isSet (tk : CancelToken) : BaseIO Bool :=
+  tk.ref.get
+
+end CancelToken
+
 namespace FS
 namespace Stream
 

src/Lean/CoreM.lean

@@ -11,6 +11,7 @@ import Lean.Eval
 import Lean.ResolveName
 import Lean.Elab.InfoTree.Types
 import Lean.MonadEnv
+import Lean.Elab.Exception
 
 namespace Lean
 register_builtin_option diagnostics : Bool := {
@@ -85,6 +86,13 @@ structure Context where
   Use the `set_option diag true` to set it to true.
   -/
   diag           : Bool := false
+  /-- If set, used to cancel elaboration from outside when results are not needed anymore. -/
+  cancelTk?      : Option IO.CancelToken := none
+  /--
+  If set (when `showPartialSyntaxErrors` is not set and parsing failed), suppresses most elaboration
+  errors; see also `logMessage` below.
+  -/
+  suppressElabErrors : Bool := false
   deriving Nonempty
 
 /-- CoreM is a monad for manipulating the Lean environment.
@@ -201,16 +209,45 @@ instance : MonadTrace CoreM where
   getTraceState := return (← get).traceState
   modifyTraceState f := modify fun s => { s with traceState := f s.traceState }
 
-/-- Restore backtrackable parts of the state. -/
-def restore (b : State) : CoreM Unit :=
-  modify fun s => { s with env := b.env, messages := b.messages, infoState := b.infoState }
+structure SavedState extends State where
+  /-- Number of heartbeats passed inside `withRestoreOrSaveFull`, not used otherwise. -/
+  passedHearbeats : Nat
+deriving Nonempty
+
+def saveState : CoreM SavedState := do
+  let s ← get
+  return { toState := s, passedHearbeats := 0 }
 
 /--
-Restores full state including sources for unique identifiers. Only intended for incremental reuse
-between elaboration runs, not for backtracking within a single run.
+Incremental reuse primitive: if `reusableResult?` is `none`, runs `cont` with an action `save` that
+on execution returns the saved monadic state at this point including the heartbeats used by `cont`
+so far. If `reusableResult?` on the other hand is `some (a, state)`, restores full `state` including
+heartbeats used and returns `a`.
+
+The intention is for steps that support incremental reuse to initially pass `none` as
+`reusableResult?` and call `save` as late as possible in `cont`. In a further run, if reuse is
+possible, `reusableResult?` should be set to the previous state and result, ensuring that the state
+after running `withRestoreOrSaveFull` is identical in both runs. Note however that necessarily this
+is only an approximation in the case of heartbeats as heartbeats used by `withRestoreOrSaveFull`, by
+the remainder of `cont` after calling `save`, as well as by reuse-handling code such as the one
+supplying `reusableResult?` are not accounted for.
 -/
-def restoreFull (b : State) : CoreM Unit :=
-  set b
+@[specialize] def withRestoreOrSaveFull (reusableResult? : Option (α × SavedState))
+    (cont : (save : CoreM SavedState) → CoreM α) : CoreM α := do
+  if let some (val, state) := reusableResult? then
+    set state.toState
+    IO.addHeartbeats state.passedHearbeats.toUInt64
+    return val
+
+  let startHeartbeats ← IO.getNumHeartbeats
+  cont (do
+    let s ← get
+    let stopHeartbeats ← IO.getNumHeartbeats
+    return { toState := s, passedHearbeats := stopHeartbeats - startHeartbeats })
+
+/-- Restore backtrackable parts of the state. -/
+def SavedState.restore (b : SavedState) : CoreM Unit :=
+  modify fun s => { s with env := b.env, messages := b.messages, infoState := b.infoState }
 
 private def mkFreshNameImp (n : Name) : CoreM Name := do
   let fresh ← modifyGet fun s => (s.nextMacroScope, { s with nextMacroScope := s.nextMacroScope + 1 })
@@ -241,10 +278,18 @@ instance [MetaEval α] : MetaEval (CoreM α) where
 protected def withIncRecDepth [Monad m] [MonadControlT CoreM m] (x : m α) : m α :=
   controlAt CoreM fun runInBase => withIncRecDepth (runInBase x)
 
+builtin_initialize interruptExceptionId : InternalExceptionId ← registerInternalExceptionId `interrupt
+
+/--
+Throws an internal interrupt exception if cancellation has been requested. The exception is not
+caught by `try catch` but is intended to be caught by `Command.withLoggingExceptions` at the top
+level of elaboration. In particular, we want to skip producing further incremental snapshots after
+the exception has been thrown.
+ -/
 @[inline] def checkInterrupted : CoreM Unit := do
-  if (← IO.checkCanceled) then
-    -- should never be visible to users!
-    throw <| Exception.error .missing "elaboration interrupted"
+  if let some tk := (← read).cancelTk? then
+    if (← tk.isSet) then
+      throw <| .internal interruptExceptionId
 
 register_builtin_option debug.moduleNameAtTimeout : Bool := {
   defValue := true
@@ -289,18 +334,26 @@ def getMessageLog : CoreM MessageLog :=
   return (← get).messages
 
 /--
-Returns the current log and then resets its messages but does NOT reset `MessageLog.hadErrors`. Used
+Returns the current log and then resets its messages while adjusting `MessageLog.hadErrors`. Used
 for incremental reporting during elaboration of a single command.
 -/
 def getAndEmptyMessageLog : CoreM MessageLog :=
-  modifyGet fun log => ({ log with msgs := {} }, log)
+  modifyGet fun s => (s.messages, { s with
+    messages.unreported := {}
+    messages.hadErrors  := s.messages.hasErrors })
 
 instance : MonadLog CoreM where
   getRef      := getRef
   getFileMap  := return (← read).fileMap
   getFileName := return (← read).fileName
   hasErrors   := return (← get).messages.hasErrors
   logMessage msg := do
+    if (← read).suppressElabErrors then
+      -- discard elaboration errors, except for a few important and unlikely misleading ones, on
+      -- parse error
+      unless msg.data.hasTag (· matches `Elab.synthPlaceholder | `Tactic.unsolvedGoals) do
+        return
+
     let ctx ← read
     let msg := { msg with data := MessageData.withNamingContext { currNamespace := ctx.currNamespace, openDecls := ctx.openDecls } msg.data };
     modify fun s => { s with messages := s.messages.add msg }
@@ -408,19 +461,26 @@ def ImportM.runCoreM (x : CoreM α) : ImportM α := do
   let (a, _) ← (withOptions (fun _ => ctx.opts) x).toIO { fileName := "<ImportM>", fileMap := default } { env := ctx.env }
   return a
 
-/-- Return `true` if the exception was generated by one our resource limits. -/
+/-- Return `true` if the exception was generated by one of our resource limits. -/
 def Exception.isRuntime (ex : Exception) : Bool :=
   ex.isMaxHeartbeat || ex.isMaxRecDepth
 
+/-- Returns `true` if the exception is an interrupt generated by `checkInterrupted`. -/
+def Exception.isInterrupt : Exception → Bool
+  | Exception.internal id _ => id == Core.interruptExceptionId
+  | _ => false
+
 /--
-Custom `try-catch` for all monads based on `CoreM`. We don't want to catch "runtime exceptions"
-in these monads, but on `CommandElabM`. See issues #2775 and #2744 as well as `MonadAlwayExcept`.
+Custom `try-catch` for all monads based on `CoreM`. We usually don't want to catch "runtime
+exceptions" these monads, but on `CommandElabM`. See issues #2775 and #2744 as well as
+`MonadAlwaysExcept`. Also, we never want to catch interrupt exceptions inside the elaborator.
 -/
 @[inline] protected def Core.tryCatch (x : CoreM α) (h : Exception → CoreM α) : CoreM α := do
   try
     x
   catch ex =>
-    if ex.isRuntime then
+    if ex.isInterrupt || ex.isRuntime then
+
       throw ex -- We should use `tryCatchRuntimeEx` for catching runtime exceptions
     else
       h ex