f97a7d4234
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  *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 <scott.morrison@gmail.com>
45 lines
1,020 B
Text
45 lines
1,020 B
Text
/-! Basic incremental reuse in top-level tactic block -/
|
||
|
||
-- set_option trace.Elab.reuse true
|
||
|
||
def basic : True := by
|
||
dbg_trace "b 0"
|
||
apply id
|
||
dbg_trace "b 1"
|
||
apply id
|
||
dbg_trace "b 2"
|
||
--^ sync
|
||
--^ insert: ".5"
|
||
|
||
-- RESET
|
||
def trailingWhitespace : True := by
|
||
dbg_trace "t 0"
|
||
dbg_trace "t 1"
|
||
dbg_trace "t 2"
|
||
--^ sync
|
||
--^ insert: "\n "
|
||
|
||
|
||
-- RESET
|
||
-- this used to restore the wrong elab state because of input context mis-tracking
|
||
def haveBug : True := by
|
||
have (a : Nat) : Nat → True := by
|
||
intro n m
|
||
--^ sync
|
||
--^ delete: "intro n m"
|
||
--^ sync
|
||
--^ insert: "intro n m"
|
||
--^ collectDiagnostics
|
||
exact m
|
||
|
||
/-! incremental reporting should obey `showPartialSyntaxErrors` -/
|
||
-- RESET
|
||
def partialSyntax : True := by apply (
|
||
--^ collectDiagnostics
|
||
|
||
/-! A tactic block not supported by incrementality should not accidentally swallow messages. -/
|
||
-- RESET
|
||
def otherMessage : Nat × Nat where
|
||
fst := no
|
||
snd := by skip
|
||
--^ collectDiagnostics
|