Incr tactic rc1

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/Init/Data/String/Basic.lean

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

@@ -228,6 +228,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).
 
@@ -744,6 +751,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 := {
@@ -89,6 +90,8 @@ 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
   deriving Nonempty
 
 /-- CoreM is a monad for manipulating the Lean environment.
@@ -198,16 +201,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 `old?` 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 `old?` 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 `old?` and
+call `save` as late as possible in `cont`. In a further run, if reuse is possible, `old?` 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 `old?` are not accounted
+for.
 -/
-def restoreFull (b : State) : CoreM Unit :=
-  set b
+@[specialize] def withRestoreOrSaveFull (old? : Option (α × SavedState))
+    (cont : (save : CoreM SavedState) → CoreM α) : CoreM α := do
+  if let some (oldVal, oldState) := old? then
+    set oldState.toState
+    IO.addHeartbeats oldState.passedHearbeats.toUInt64
+    return oldVal
+
+  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 })
@@ -238,10 +270,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
 
 def throwMaxHeartbeat (moduleName : Name) (optionName : Name) (max : Nat) : CoreM Unit := do
   let msg := s!"(deterministic) timeout at `{moduleName}`, maximum number of heartbeats ({max/1000}) has been reached\nuse `set_option {optionName} <num>` to set the limit\nuse `set_option {diagnostics.name} true` to get diagnostic information"
@@ -278,11 +318,13 @@ 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.msgs := {}
+    messages.hadErrors := s.messages.hasErrors })
 
 instance : MonadLog CoreM where
   getRef      := getRef
@@ -409,19 +451,25 @@ 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 && !(← read).catchRuntimeEx then
+    if ex.isInterrupt || (ex.isRuntime && !(← read).catchRuntimeEx) then
       throw ex
     else
       h ex

src/Lean/Elab/Command.lean

@@ -47,15 +47,18 @@ structure Context where
   ref            : Syntax := Syntax.missing
   tacticCache?   : Option (IO.Ref Tactic.Cache)
   /--
-  Snapshot for incremental reuse and reporting of command elaboration. Currently unused in Lean
-  itself.
+  Snapshot for incremental reuse and reporting of command elaboration. Currently only used for
+  (mutual) defs and contained tactics, in which case the `DynamicSnapshot` is a
+  `HeadersParsedSnapshot`.
 
   Definitely resolved in `Language.Lean.process.doElab`.
 
   Invariant: if the bundle's `old?` is set, the context and state at the beginning of current and
   old elaboration are identical.
   -/
   snap?          : Option (Language.SnapshotBundle Language.DynamicSnapshot)
+  /-- Cancellation token forwarded to `Core.cancelTk?`. -/
+  cancelTk?      : Option IO.CancelToken
 
 abbrev CommandElabCoreM (ε) := ReaderT Context $ StateRefT State $ EIO ε
 abbrev CommandElabM := CommandElabCoreM Exception
@@ -73,6 +76,21 @@ Remark: see comment at TermElabM
 @[always_inline]
 instance : Monad CommandElabM := let i := inferInstanceAs (Monad CommandElabM); { pure := i.pure, bind := i.bind }
 
+/-- Like `Core.tryCatch` but do catch runtime exceptions. -/
+@[inline] protected def tryCatch (x : CommandElabM α) (h : Exception → CommandElabM α) :
+    CommandElabM α := do
+  try
+    x
+  catch ex =>
+    if ex.isInterrupt then
+      throw ex
+    else
+      h ex
+
+instance : MonadExceptOf Exception CommandElabM where
+  throw    := throw
+  tryCatch := Command.tryCatch
+
 def mkState (env : Environment) (messages : MessageLog := {}) (opts : Options := {}) : State := {
   env         := env
   messages    := messages
@@ -140,7 +158,8 @@ private def mkCoreContext (ctx : Context) (s : State) (heartbeats : Nat) : Core.
     openDecls      := scope.openDecls
     initHeartbeats := heartbeats
     currMacroScope := ctx.currMacroScope
-    diag           := getDiag scope.opts }
+    diag           := getDiag scope.opts
+    cancelTk?      := ctx.cancelTk? }
 
 private def addTraceAsMessagesCore (ctx : Context) (log : MessageLog) (traceState : TraceState) : MessageLog := Id.run do
   if traceState.traces.isEmpty then return log
@@ -468,7 +487,12 @@ def runTermElabM (elabFn : Array Expr → TermElabM α) : CommandElabM α := do
           Term.addAutoBoundImplicits' xs someType fun xs _ =>
             Term.withoutAutoBoundImplicit <| elabFn xs
 
-@[inline] def catchExceptions (x : CommandElabM Unit) : CommandElabCoreM Empty Unit := fun ctx ref =>
+/--
+Catches and logs exceptions occurring in `x`. Unlike `try catch` in `CommandElabM`, this function
+catches interrupt exceptions as well and thus is intended for use at the top level of elaboration.
+Interrupt and abort exceptions are caught but not logged.
+-/
+@[inline] def withLoggingExceptions (x : CommandElabM Unit) : CommandElabCoreM Empty Unit := fun ctx ref =>
   EIO.catchExceptions (withLogging x ctx ref) (fun _ => pure ())
 
 private def liftAttrM {α} (x : AttrM α) : CommandElabM α := do
