Skip to content

Commit 3448a7d

Browse files
GZGavinZhaoGZGavinZhao
committed
Introduce lint-args
1 parent 65f454b commit 3448a7d

6 files changed

Lines changed: 165 additions & 1 deletion

File tree

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

Lines changed: 135 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,135 @@
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+
cp lakefile.lean lint_script.template
27+
cat <<'TEMPLATE' >> lint_script.template
28+
@[lint_driver]
29+
script check_lint_args (args) do
30+
let expected := @EXPECTED_ARGS@
31+
if args == expected then
32+
IO.println s!"✓ Arguments match expected: {expected}"
33+
return 0
34+
else
35+
IO.eprintln s!"✗ Arguments mismatch!"
36+
IO.eprintln s!" Expected: {expected}"
37+
IO.eprintln s!" Got: {args}"
38+
return 1
39+
TEMPLATE
40+
shell: bash
41+
42+
- name: configure script for single driver argument test
43+
run: |
44+
sed 's/@EXPECTED_ARGS@/["test-arg"]/' lint_script.template > lakefile.lean
45+
shell: bash
46+
47+
- name: "run `lean-action` with single lint-arg passed to driver"
48+
id: lean-action-single
49+
uses: ./
50+
with:
51+
lint: true
52+
lint-args: "-- test-arg"
53+
use-github-cache: false
54+
55+
- name: verify `lean-action` outcome success
56+
env:
57+
OUTPUT_NAME: "lean-action-single.outcome"
58+
EXPECTED_VALUE: "success"
59+
ACTUAL_VALUE: ${{ steps.lean-action-single.outcome }}
60+
run: .github/functional_tests/test_helpers/verify_action_output.sh
61+
shell: bash
62+
63+
- name: verify single argument was passed correctly
64+
env:
65+
OUTPUT_NAME: "lint-status (single arg)"
66+
EXPECTED_VALUE: "SUCCESS"
67+
ACTUAL_VALUE: ${{ steps.lean-action-single.outputs.lint-status }}
68+
run: .github/functional_tests/test_helpers/verify_action_output.sh
69+
shell: bash
70+
71+
- name: lake clean
72+
run: lake clean
73+
shell: bash
74+
75+
- name: configure script for multiple driver arguments test
76+
run: |
77+
sed 's/@EXPECTED_ARGS@/["arg1", "arg2", "arg3"]/' lint_script.template > lakefile.lean
78+
shell: bash
79+
80+
- name: "run `lean-action` with multiple lint args passed to driver"
81+
id: lean-action-multiple
82+
uses: ./
83+
with:
84+
lint: true
85+
lint-args: "-- arg1 arg2 arg3"
86+
use-github-cache: false
87+
88+
- name: verify `lean-action-multiple` outcome success
89+
env:
90+
OUTPUT_NAME: "lean-action-multiple.outcome"
91+
EXPECTED_VALUE: "success"
92+
ACTUAL_VALUE: ${{ steps.lean-action-multiple.outcome }}
93+
run: .github/functional_tests/test_helpers/verify_action_output.sh
94+
shell: bash
95+
96+
- name: verify multiple arguments were passed correctly
97+
env:
98+
OUTPUT_NAME: "lint-status (multiple args)"
99+
EXPECTED_VALUE: "SUCCESS"
100+
ACTUAL_VALUE: ${{ steps.lean-action-multiple.outputs.lint-status }}
101+
run: .github/functional_tests/test_helpers/verify_action_output.sh
102+
shell: bash
103+
104+
- name: lake clean
105+
run: lake clean
106+
shell: bash
107+
108+
- name: configure script for empty args test (lake flags)
109+
run: |
110+
sed 's/@EXPECTED_ARGS@/([] : List String)/' lint_script.template > lakefile.lean
111+
shell: bash
112+
113+
- name: "run `lean-action` with lake flags (not driver args)"
114+
id: lean-action-flags
115+
uses: ./
116+
with:
117+
lint: true
118+
lint-args: "--quiet"
119+
use-github-cache: false
120+
121+
- name: verify `lean-action-flags` outcome success
122+
env:
123+
OUTPUT_NAME: "lean-action-flags.outcome"
124+
EXPECTED_VALUE: "success"
125+
ACTUAL_VALUE: ${{ steps.lean-action-flags.outcome }}
126+
run: .github/functional_tests/test_helpers/verify_action_output.sh
127+
shell: bash
128+
129+
- name: verify lake flag was passed correctly
130+
env:
131+
OUTPUT_NAME: "lint-status (lake flags)"
132+
EXPECTED_VALUE: "SUCCESS"
133+
ACTUAL_VALUE: ${{ steps.lean-action-flags.outputs.lint-status }}
134+
run: .github/functional_tests/test_helpers/verify_action_output.sh
135+
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: 2 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -19,4 +19,5 @@ handle_exit() {
1919

2020
trap handle_exit EXIT
2121

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

0 commit comments

Comments
 (0)