Skip to content
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

Jump to bottom

[Merged by Bors] - feat(scripts/lint_mathlib): implement github annotations for mathlib linters #11345

Closed
wants to merge 7 commits into from
Closed

[Merged by Bors] - feat(scripts/lint_mathlib): implement github annotations for mathlib linters #11345

wants to merge 7 commits into from

Conversation

alexjbest
Copy link
Member

@alexjbest alexjbest commented Jan 10, 2022 •
edited

Resolves the last part of #5863

This causes lean --run lint_mathlib --github to produce error messages understood by github actions, which will tag the lines causing linter failures with annotations in the files changed tab

Screen Shot 2022-01-11 at 03 08 49

Open in Gitpod

@alexjbest alexjbest added WIP Work in progress CI This issue or PR is about continuous integration labels Jan 10, 2022
@alexjbest alexjbest added awaiting-CI The author would like to see what CI has to say before doing more work. awaiting-review The author would like community review of the PR and removed WIP Work in progress labels Jan 10, 2022
@alexjbest alexjbest added awaiting-review The author would like community review of the PR and removed awaiting-review The author would like community review of the PR awaiting-CI The author would like to see what CI has to say before doing more work. labels Jan 10, 2022
@alexjbest alexjbest added the awaiting-CI The author would like to see what CI has to say before doing more work. label Jan 10, 2022
@gebner
Copy link
Member

gebner commented Jan 11, 2022

bors d+

@bors
Copy link

bors bot commented Jan 11, 2022

✌️ alexjbest can now approve this pull request. To approve and merge a pull request, simply reply with bors r+. More detailed instructions are available here.

@github-actions github-actions bot added delegated The PR author may merge after reviewing final suggestions. and removed awaiting-review The author would like community review of the PR labels Jan 11, 2022
@alexjbest
Copy link
Member Author

bors r+

@bors
Copy link

bors bot commented Jan 11, 2022

👎 Rejected by label

@alexjbest alexjbest removed the awaiting-CI The author would like to see what CI has to say before doing more work. label Jan 11, 2022
@alexjbest
Copy link
Member Author

bors r+

bors bot pushed a commit that referenced this pull request Jan 11, 2022
@alexjbest
feat(scripts/lint_mathlib): implement github annotations for mathlib …
be4c5aa 
…linters (#11345)

Resolves the last part of #5863

This causes `lean --run lint_mathlib --github` to produce error messages understood by github actions, which will tag the lines causing linter failures with annotations in the files changed tab
@bors
Copy link

bors bot commented Jan 11, 2022

Pull request successfully merged into master.

Build succeeded:

@bors bors bot changed the title feat(scripts/lint_mathlib): implement github annotations for mathlib linters [Merged by Bors] - feat(scripts/lint_mathlib): implement github annotations for mathlib linters Jan 11, 2022
@bors bors bot closed this Jan 11, 2022
@bors bors bot deleted the alexjbest/lint-github branch January 11, 2022 17:12
gebner
gebner reviewed Jan 24, 2022
View reviewed changes
.github/workflows/build.yml
@@ -153,7 +153,7 @@ jobs:
- name: lint
run: |
./scripts/mk_all.sh
lean --run scripts/lint_mathlib.lean
lean --run scripts/lint_mathlib.lean --github
Copy link
Member

Choose a reason for hiding this comment

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

BTW, you changed the wrong file here. There's a big warning on top:

# DO NOT EDIT THIS FILE!!!

# This file is automatically generated by mk_build_yml.sh
# Edit build.yml.in instead and run mk_build_yml.sh to update.

Copy link
Member Author

Choose a reason for hiding this comment

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

Thanks for catching this, I've seen this warning before but totally missed it this time. I'll fix this tonight or tomorrow if nobody beats me to it

Copy link
Collaborator

Choose a reason for hiding this comment

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

@alexjbest it looks like it's fixed in #11645, which I'll put on the queue shortly

Copy link
Member Author

Choose a reason for hiding this comment

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

Great! Do either of you have an easy to implement way to prevent this sort of thing happening again?
E.g. a check in CI that the workflow files are the same as those generated from the .in file? How hard would that be to check?

Copy link
Member

Choose a reason for hiding this comment

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

That shouldn't be too hard. I believe a ./.github/workflows/mk_build_yml.sh && git diff --exit-code .github should do the trick.

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

@gebner gebner gebner left review comments

@robertylewis robertylewis robertylewis left review comments

@bryangingechen bryangingechen bryangingechen left review comments

Assignees
No one assigned
Labels
CI This issue or PR is about continuous integration delegated The PR author may merge after reviewing final suggestions.
Projects
None yet
Milestone
No milestone
Development

Successfully merging this pull request may close these issues.

None yet
4 participants
@alexjbest @gebner @robertylewis @bryangingechen