fix: only log goals accomplished in language server (#7416)

This PR addresses a performance regression noticed at
https://github.com/leanprover/lean4/pull/7366#issuecomment-2708162029.
It also ensures that we also consider the current message log when
logging the goals accomplished message.


`Language.Lean.internal.cmdlineSnapshots` in `Lean.Language.Lean` is
moved to `Lean.internal.cmdlineSnapshots` in `Lean.CoreM` to make the
option available in the elaborator.

src/Lean/CoreM.lean

@@ -44,6 +44,13 @@ register_builtin_option Elab.async : Bool := {
       `Lean.Command.State.snapshotTasks`."
 }
 
+/-- Performance option used by cmdline driver. -/
+register_builtin_option internal.cmdlineSnapshots : Bool := {
+  defValue := false
+  descr    := "reduce information stored in snapshots to the minimum necessary \
+    for the cmdline driver: diagnostics per command and final full snapshot"
+}
+
 /--
 If the `diagnostics` option is not already set, gives a message explaining this option.
 Begins with a `\n\n`, so an error message can look like `m!"some error occurred{useDiagnosticMsg}"`.

src/Lean/Elab/Frontend.lean

@@ -146,7 +146,7 @@ def runFrontend
     : IO (Environment × Bool) := do
   let startTime := (← IO.monoNanosNow).toFloat / 1000000000
   let inputCtx := Parser.mkInputContext input fileName
-  let opts := Language.Lean.internal.cmdlineSnapshots.setIfNotSet opts true
+  let opts := Lean.internal.cmdlineSnapshots.setIfNotSet opts true
   let ctx := { inputCtx with }
   let processor := Language.Lean.process
   let snap ← processor (fun _ => pure <| .ok { mainModuleName, opts, trustLevel, plugins }) none ctx

src/Lean/Elab/MutualDef.lean

@@ -1075,12 +1075,17 @@ is error-free and contains no syntactical `sorry`s.
 -/
 private def logGoalsAccomplishedSnapshotTask (views : Array DefView)
     (defsParsedSnap : DefsParsedSnapshot) : TermElabM Unit := do
+  if Lean.internal.cmdlineSnapshots.get (← getOptions) then
+    -- Skip 'goals accomplished' task if we are on the command line.
+    -- These messages are only used in the language server.
+    return
+  let currentLog ← Core.getMessageLog
   let snaps := #[SnapshotTask.finished none (toSnapshotTree defsParsedSnap)] ++
     (← getThe Core.State).snapshotTasks
   let tree := SnapshotTree.mk { diagnostics := .empty } snaps
   let logGoalsAccomplishedAct ← Term.wrapAsyncAsSnapshot (cancelTk? := none) fun () => do
     -- NOTE: `waitAll` below ensures `getAll` will not block here
-    let logs := tree.getAll.map (·.diagnostics.msgLog)
+    let logs := tree.getAll.map (·.diagnostics.msgLog) |>.push currentLog
     let hasErrorOrSorry := logs.any fun log =>
       log.reportedPlusUnreported.any fun msg =>
         msg.severity matches .error || msg.data.hasTag (· == `hasSorry)

src/Lean/Language/Lean.lean

@@ -290,13 +290,6 @@ structure SetupImportsResult where
   /-- Lean plugins to load as part of the environment setup. -/
   plugins : Array System.FilePath := #[]
 
-/-- Performance option used by cmdline driver. -/
-register_builtin_option internal.cmdlineSnapshots : Bool := {
-  defValue := false
-  descr    := "reduce information stored in snapshots to the minimum necessary \
-    for the cmdline driver: diagnostics per command and final full snapshot"
-}
-
 /--
 Parses values of options registered during import and left by the C++ frontend as strings.
 Removes `weak` prefixes from both parsed and unparsed options and fails if any option names remain