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

test: autolabel D #17168

Closed
wants to merge 55 commits into from
Closed

test: autolabel D #17168

wants to merge 55 commits into from

Conversation

joneugster
Copy link
Collaborator

Open in Gitpod

adomani and others added 30 commits August 18, 2024 17:27
@adomani
feat: add autolabelling of PRs
6536d53
@adomani
fix test
64fdaad
@adomani @jcommelin
Update Mathlib/Tactic/Autolabels/EnvExtension.lean
7a1df6e 
Co-authored-by: Johan Commelin <[email protected]>
@adomani
Comments to address Jon's review
2a9d807
@adomani
Merge remote-tracking branch 'origin/master' into adomani/autolabels_…
a7f9140 
…in_lean
@adomani
update deprecations, use simple extension, sort output
8869066
@adomani
remove cache get step
e6872d2
@adomani
use tee
c93053b
@adomani
remove clutter
f8fbcd3
@adomani
fix
5b7e9c4
@joneugster
reimplementation
5db3a3b
@joneugster
add gh functionality
935552e
@joneugster
add env
0ec6a5b
@joneugster
debug
d22a5b5
@joneugster
fix
2514dee
@joneugster
what's the checkout dance
039e3b9
@joneugster
debug
58ec715
@joneugster
fix
2b37c61
@joneugster
simplify logic
387eaf2
@joneugster
cleanup workflow
c7331a0
@joneugster
delete old approach
468e4d9
@joneugster
doc
91a3909
@joneugster
use 'gh pr'
52027f1
@joneugster
fix label mapping
7daf92f
@joneugster
code review by adomani
6e1520e
@joneugster
code review by grunweg
11323cd
@joneugster
unicode fun
5ebde10
@joneugster
error on multiple arguments
8a87f44
@joneugster
adding tests; incorporating feedback
2a9a253
@joneugster
implement autodetection of folder name
703923a
joneugster and others added 19 commits September 24, 2024 19:29
@joneugster
test workflow failure
d282ed6
@joneugster
undo test
b0d8c74
@joneugster
add test ensuring all content folders are covered
f858411
@joneugster
move test to executable call
2334e69
@joneugster
test
46c4c05
@joneugster
undo tests
87b7b0a
@joneugster
remove action triggering on push
31030f0
@joneugster
cleanup
dc82420
@joneugster @adomani
Update scripts/autolabel.lean
f82c300 
Co-authored-by: damiano <[email protected]>
@joneugster
turn error/warnings into github annotations
d38a6a2
@joneugster
fix
b039a37
@joneugster
remove workflow_dispatch
382dd5d
@joneugster
update documentation about requiring gh
47588c7
@joneugster @adomani
update "CI" label definiton
66f4bee 
Co-authored-by: damiano <[email protected]>
@joneugster @adomani
Apply suggestions from code review
d2da3fe 
Co-authored-by: damiano <[email protected]>
@joneugster @bryangingechen
Apply suggestions from code review
0a8735f 
Co-authored-by: Bryan Gin-ge Chen <[email protected]>
@joneugster
update line number of github annotations
dd53deb
@joneugster
update github annotations
516f65c
@joneugster
fixes
ba612b1
@mergify Mergify
Copy link

mergify bot commented Sep 26, 2024

⚠️ The sha of the head commit of this PR conflicts with #17062. Mergify cannot evaluate rules on this PR. ⚠️

@github-actions GitHub Actions
Copy link

github-actions bot commented Sep 26, 2024 •
edited
Loading

PR summary 7ded21e4d8

Import changes for modified files

No significant changes to the import graph

Import changes for all files
Files Import difference

Declarations diff

+ Label
+ _root_.System.FilePath.isPrefixOf
+ getMatchingLabels
+ githubAnnotation
+ mathlibLabels
+ mathlibUnlabelled

You can run this locally as follows 
## summary with just the declaration names:
./scripts/declarations_diff.sh <optional_commit>

## more verbose report:
./scripts/declarations_diff.sh long <optional_commit>

The doc-module for script/declarations_diff.sh contains some details about this script.

@github-actions github-actions bot added the CI Modifies the continuous integration / deployment setup label Sep 26, 2024
@joneugster joneugster mentioned this pull request Sep 26, 2024
Closed
1 task
@mergify Mergify
Copy link

mergify bot commented Sep 26, 2024

⚠️ The sha of the head commit of this PR conflicts with #17062. Mergify cannot evaluate rules on this PR. ⚠️

@mergify Mergify
Copy link

mergify bot commented Sep 26, 2024

⚠️ The sha of the head commit of this PR conflicts with #17062. Mergify cannot evaluate rules on this PR. ⚠️

@joneugster joneugster closed this Sep 26, 2024
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Reviewers
No reviews
Assignees
No one assigned
Labels
CI Modifies the continuous integration / deployment setup
Projects
None yet
Milestone
No milestone
Development

Successfully merging this pull request may close these issues.
2 participants
@joneugster @adomani