Skip to content

perf(ci): reuse the prepared environment for style linting - #1014

Closed
SamuelSchlesinger wants to merge 2 commits into
leanprover:mainfrom
SamuelSchlesinger:samschles/ci-reuse-style-environment
Closed

SamuelSchlesinger wants to merge 2 commits into
leanprover:mainfrom
SamuelSchlesinger:samschles/ci-reuse-style-environment

Conversation

@SamuelSchlesinger

Copy link
Copy Markdown
Collaborator

Run lake exe lint-style in the prepared checkout, preserving all existing checks while avoiding redundant checkout and dependency setup.

Codex assisted with the workflow edit and validation.

Retain the pinned case-sensitivity and ignored-file actions and the executable-bit check from lint-style-action, running them before Lean restores dependencies. Run lake exe lint-style in the existing checkout to avoid deleting dependencies and repeating setup.

Validated with actionlint 1.7.12, source-file checks, lake exe lint-style, and git diff --check. No Lean sources or other CI gates change.
@SamuelSchlesinger

Copy link
Copy Markdown
Collaborator Author

For context for onlookers, I maintain a very large Lean formalization and I've got a few tricks over there to lower the CI time in GitHub actions, so I am seeing what might apply to CSLib as well.

@SamuelSchlesinger

Copy link
Copy Markdown
Collaborator Author

CI is green! Style checks took ~7s here versus 113s on the base commit, including the preserved file checks. The full job finished in 3m10s.

@SamuelSchlesinger
SamuelSchlesinger marked this pull request as ready for review October 1, 2026 15:04
@SamuelSchlesinger

Copy link
Copy Markdown
Collaborator Author

@jessealama I wonder what you think of this, or if you have a better way to do it.

@chenson2018

Copy link
Copy Markdown
Collaborator

This part of CI has been a thorn in my side for some time because of how slow it is. It should be completely removed once the autoformatter lands (and I wouldn't mind even anticipating this change). Otherwise I'm fine with any non-breaking change that is faster.

@SamuelSchlesinger

Copy link
Copy Markdown
Collaborator Author

@chenson2018 if you want to merge this, I think we can sync with Jesse later.

@chenson2018

Copy link
Copy Markdown
Collaborator

I'd prefer we just go ahead and remove it entirely. Nobody will miss it in the interim.

Comment thread .github/workflows/lean_action_ci.yml Resolved
Co-authored-by: Jesse Alama <jessealama@users.noreply.github.com>
@SamuelSchlesinger

Copy link
Copy Markdown
Collaborator Author

Up to you @chenson2018, feel free to merge or close it.

@chenson2018

Copy link
Copy Markdown
Collaborator

@SamuelSchlesinger I'd rather you merge #1047 :)

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Labels

None yet

Projects

None yet

Development

Successfully merging this pull request may close these issues.

3 participants