ci: wrap linting with stdbuf -oL so log output appears immediately (leanprover-community#33783)

leanprover-community#33696 changed the linting step so that it pipes its output into `tee`; this causes `lake exe runLinter` to block buffer its output, which means that if the linters freeze (cf. [#mathlib4 > slow linting step CI?](https://leanprover.zulipchat.com/#narrow/channel/287929-mathlib4/topic/slow.20linting.20step.20CI.3F/with/567049377)), we may not see all of the log output.

This PR uses [`stdbuf -oL`](https://www.gnu.org/software/coreutils/manual/html_node/stdbuf-invocation.html) to make the output line buffered instead, which should solve this.

Author: bryangingechen

.github/build.in.yml

@@ -503,7 +503,7 @@ jobs:
           cd pr-branch
           # Try running with --trace; if it fails due to argument parsing, the PR needs to merge master
           # We use .lake/ for the output file because landrun restricts /tmp access
-          if ! env LEAN_ABORT_ON_PANIC=1 lake exe runLinter --trace Mathlib 2>&1 | tee .lake/lint_output.txt; then
+          if ! env LEAN_ABORT_ON_PANIC=1 stdbuf -oL lake exe runLinter --trace Mathlib 2>&1 | tee .lake/lint_output.txt; then
             if grep -q "cannot parse arguments" .lake/lint_output.txt; then
               echo ""
               echo "=============================================================================="

.github/workflows/bors.yml

@@ -513,7 +513,7 @@ jobs:
           cd pr-branch
           # Try running with --trace; if it fails due to argument parsing, the PR needs to merge master
           # We use .lake/ for the output file because landrun restricts /tmp access
-          if ! env LEAN_ABORT_ON_PANIC=1 lake exe runLinter --trace Mathlib 2>&1 | tee .lake/lint_output.txt; then
+          if ! env LEAN_ABORT_ON_PANIC=1 stdbuf -oL lake exe runLinter --trace Mathlib 2>&1 | tee .lake/lint_output.txt; then
             if grep -q "cannot parse arguments" .lake/lint_output.txt; then
               echo ""
               echo "=============================================================================="

.github/workflows/build.yml

@@ -519,7 +519,7 @@ jobs:
           cd pr-branch
           # Try running with --trace; if it fails due to argument parsing, the PR needs to merge master
           # We use .lake/ for the output file because landrun restricts /tmp access
-          if ! env LEAN_ABORT_ON_PANIC=1 lake exe runLinter --trace Mathlib 2>&1 | tee .lake/lint_output.txt; then
+          if ! env LEAN_ABORT_ON_PANIC=1 stdbuf -oL lake exe runLinter --trace Mathlib 2>&1 | tee .lake/lint_output.txt; then
             if grep -q "cannot parse arguments" .lake/lint_output.txt; then
               echo ""
               echo "=============================================================================="

.github/workflows/build_fork.yml

@@ -517,7 +517,7 @@ jobs:
           cd pr-branch
           # Try running with --trace; if it fails due to argument parsing, the PR needs to merge master
           # We use .lake/ for the output file because landrun restricts /tmp access
-          if ! env LEAN_ABORT_ON_PANIC=1 lake exe runLinter --trace Mathlib 2>&1 | tee .lake/lint_output.txt; then
+          if ! env LEAN_ABORT_ON_PANIC=1 stdbuf -oL lake exe runLinter --trace Mathlib 2>&1 | tee .lake/lint_output.txt; then
             if grep -q "cannot parse arguments" .lake/lint_output.txt; then
               echo ""
               echo "=============================================================================="