Skip to content

ci: set TEST_ARGS manually #422

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Merged
fmontesi merged 4 commits into from
Mar 17, 2026
Merged

ci: set TEST_ARGS manually #422

Changes from all commits
Commits
Show all changes
4 commits
Select commit Hold shift + click to select a range
86b1a33
ci: set TEST_ARGS manually
chenson2018 Mar 12, 2026
d3d8ed0
implicit_reducible
chenson2018 Mar 12, 2026
f844d13
use instance for Fintype
chenson2018 Mar 17, 2026
70bb918
Merge remote-tracking branch 'origin/main' into test-args-temp
chenson2018 Mar 17, 2026
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
4 changes: 4 additions & 0 deletions .github/workflows/lean_action_ci.yml
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -14,6 +14,10 @@ jobs:
runs-on: ubuntu-latest
steps:
- uses: actions/checkout@v4
- name: Set TEST_ARGS manually
run: |
echo "TEST_ARGS='--wfail --iofail'" >> $GITHUB_ENV
shell: bash
- uses: leanprover/lean-action@v1
Copy link
Collaborator

@eric-wieser eric-wieser Mar 17, 2026

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

I think you can also change the v1 and possibly the username here to point at the commit with the fix

Copy link
Collaborator Author

@chenson2018 chenson2018 Mar 17, 2026 •
edited
Loading

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

I'd be happy to point to a specific commit in the lean-action repo once the fix lands, but I'm not sure we should point to individual usernames in CI if at all avoidable. I was initially of the opinion that sticking to v1 seemed fine as this does pick up new minor releases, but the PR adding test-args (where I was the one who introduced the bug...) took ~5 months to land in a release,

Copy link
Collaborator

@eric-wieser eric-wieser Mar 17, 2026

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

If you point to a specific git hash then I think the risk of pointing to an external user goes away.

with:
build-args: "--wfail --iofail"
Expand Down
Loading