@@ -534,6 +558,7 @@ def liftCommandElabM (cmd : CommandElabM α) : CoreM α := do
       ref := ← getRef
       tacticCache? := none
       snap? := none
+      cancelTk? := (← read).cancelTk?
     } |>.run {
       env := ← getEnv
       maxRecDepth := ← getMaxRecDepth

src/Lean/Elab/DefView.lean

@@ -28,6 +28,81 @@ def DefKind.isExample : DefKind → Bool
   | .example => true
   | _        => false
 
+/-- Header elaboration data of a `DefView`. -/
+structure DefViewElabHeaderData where
+  /--
+    Short name. Recall that all declarations in Lean 4 are potentially recursive. We use `shortDeclName` to refer
+    to them at `valueStx`, and other declarations in the same mutual block. -/
+  shortDeclName : Name
+  /-- Full name for this declaration. This is the name that will be added to the `Environment`. -/
+  declName      : Name
+  /-- Universe level parameter names explicitly provided by the user. -/
+  levelNames    : List Name
+  /-- Syntax objects for the binders occurring before `:`, we use them to populate the `InfoTree` when elaborating `valueStx`. -/
+  binderIds     : Array Syntax
+  /-- Number of parameters before `:`, it also includes auto-implicit parameters automatically added by Lean. -/
+  numParams     : Nat
+  /-- Type including parameters. -/
+  type          : Expr
+deriving Inhabited
+
+section Snapshots
+open Language
+
+/-- Snapshot after processing of a definition body.  -/
+structure BodyProcessedSnapshot extends Language.Snapshot where
+  /-- State after elaboration. -/
+  state : Term.SavedState
+  /-- Elaboration result. -/
+  value : Expr
+deriving Nonempty
+instance : Language.ToSnapshotTree BodyProcessedSnapshot where
+  toSnapshotTree s := ⟨s.toSnapshot, #[]⟩
+
+/-- Snapshot after elaboration of a definition header. -/
+structure HeaderProcessedSnapshot extends Language.Snapshot where
+  /-- Elaboration results. -/
+  view : DefViewElabHeaderData
+  /-- Resulting elaboration state, including any environment additions. -/
+  state : Term.SavedState
+  /-- Syntax of top-level tactic block if any, for checking reuse of `tacSnap?`. -/
+  tacStx? : Option Syntax
+  /-- Incremental execution of main tactic block, if any. -/
+  tacSnap? : Option (SnapshotTask Tactic.TacticParsedSnapshot)
+  /-- Syntax of definition body, for checking reuse of `bodySnap`. -/
+  bodyStx : Syntax
+  /-- Result of body elaboration. -/
+  bodySnap : SnapshotTask (Option BodyProcessedSnapshot)
+deriving Nonempty
+instance : Language.ToSnapshotTree HeaderProcessedSnapshot where
+  toSnapshotTree s := ⟨s.toSnapshot,
+    (match s.tacSnap? with
+      | some tac => #[tac.map (sync := true) toSnapshotTree]
+      | none     => #[]) ++
+    #[s.bodySnap.map (sync := true) toSnapshotTree]⟩
+
+/-- State before elaboration of a mutual definition. -/
+structure DefParsed where
+  /--
+  Input substring uniquely identifying header elaboration result given the same `Environment`.
+  If missing, results should never be reused.
+  -/
+  headerSubstr? : Option Substring
+  /-- Elaboration result, unless fatal exception occurred. -/
+  headerProcessedSnap : SnapshotTask (Option HeaderProcessedSnapshot)
+deriving Nonempty
+
+/-- Snapshot after syntax tree has been split into separate mutual def headers. -/
+structure DefsParsedSnapshot extends Language.Snapshot where
+  /-- Definitions of this mutual block. -/
+  defs : Array DefParsed
+deriving Nonempty, TypeName
+instance : Language.ToSnapshotTree DefsParsedSnapshot where
+  toSnapshotTree s := ⟨s.toSnapshot,
+    s.defs.map (·.headerProcessedSnap.map (sync := true) toSnapshotTree)⟩
+
+end Snapshots
+
 structure DefView where
   kind          : DefKind
   ref           : Syntax
@@ -36,6 +111,13 @@ structure DefView where
   binders       : Syntax
   type?         : Option Syntax
   value         : Syntax
+  /--
+  Snapshot for incremental processing of this definition.
+
+  Invariant: If the bundle's `old?` is set, then elaboration of the header is guaranteed to result
+  in the same elaboration result and state, i.e. reuse is possible.
+  -/
+  headerSnap?   : Option (Language.SnapshotBundle (Option HeaderProcessedSnapshot)) := none
   deriving?     : Option (Array Syntax) := none
   deriving Inhabited