Revert "perf: keep alive old single-threaded cmdline driver for a lit…

…tle longer"

This reverts commit 6ec85ec.

src/Lean/Elab/Frontend.lean

@@ -38,19 +38,7 @@ def setCommandState (commandState : Command.State) : FrontendM Unit :=
 
 def elabCommandAtFrontend (stx : Syntax) : FrontendM Unit := do
   runCommandElabM do
-    let initMsgs ← modifyGet fun st => (st.messages, { st with messages := {} })
     Command.elabCommandTopLevel stx
-    let mut msgs := (← get).messages
-    -- `stx.hasMissing` should imply `initMsgs.hasErrors`, but the latter should be cheaper to check
-    -- in general
-    if !Language.Lean.showPartialSyntaxErrors.get (← getOptions) && initMsgs.hasErrors &&
-        stx.hasMissing then
-      -- discard elaboration errors, except for a few important and unlikely misleading ones, on
-      -- parse error
-      msgs := ⟨msgs.msgs.filter fun msg =>
-        msg.data.hasTag (fun tag => tag == `Elab.synthPlaceholder ||
-          tag == `Tactic.unsolvedGoals || (`_traceMsg).isSuffixOf tag)⟩
-    modify ({ · with messages := initMsgs ++ msgs })
 
 def updateCmdPos : FrontendM Unit := do
   modify fun s => { s with cmdPos := s.parserState.pos }
@@ -110,32 +98,6 @@ def runFrontend
   let inputCtx := Parser.mkInputContext input fileName
   -- TODO: replace with `#lang` processing
   let lang := Language.Lean
-  if /- Lean #lang? -/ true then
-    -- Temporarily keep alive old cmdline driver for the Lean language so that we don't pay the
-    -- overhead of passing the environment between snapshots until we actually make good use of it
-    -- outside the server
-    let (header, parserState, messages) ← Parser.parseHeader inputCtx
-    -- allow `env` to be leaked, which would live until the end of the process anyway
-    let (env, messages) ← processHeader (leakEnv := true) header opts messages inputCtx trustLevel
-    let env := env.setMainModule mainModuleName
-    let mut commandState := Command.mkState env messages opts
-
-    if ileanFileName?.isSome then
-      -- Collect InfoTrees so we can later extract and export their info to the ilean file
-      commandState := { commandState with infoState.enabled := true }
-
-    let s ← IO.processCommands inputCtx parserState commandState
-    for msg in s.commandState.messages.toList do
-      IO.print (← msg.toString (includeEndPos := Language.printMessageEndPos.get opts))
-
-    if let some ileanFileName := ileanFileName? then
-      let trees := s.commandState.infoState.trees.toArray
-      let references := Lean.Server.findModuleRefs inputCtx.fileMap trees (localVars := false)
-      let ilean := { module := mainModuleName, references : Lean.Server.Ilean }
-      IO.FS.writeFile ileanFileName $ Json.compress $ toJson ilean
-
-    return (s.commandState.env, !s.commandState.messages.hasErrors)
-
   let ctx := { inputCtx with
     mainModuleName, opts, trustLevel
     fileSetupHandler? := none
@@ -156,5 +118,4 @@ def runFrontend
   let env := lang.getFinalEnv? snap |>.getD (← mkEmptyEnvironment)
   pure (env, !hasErrors)
 
-
 end Lean.Elab

tests/lean/Process.lean.expected.out

@@ -1,6 +1,5 @@
-hi!
-<stdin>:1:0: warning: using 'exit' to interrupt Lean
 1
+hi!
 0
 "ho!\n"
 "hu!\n"
@@ -9,5 +8,6 @@ flush of broken pipe failed
 100000
 0
 0
+<stdin>:1:0: warning: using 'exit' to interrupt Lean
 0
 0

tests/lean/dbgMacros.lean.expected.out

@@ -1,10 +1,10 @@
 PANIC at f dbgMacros:2:14: unexpected zero
-PANIC at g dbgMacros:10:14: unreachable code has been reached
-PANIC at h dbgMacros:16:0: assertion violation: x != 0
 0
 9
+PANIC at g dbgMacros:10:14: unreachable code has been reached
 0
 0
+PANIC at h dbgMacros:16:0: assertion violation: x != 0
 0
 f2, x: 10
 11