Git Bash/mintty is not recognized as a tty on Windows

Prerequisites

Please put an X between the brackets as you perform the following steps:

• Check that your issue is not already filed:
  https://github.com/leanprover/lean4/issues
• Reduce the issue to a minimal, self-contained, reproducible test case.
  Avoid dependencies to Mathlib or Batteries.
• Test your test case against the latest nightly release, for example on
  https://live.lean-lang.org/#project=lean-nightly
  (You can also use the settings there to switch to “Lean nightly”)

Description

When invoking lake build inside Git Bash on Windows Server 2022, Lake's ANSI autodetection decides that the terminal is not a tty and uses the non-interactive format for status messages.

The problem is reproducible when using the Git Bash backed by mintty 3.7.6 on the FRO Windows machine.

The problem is not present on the FRO Windows machine in the following scenarios:

• Git Bash inside VS Code
• CLANG64 shell backed by mintty 3.7.4
• PowerShell

Previously there was an older version of Git for Windows installed on the FRO machine that shipped with mintty 3.7.1 and there the problem was also reproducible. So unless the bug is there in mintty 3.7.1 and 3.7.6 but not in 3.7.4, this seems to be a problem with Git for Windows and not with upstream mintty.

Expected behavior: lake build and lake build --ansi are equivalent when calling from Git Bash

Actual behavior: lake build and lake build --no-ansi are equivalent when calling from Git Bash

Versions

Windows Server 2022 Version 21H2 (OS Build 20348.1487)

Lean (version 4.12.0-rc1, x86_64-w64-windows-gnu, commit e9e858a44849, Release)

Impact

Add 👍 to issues you consider important. If others are impacted by this issue, please ask them to add 👍 to it.

Start by reproducing lake build and comparing it with lake build --ansi in Git Bash backed by mintty on Windows. Trace Lake's ANSI autodetection and compare the terminal behavior with the listed PowerShell, VS Code Git Bash, and CLANG64 scenarios; done means Git Bash treats lake build and lake build --ansi equivalently without regressing the other environments.