From e4364e747f8a5570f1bfca92ee6185b98a18e5ae Mon Sep 17 00:00:00 2001 From: Sebastian Ullrich Date: Tue, 28 Jan 2025 11:42:17 +0100 Subject: [PATCH] chore: temporarily disable async in server (#6813) ... pending an interruption bug fix and further testing --- 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 2ee0c9e1ba..281a01939d 100644 --- a/src/Lean/Server/FileWorker.lean +++ b/src/Lean/Server/FileWorker.lean @@ -326,7 +326,7 @@ def setupImports (meta : DocumentMeta) (cmdlineOpts : Options) (chanOut : Std.Ch let opts := cmdlineOpts.mergeBy (fun _ _ fileOpt => fileOpt) fileSetupResult.fileOptions -- default to async elaboration; see also `Elab.async` docs - let opts := Elab.async.setIfNotSet opts true + --let opts := Elab.async.setIfNotSet opts true return .ok { mainModuleName