d42d6c5246
This PR fixes an `Elab.async` regression where elaboration tasks are cancelled on document edit even though their result may be reused in the new document version, reporting an incomplete result. While this PR fixes the functional regression, it does so as an over-approximation by never cancelling such tasks. A follow-up PR will implement the correct behavior of only cancelling the tasks that are not reused.
53 lines
1.3 KiB
Text
53 lines
1.3 KiB
Text
import Lean.Server.Test.Cancel
|
|
open Lean.Server.Test.Cancel
|
|
|
|
/-!
|
|
Cancellation tests. Use `wait_for_cancel_once` to block the server and send a message to the client
|
|
who should wait for it with `waitFor` and then issue a new document version, which will unblock
|
|
`wait_for_cancel_once`
|
|
-/
|
|
|
|
/-! Changes in a declaration should invalidate elaboration of later declarations. -/
|
|
|
|
example : True := by
|
|
trivial
|
|
--^ waitFor: blocked
|
|
--^ insert: "; skip"
|
|
--^ collectDiagnostics
|
|
-- (should never print "blocked")
|
|
|
|
theorem t : True := by
|
|
wait_for_cancel_once
|
|
dbg_trace "rerun!"
|
|
trivial
|
|
|
|
-- RESET
|
|
import Lean.Server.Test.Cancel
|
|
open Lean.Server.Test.Cancel
|
|
|
|
/-! Changes in a declaration should not invalidate async tasks of previous declarations. -/
|
|
|
|
theorem t1 : True := by
|
|
wait_for_unblock_async
|
|
trivial
|
|
|
|
example : True := by
|
|
trivial
|
|
--^ waitFor: blocked
|
|
--^ insert: "; unblock"
|
|
--^ collectDiagnostics
|
|
-- (should print "blocked" exactly once)
|
|
|
|
-- RESET
|
|
import Lean.Server.Test.Cancel
|
|
open Lean.Server.Test.Cancel
|
|
|
|
/-! Changes in a tactic should not invalidate async tasks of previous tactics. -/
|
|
|
|
theorem t1 : True := by
|
|
wait_for_unblock_async
|
|
trivial
|
|
--^ waitFor: blocked
|
|
--^ insert: "; unblock"
|
|
--^ collectDiagnostics
|
|
-- (should print "blocked" exactly once)
|