Skip to content

Commit f217e8c

Browse files
authored
test: iofail and merge_group trigger (#224)
This PR makes two small changes to CI: - Adds a `merge_group` trigger - Passes the `--iofail` option to `build-args` The motivation of having the `merge_group` trigger is to ensure that there is a final build that happens before a PR is merged into `main`, preventing situations where a release happens while a PR is pending and then only failing after being merged. For this to take effect, I need someone with adequate permissions to require merge queues for the `main` branch. These should still be configured as squash commits. I would be fine setting the merge limit low (maybe even 1) for simplicity since we don't yet have high enough volume of commits for this to matter. The `--iofail` option is straightforward, mirroring what Mathlib already does.
1 parent fb7ccbe commit f217e8c

2 files changed

Lines changed: 3 additions & 2 deletions

File tree

.github/workflows/docs.yml

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -25,7 +25,7 @@ jobs:
2525
id: build-lean
2626
uses: leanprover/lean-action@v1
2727
with:
28-
build-args: "--wfail"
28+
build-args: "--wfail --iofail"
2929

3030
- name: Build project documentation
3131
id: build-docgen

.github/workflows/lean_action_ci.yml

Lines changed: 2 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -6,6 +6,7 @@ on:
66
- main
77
- nightly-testing
88
pull_request:
9+
merge_group:
910
workflow_dispatch:
1011

1112
jobs:
@@ -15,7 +16,7 @@ jobs:
1516
- uses: actions/checkout@v4
1617
- uses: leanprover/lean-action@v1
1718
with:
18-
build-args: "--wfail"
19+
build-args: "--wfail --iofail"
1920
mk_all-check: "true"
2021
- name: "lake exe shake"
2122
run: |

0 commit comments

Comments
 (0)