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

chore: temporarily disable async in server (#6813)

Browse source 
... pending an interruption bug fix and further testing
This commit is contained in:
Sebastian Ullrich 2025-01-28 11:42:17 +01:00 • committed by GitHub
parent 6aa6407af1
commit e4364e747f
No known key found for this signature in database
GPG key ID: B5690EEEBB952194
1 changed files with 1 additions and 1 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

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

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