From 18507dcd513a1bdf7f8db8bb07296489d51a2766 Mon Sep 17 00:00:00 2001
From: Jesse Alama <hello@jessealama.net>
Date: Tue, 8 Sep 2026 18:25:11 +0000
Subject: [PATCH] ci: declare shell: bash as the workflow default for pipefail

When a run step has no shell key, GitHub executes it with 'bash -e {0}';
declaring 'shell: bash' explicitly upgrades that to
'bash --noprofile --norc -eo pipefail {0}', so every step gets pipefail
for free. Applied to the six workflows that have run steps.

Audited every existing pipeline for behaviour changes:
- weekly-lints: 'lake build | tee' already sets pipefail by hand and
  captures the status with '|| build_status=$?', so nothing changes
- shellcheck: a failure of the 'find' feeding xargs now fails the step
  instead of being masked
- the remaining bash steps contain no pipelines

The explicit 'set -e' lines in lean_action_ci.yml are dropped as
redundant; steps with 'shell: python' are unaffected by the default.
---
 .../workflows/bump_toolchain_nightly-testing.yml    |  5 +++++
 .github/workflows/lean_action_ci.yml                | 13 +++++++------
 .../workflows/merge_main_into_nightly-testing.yml   |  5 +++++
 .../workflows/report_failures_nightly-testing.yml   |  5 +++++
 .github/workflows/shellcheck.yml                    |  5 +++++
 .github/workflows/weekly-lints.yml                  |  5 +++++
 6 files changed, 32 insertions(+), 6 deletions(-)

diff --git a/.github/workflows/bump_toolchain_nightly-testing.yml b/.github/workflows/bump_toolchain_nightly-testing.yml
index 7bab15c8fc..3bdc8ff79c 100644
--- a/.github/workflows/bump_toolchain_nightly-testing.yml
+++ b/.github/workflows/bump_toolchain_nightly-testing.yml
@@ -7,6 +7,11 @@ on:
     # This should be 3 hours after lean4 starts building its nightly.
   workflow_dispatch:
 
+# Runs every step under `bash --noprofile --norc -eo pipefail`
+defaults:
+  run:
+    shell: bash
+
 jobs:
   update-toolchain:
     if: github.repository == 'leanprover/cslib'
diff --git a/.github/workflows/lean_action_ci.yml b/.github/workflows/lean_action_ci.yml
index 95bc25bd12..85923ccde8 100644
--- a/.github/workflows/lean_action_ci.yml
+++ b/.github/workflows/lean_action_ci.yml
@@ -9,6 +9,11 @@ on:
   merge_group:
   workflow_dispatch:
 
+# Runs every step under `bash --noprofile --norc -eo pipefail`
+defaults:
+  run:
+    shell: bash
+
 jobs:
   ci-checks:
     runs-on: ubuntu-latest
@@ -19,17 +24,13 @@ jobs:
           build-args: "--wfail --iofail"
           test-args: "--wfail --iofail"
       - name: "lake exe mk_all --check"
-        run: |
-          set -e
-          lake exe mk_all --check
+        run: lake exe mk_all --check
       #- name: "lake shake"
       #  run: |
       #    set -e
       #    lake shake --add-public --keep-implied --keep-prefix Cslib
       - name: "checkInitImports"
-        run: |
-          set -e
-          lake exe checkInitImports
+        run: lake exe checkInitImports
       - uses: leanprover-community/lint-style-action@e6128ab22cb03b509075ae46c33727e3952ffab7 # 2026-05-12
         with:
           mode: check
diff --git a/.github/workflows/merge_main_into_nightly-testing.yml b/.github/workflows/merge_main_into_nightly-testing.yml
index 3d73be5c56..a5f27e48be 100644
--- a/.github/workflows/merge_main_into_nightly-testing.yml
+++ b/.github/workflows/merge_main_into_nightly-testing.yml
@@ -8,6 +8,11 @@ on:
     - cron: '30 */3 * * *'  # At minute 30 past every 3rd hour.
   workflow_dispatch:
 
+# Runs every step under `bash --noprofile --norc -eo pipefail`
+defaults:
+  run:
+    shell: bash
+
 jobs:
   merge-to-nightly-testing:
     if: github.repository == 'leanprover/cslib'
diff --git a/.github/workflows/report_failures_nightly-testing.yml b/.github/workflows/report_failures_nightly-testing.yml
index edeeb91682..9dfadcb31e 100644
--- a/.github/workflows/report_failures_nightly-testing.yml
+++ b/.github/workflows/report_failures_nightly-testing.yml
@@ -6,6 +6,11 @@ on:
     types:
       - completed
 
+# Runs every step under `bash --noprofile --norc -eo pipefail`
+defaults:
+  run:
+    shell: bash
+
 jobs:
   handle_failure:
 
diff --git a/.github/workflows/shellcheck.yml b/.github/workflows/shellcheck.yml
index ea590a0369..4acbefefcf 100644
--- a/.github/workflows/shellcheck.yml
+++ b/.github/workflows/shellcheck.yml
@@ -11,6 +11,11 @@ on:
       - 'scripts/**/*.sh'
   workflow_dispatch:
 
+# Runs every step under `bash --noprofile --norc -eo pipefail`
+defaults:
+  run:
+    shell: bash
+
 jobs:
   shellcheck:
     name: Check shell scripts
diff --git a/.github/workflows/weekly-lints.yml b/.github/workflows/weekly-lints.yml
index 74c6afc08c..39b3e92783 100644
--- a/.github/workflows/weekly-lints.yml
+++ b/.github/workflows/weekly-lints.yml
@@ -8,6 +8,11 @@ on:
 env:
   CSLIB: cslib
 
+# Runs every step under `bash --noprofile --norc -eo pipefail`
+defaults:
+  run:
+    shell: bash
+
 jobs:
   weekly-lints:
     name: Weekly Linting