From bcc84ce49bc824005e649351a27dfb5bf932f4aa Mon Sep 17 00:00:00 2001 From: Sebastian Ullrich Date: Wed, 30 Dec 2020 22:11:40 +0100 Subject: [PATCH] fix: cancellation Interestingly this led to a deadlock in `edits.lean` using `-j2` (hardcoded because of #246), should maybe investigate this... --- src/Lean/Server/FileWorker.lean | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/Lean/Server/FileWorker.lean b/src/Lean/Server/FileWorker.lean index 50c316f991..167b38e423 100644 --- a/src/Lean/Server/FileWorker.lean +++ b/src/Lean/Server/FileWorker.lean @@ -163,7 +163,6 @@ section ServerM -- need to reparse the header so that the offsets are correct. let st ← read let oldDoc ← st.docRef.get - oldDoc.cancelTk.set let newHeaderSnap ← reparseHeader newMeta.text.source oldDoc.headerSnap if newHeaderSnap.stx != oldDoc.headerSnap.stx then throwServerError "Internal server error: header changed but worker wasn't restarted." @@ -175,6 +174,7 @@ section ServerM throwServerError "Internal server error: elab task was aborted while still in use." | some (TaskError.ioError ioError) => throw ioError | _ => -- No error or EOF + oldDoc.cancelTk.set -- NOTE(WN): we invalidate eagerly as `endPos` consumes input greedily. To re-elaborate only -- when really necessary, we could do a whitespace-aware `Syntax` comparison instead. let mut validSnaps := cmdSnaps.finishedPrefix.takeWhile (fun s => s.endPos < changePos)