Skip to content

Commit 11b09de

Browse files
GZGavinZhaoGZGavinZhao
committed
Introduce lint-args
1 parent 65f454b commit 11b09de

6 files changed

Lines changed: 166 additions & 1 deletion

File tree

‎.github/functional_tests/lake_lint_args/action.yml‎

Lines changed: 134 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,134 @@
1+
name: 'Lake Lint Args'
2+
description: 'Run `lean-action` on with `lint-args` input'
3+
inputs:
4+
toolchain:
5+
description: 'Toolchain to use for the test'
6+
required: true
7+
runs:
8+
using: 'composite'
9+
steps:
10+
# TODO: once `lean-action` supports just setup, use it here
11+
- name: install elan
12+
run: |
13+
set -o pipefail
14+
curl https://raw.githubusercontent.com/leanprover/elan/master/elan-init.sh -sSf | sh -s -- -y --default-toolchain ${{ inputs.toolchain }}
15+
echo "$HOME/.elan/bin" >> "$GITHUB_PATH"
16+
shell: bash
17+
18+
- name: create lake package with `lake init ${{ inputs.lake-init-arguments }}`
19+
run: |
20+
lake init lintargs .lean
21+
lake update
22+
shell: bash
23+
24+
- name: create lint script template
25+
run: |
26+
cat <<'TEMPLATE' > lint_script.template
27+
@[lint_driver]
28+
script check_lint_args (args) do
29+
let expected := @EXPECTED_ARGS@
30+
if args == expected then
31+
IO.println s!"✓ Arguments match expected: {expected}"
32+
return 0
33+
else
34+
IO.eprintln s!"✗ Arguments mismatch!"
35+
IO.eprintln s!" Expected: {expected}"
36+
IO.eprintln s!" Got: {args}"
37+
return 1
38+
TEMPLATE
39+
shell: bash
40+
41+
- name: configure script for single driver argument test
42+
run: |
43+
sed 's/@EXPECTED_ARGS@/["test-arg"]/' lint_script.template > lakefile.lean
44+
shell: bash
45+
46+
- name: "run `lean-action` with single lint-arg passed to driver"
47+
id: lean-action-single
48+
uses: ./
49+
with:
50+
lint: true
51+
lint-args: "-- test-arg"
52+
use-github-cache: false
53+
54+
- name: verify `lean-action` outcome success
55+
env:
56+
OUTPUT_NAME: "lean-action-single.outcome"
57+
EXPECTED_VALUE: "success"
58+
ACTUAL_VALUE: ${{ steps.lean-action-single.outcome }}
59+
run: .github/functional_tests/test_helpers/verify_action_output.sh
60+
shell: bash
61+
62+
- name: verify single argument was passed correctly
63+
env:
64+
OUTPUT_NAME: "lint-status (single arg)"
65+
EXPECTED_VALUE: "SUCCESS"
66+
ACTUAL_VALUE: ${{ steps.lean-action-single.outputs.lint-status }}
67+
run: .github/functional_tests/test_helpers/verify_action_output.sh
68+
shell: bash
69+
70+
- name: lake clean
71+
run: lake clean
72+
shell: bash
73+
74+
- name: configure script for multiple driver arguments test
75+
run: |
76+
sed 's/@EXPECTED_ARGS@/["arg1", "arg2", "arg3"]/' lint_script.template > lakefile.lean
77+
shell: bash
78+
79+
- name: "run `lean-action` with multiple lint args passed to driver"
80+
id: lean-action-multiple
81+
uses: ./
82+
with:
83+
lint: true
84+
lint-args: "-- arg1 arg2 arg3"
85+
use-github-cache: false
86+
87+
- name: verify `lean-action-multiple` outcome success
88+
env:
89+
OUTPUT_NAME: "lean-action-multiple.outcome"
90+
EXPECTED_VALUE: "success"
91+
ACTUAL_VALUE: ${{ steps.lean-action-multiple.outcome }}
92+
run: .github/functional_tests/test_helpers/verify_action_output.sh
93+
shell: bash
94+
95+
- name: verify multiple arguments were passed correctly
96+
env:
97+
OUTPUT_NAME: "lint-status (multiple args)"
98+
EXPECTED_VALUE: "SUCCESS"
99+
ACTUAL_VALUE: ${{ steps.lean-action-multiple.outputs.lint-status }}
100+
run: .github/functional_tests/test_helpers/verify_action_output.sh
101+
shell: bash
102+
103+
- name: lake clean
104+
run: lake clean
105+
shell: bash
106+
107+
- name: configure script for empty args test (lake flags)
108+
run: |
109+
sed 's/@EXPECTED_ARGS@/([] : List String)/' lint_script.template > lakefile.lean
110+
shell: bash
111+
112+
- name: "run `lean-action` with lake flags (not driver args)"
113+
id: lean-action-flags
114+
uses: ./
115+
with:
116+
lint: true
117+
lint-args: "--quiet"
118+
use-github-cache: false
119+
120+
- name: verify `lean-action-flags` outcome success
121+
env:
122+
OUTPUT_NAME: "lean-action-flags.outcome"
123+
EXPECTED_VALUE: "success"
124+
ACTUAL_VALUE: ${{ steps.lean-action-flags.outcome }}
125+
run: .github/functional_tests/test_helpers/verify_action_output.sh
126+
shell: bash
127+
128+
- name: verify lake flag was passed correctly
129+
env:
130+
OUTPUT_NAME: "lint-status (lake flags)"
131+
EXPECTED_VALUE: "SUCCESS"
132+
ACTUAL_VALUE: ${{ steps.lean-action-flags.outputs.lint-status }}
133+
run: .github/functional_tests/test_helpers/verify_action_output.sh
134+
shell: bash

