chore: temporarily disable Elab.async in the server

2026-03-21 12:24:11 +00:00 · 2025-02-27 09:14:09 +01:00
1 changed files with 2 additions and 1 deletions
--- 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