max/lean4-htt
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions 2

chore: temporarily disable Elab.async in the server (#7254)

Browse source 
...pending further testing of #7241 post-release
This commit is contained in:
Sebastian Ullrich 2025-02-27 09:31:54 +01:00 • committed by GitHub
parent 727c696d9f
commit 87e8da5230
No known key found for this signature in database
GPG key ID: B5690EEEBB952194
1 changed files with 2 additions and 1 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

3
src/Lean/Server/FileWorker.lean
View file

@ -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