‎.github/workflows/functional_tests.yml‎

Lines changed: 8 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -118,6 +118,14 @@ jobs:
118118
with:
119119
toolchain: ${{ env.toolchain }}
120120

121+
lake-lint-args:
122+
runs-on: ubuntu-latest
123+
steps:
124+
- uses: actions/checkout@v5
125+
- uses: ./.github/functional_tests/lake_lint_args
126+
with:
127+
toolchain: ${{ env.toolchain }}
128+
121129
lake-check-test-failure:
122130
runs-on: ubuntu-latest
123131
steps:

‎CHANGELOG.md‎

Lines changed: 4 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -7,6 +7,10 @@ and this project adheres to [Semantic Versioning](https://semver.org/spec/v2.0.0
77

88
## Unreleased
99

10+
### Added
11+
12+
- new `lint-args` input to specify arguments to pass to `lake lint`
13+
1014
## v1.4.0 - 2026-01-15
1115

1216
### Added

‎README.md‎

Lines changed: 5 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -183,6 +183,11 @@ To be certain `lean-action` runs a step, specify the desire feature with a featu
183183
# By default, `lean-action` calls `lake test` with no arguments.
184184
test-args: ""
185185

186+
# Lint arguments to pass to `lake lint {lint-args}`.
187+
# For example, `lint-args: "--quiet"` will run `lake lint --quiet`.
188+
# By default, `lean-action` calls `lake lint` with no arguments.
189+
lint-args: ""
190+
186191
# By default, `lean-action` attempts to automatically detect a Mathlib dependency and run `lake exe cache get` accordingly.
187192
# Setting `use-mathlib-cache` will override automatic detection and run (or not run) `lake exe cache get`.
188193
# Project must be downstream of Mathlib to use the Mathlib cache.

‎action.yml‎

Lines changed: 11 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -61,6 +61,13 @@ inputs:
6161
By default, `lean-action` calls `lake test` with no arguments.
6262
required: false
6363
default: ""
64+
lint-args:
65+
description: |
66+
Lint arguments to pass to `lake lint {lint-args}`.
67+
For example, `lint-args: "--quiet"` will run `lake lint --quiet`.
68+
By default, `lean-action` calls `lake lint` with no arguments.
69+
required: false
70+
default: ""
6471
use-mathlib-cache:
6572
description: |
6673
By default, `lean-action` attempts to automatically detect a Mathlib dependency and run `lake exe cache get` accordingly.
@@ -225,6 +232,8 @@ runs:
225232
- name: test ${{ github.repository }}
226233
id: test
227234
if: ${{ steps.config.outputs.run-lake-test == 'true'}}
235+
env:
236+
TEST_ARGS: ${{ inputs.test-args }}
228237
run: |
229238
: Lake Test
230239
${GITHUB_ACTION_PATH}/scripts/lake_test.sh
@@ -235,6 +244,8 @@ runs:
235244
id: lint
236245
# only run linter if the user provided a module to lint
237246
if: ${{ steps.config.outputs.run-lake-lint == 'true'}}
247+
env:
248+
LINT_ARGS: ${{ inputs.lint-args }}
238249
run: |
239250
: Lake Lint
240251
${GITHUB_ACTION_PATH}/scripts/lake_lint.sh

‎scripts/lake_lint.sh‎

Lines changed: 4 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -1,6 +1,7 @@
11
#!/bin/bash
22
set -e
33

4+
# start log group
45
echo "::group::Lake Lint Output"
56

67
# handle_exit function to handle the exit status of the script
@@ -12,11 +13,13 @@ handle_exit() {
1213
echo "::error:: lake lint failed"
1314
else
1415
echo "lint-status=SUCCESS" >>"$GITHUB_OUTPUT"
16+
# end log group and add a new line to improve readabiltiy
1517
echo "::endgroup::"
1618
echo
1719
fi
1820
}
1921

2022
trap handle_exit EXIT
2123

22-
lake lint
24+
# use eval to ensure lint arguments are expanded
25+
eval "lake lint $LINT_ARGS"

0 commit comments

Comments
 (0)