private def waitForExit (child : LspChild) (tries : Nat := 50) (sleepMs : Nat := 20) : IO Bool := do
  let rec loop : Nat → IO Bool
    | 0 => do
        match (← child.tryWait) with
        | some _ => pure true
        | none => pure false
    | n + 1 => do
        match (← child.tryWait) with
        | some _ => pure true
        | none =>
            IO.sleep sleepMs.toUInt32
            loop n
  loop tries
private def gracefulStopTries : Nat := 8
private def postKillStopTries : Nat := 12
private def finalStopTries : Nat := 6
private def stopPollMs : Nat := 10

private def terminateSession (s : Session) : IO Bool := do
  let killDescendants (sig : String) : IO Unit := do
    try
      let _ ← IO.Process.output {
        cmd := "pkill"
        args := #["-" ++ sig, "-P", toString s.child.pid]
        stdin := .null
        stderr := .null
      }
      pure ()
    catch _ =>
      pure ()
  let shutdownReq := mkRequest s.nextId "shutdown" (Lean.Json.mkObj [])
  let exitNotif := mkNotification "exit" (Lean.Json.mkObj [])
  try
    send s.child.stdin shutdownReq
    send s.child.stdin exitNotif
  catch _ =>
    pure ()
  let stoppedGracefully ← waitForExit s.child gracefulStopTries stopPollMs
  if stoppedGracefully then
    pure true
  else
    killDescendants "TERM"
    try
      s.child.kill
    catch _ =>
      pure ()
    let stoppedAfterKill ← waitForExit s.child postKillStopTries stopPollMs
    if stoppedAfterKill then
      pure true
    else
      killDescendants "KILL"
      waitForExit s.child finalStopTries stopPollMs

        s.child.kill
        let _ ← s.child.wait

        let stopped ← terminateSession s

        return { state with message := "LSP stopped" }

        return { state with message := if stopped then "LSP stopped" else "LSP stop timeout; force-detached" }

            s.child.kill
            let _ ← s.child.wait

            let _ ← terminateSession s

      let wsClosed :=

      let (wsClosed, forceQuit) :=

        | none => ws

        | none => (ws, false)

            | none => ws

            | none =>
                (ws, true)

                { ws with layout := layout', activeWindowId := active' }.pruneFloatingWindows

                ({ ws with layout := layout', activeWindowId := active' }.pruneFloatingWindows, false)

      state.updateCurrentWorkspace (fun _ => wsFinal)

      let s' := state.updateCurrentWorkspace (fun _ => wsFinal)
      if forceQuit then
        { s' with shouldQuit := true }
      else
        s'

    ViE.Lsp.Lean.stopIfRunning

  let sInfoOnly := ViE.Window.closeActiveWindow sLean'
  let sInfoOnly' ← ViE.Lsp.Lean.syncInfoViewWindow sInfoOnly
  let wsInfoOnly := sInfoOnly'.getCurrentWorkspace
  assertEqual "InfoView-only fallback requests quit" true sInfoOnly'.shouldQuit
  assertEqual "InfoView-only fallback removes InfoView buffer" true ((wsInfoOnly.buffers.find? (fun b => b.filename == some ViE.Lsp.Lean.infoViewVirtualPath)).isNone)