From 87e8da5230540a779c4eaed1d2a6276794564263 Mon Sep 17 00:00:00 2001 From: Sebastian Ullrich Date: Thu, 27 Feb 2025 09:31:54 +0100 Subject: [PATCH] chore: temporarily disable Elab.async in the server (#7254) ...pending further testing of #7241 post-release --- src/Lean/Server/FileWorker.lean | 3 ++- 1 file changed, 2 insertions(+), 1 deletion(-) diff --git a/src/Lean/Server/FileWorker.lean b/src/Lean/Server/FileWorker.lean index fab55b498d..c5e599fa6a 100644 --- a/src/Lean/Server/FileWorker.lean +++ b/src/Lean/Server/FileWorker.lean @@ -390,7 +390,8 @@ 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 + -- (temporarily disabled pending #7241) + --let opts := Elab.async.setIfNotSet opts true return .ok { mainModuleName