diff --git a/src/Lean/CoreM.lean b/src/Lean/CoreM.lean index 8b9c9c46ac..293b8ab4c2 100644 --- a/src/Lean/CoreM.lean +++ b/src/Lean/CoreM.lean @@ -36,7 +36,7 @@ register_builtin_option Elab.async : Bool := { descr := "perform elaboration using multiple threads where possible\ \n\ \nThis option defaults to `false` but (when not explicitly set) is overridden to `true` in \ - `Lean.Language.Lean.process` as used by the cmdline driver and language server. \ + the language server. \ Metaprogramming users driving elaboration directly via e.g. \ `Lean.Elab.Command.elabCommandTopLevel` can opt into asynchronous elaboration by setting \ this option but then are responsible for processing messages and other data not only in the \ diff --git a/src/Lean/Language/Lean.lean b/src/Lean/Language/Lean.lean index c1a467f4a6..33a0807bee 100644 --- a/src/Lean/Language/Lean.lean +++ b/src/Lean/Language/Lean.lean @@ -433,8 +433,6 @@ where } -- now that imports have been loaded, check options again let opts ← reparseOptions setup.opts - -- default to async elaboration; see also `Elab.async` docs - let opts := Elab.async.setIfNotSet opts true let cmdState := Elab.Command.mkState headerEnv msgLog opts let cmdState := { cmdState with infoState := { diff --git a/src/Lean/Server/FileWorker.lean b/src/Lean/Server/FileWorker.lean index a10dda3aba..2ee0c9e1ba 100644 --- a/src/Lean/Server/FileWorker.lean +++ b/src/Lean/Server/FileWorker.lean @@ -325,6 +325,9 @@ def setupImports (meta : DocumentMeta) (cmdlineOpts : Options) (chanOut : Std.Ch -- override cmdline options with file options 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 + return .ok { mainModuleName opts diff --git a/tests/bench/speedcenter.exec.velcom.yaml b/tests/bench/speedcenter.exec.velcom.yaml index a9481abc5b..86aac12a31 100644 --- a/tests/bench/speedcenter.exec.velcom.yaml +++ b/tests/bench/speedcenter.exec.velcom.yaml @@ -54,6 +54,18 @@ wc -c ${BUILD:-../../build/release}/stage2/lib/lean/libleanshared.so | cut -d' ' -f 1 max_runs: 1 runner: output +- attributes: + description: Init.Prelude async + tags: [fast] + run_config: + <<: *time + cmd: lean ../../src/Init/Prelude.lean -DElab.async=true +- attributes: + description: Init.Data.List.Sublist async + tags: [fast] + run_config: + <<: *time + cmd: lean ../../src/Init/Data/List/Sublist.lean -DElab.async=true - attributes: description: import Lean tags: [fast]