chore: disable Elab.async on the cmdline for now

leanprover · Jan 22, 2025 · 223ae09 · 223ae09
1 parent 9b74c07
commit 223ae09
Show file tree

Hide file tree

Showing 4 changed files with 16 additions and 3 deletions.
diff --git 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
@@ -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
@@ -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
@@ -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]