Skip to content

Commit 85028a6

Browse files
joneugsterjoneugster
committed
refactor(scripts/autolabel): use type-safe labels instead of strings (leanprover-community#34949)
Change from freeform string label names to an inductive type. This is intended to prevent miss-spellings of label names, which become more likely when label dependencies will be introduced in leanprover-community#34066. This is a pure refactor without change in functionality.
1 parent 604007f commit 85028a6

1 file changed

Lines changed: 171 additions & 82 deletions

File tree

‎scripts/autolabel.lean‎

Lines changed: 171 additions & 82 deletions
Original file line numberDiff line numberDiff line change
@@ -55,98 +55,185 @@ open Lean System
5555

5656
namespace AutoLabel
5757

58+
/-- Mathlib's Github topic labels -/
59+
inductive Label where
60+
| «t-algebra»
61+
| «t-algebraic-geometry»
62+
| «t-algebraic-topology»
63+
| «t-analysis»
64+
| «t-category-theory»
65+
| «t-combinatorics»
66+
| «t-computability»
67+
| «t-condensed»
68+
| «t-convex-geometry»
69+
| «t-data»
70+
| «t-differential-geometry»
71+
| «t-dynamics»
72+
| «t-euclidean-geometry»
73+
| «t-geometric-group-theory»
74+
| «t-group-theory»
75+
| «t-linter»
76+
| «t-logic»
77+
| «t-measure-probability»
78+
| «t-meta»
79+
| «t-number-theory»
80+
| «t-order»
81+
| «t-ring-theory»
82+
| «t-set-theory»
83+
| «t-topology»
84+
| «CI»
85+
| «dependency-bump»
86+
| «IMO»
87+
deriving BEq, Hashable, Repr
88+
89+
/-- Array of all topic labels which are used in Mathlib -/
90+
def mathlibLabels : Array Label := #[
91+
.«t-algebra», .«t-algebraic-geometry», .«t-algebraic-topology», .«t-analysis»,
92+
.«t-category-theory», .«t-combinatorics», .«t-computability», .«t-condensed»,
93+
.«t-convex-geometry», .«t-data», .«t-differential-geometry», .«t-dynamics»,
94+
.«t-euclidean-geometry», .«t-geometric-group-theory», .«t-group-theory», .«t-linter»,
95+
.«t-logic», .«t-measure-probability», .«t-meta», .«t-number-theory», .«t-order»,
96+
.«t-ring-theory», .«t-set-theory», .«t-topology», .«CI», .«dependency-bump», .«IMO»
97+
]
98+
99+
def Label.toString : Label → String
100+
| .«t-algebra» => "t-algebra"
101+
| .«t-algebraic-geometry» => "t-algebraic-geometry"
102+
| .«t-algebraic-topology» => "t-algebraic-topology"
103+
| .«t-analysis» => "t-analysis"
104+
| .«t-category-theory» => "t-category-theory"
105+
| .«t-combinatorics» => "t-combinatorics"
106+
| .«t-computability» => "t-computability"
107+
| .«t-condensed» => "t-condensed"
108+
| .«t-convex-geometry» => "t-convex-geometry"
109+
| .«t-data» => "t-data"
110+
| .«t-differential-geometry» => "t-differential-geometry"
111+
| .«t-dynamics» => "t-dynamics"
112+
| .«t-euclidean-geometry» => "t-euclidean-geometry"
113+
| .«t-geometric-group-theory» => "t-geometric-group-theory"
114+
| .«t-group-theory» => "t-group-theory"
115+
| .«t-linter» => "t-linter"
116+
| .«t-logic» => "t-logic"
117+
| .«t-measure-probability» => "t-measure-probability"
118+
| .«t-meta» => "t-meta"
119+
| .«t-number-theory» => "t-number-theory"
120+
| .«t-order» => "t-order"
121+
| .«t-ring-theory» => "t-ring-theory"
122+
| .«t-set-theory» => "t-set-theory"
123+
| .«t-topology» => "t-topology"
124+
| .«CI» => "CI"
125+
| .«IMO» => "IMO"
126+
| .«dependency-bump» => "dependency-bump"
127+
128+
instance : ToString Label where
129+
toString := Label.toString
130+
131+
-- test to ensure all labels are listed in `mathlibLabels`
132+
open Lean in
133+
run_cmd
134+
let some (.inductInfo labels) := (← getEnv).find? ``Label | unreachable!
135+
let labelNames := labels.ctors.filterMap (·.components.getLast?) |>.toArray
136+
let some (.defnInfo dinfo) := (← getEnv).find? ``mathlibLabels | unreachable!
137+
let allConstants := dinfo.value.getUsedConstants
138+
let constants := allConstants.filterMap fun n =>
139+
if n.components.dropLast.getLast? == some `Label then n.components.getLast? else none
140+
if labelNames != constants then
141+
let mut out : List String := []
142+
for (a, b) in labelNames.zip constants do
143+
if a != b then
144+
out := s!"expexcted {a} got {b}" :: out
145+
logWarning m!"The available Labels is out of sync with the labels listed in \
146+
{ .ofConstName ``mathlibLabels }.\n\
147+
Please keep them sorted and in sync!\n{"\n".intercalate out.reverse}"
148+
58149
/--
59-
A `Label` consists of the
60-
* The `label` field is the actual GitHub label name.
150+
A `LabelData` consists of the
61151
* The `dirs` field is the array of all "root paths" such that a modification in a file contained
62152
in one of these paths should be labelled with `label`.
63153
* The `exclusions` field is the array of all "root paths" that are excluded, among the
64154
ones that start with the ones in `dirs`.
65155
Any modifications to a file in an excluded path is ignored for the purposes of labelling.
156+
* The `dependencies` field is the array of all labels, which are lower in the import hierarchy
157+
and which should be excluded if the label is present.
66158
-/
67-
structure Label where
68-
/-- The label name as it appears on GitHub -/
69-
label : String
159+
structure LabelData (label : Label) where
70160
/-- Array of paths which fall under this label. e.g. `"Mathlib" / "Algebra"`.
71161
72162
For a label of the form `t-set-theory` this defaults to `#["Mathlib" / "SetTheory"]`. -/
73-
dirs : Array FilePath := if label.startsWith "t-" then
74-
#["Mathlib" / ("".intercalate (label.splitOn "-" |>.drop 1 |>.map .capitalize))]
163+
dirs : Array FilePath := if label.toString.startsWith "t-" then
164+
#["Mathlib" / ("".intercalate (label.toString.splitOn "-" |>.drop 1 |>.map .capitalize))]
75165
else #[]
76166
/-- Array of paths which should be excluded.
77167
Any modifications to a file in an excluded path are ignored for the purposes of labelling. -/
78168
exclusions : Array FilePath := #[]
79169
deriving BEq, Hashable
80170

81-
/--
82-
Mathlib labels and their corresponding folders. Add new labels and folders here!
83-
-/
84-
def mathlibLabels : Array Label := #[
85-
{ label := "t-algebra",
171+
/-- Mathlib labels and their corresponding folders -/
172+
def mathlibLabelData : (l : Label) → LabelData l
173+
| .«t-algebra» => {
86174
dirs := #[
87175
"Mathlib" / "Algebra",
88176
"Mathlib" / "FieldTheory",
89177
"Mathlib" / "RepresentationTheory",
90-
"Mathlib" / "LinearAlgebra"] },
91-
{ label := "t-algebraic-geometry",
178+
"Mathlib" / "LinearAlgebra"] }
179+
| .«t-algebraic-geometry» => {
92180
dirs := #[
93181
"Mathlib" / "AlgebraicGeometry",
94-
"Mathlib" / "Geometry" / "RingedSpace"] },
95-
{ label := "t-algebraic-topology",
96-
dirs := #["Mathlib" / "AlgebraicTopology"] },
97-
{ label := "t-analysis" },
98-
{ label := "t-category-theory" },
99-
{ label := "t-combinatorics" },
100-
{ label := "t-computability" },
101-
{ label := "t-condensed" },
102-
{ label := "t-convex-geometry",
103-
dirs := #["Mathlib" / "Geometry" / "Convex"] },
104-
{ label := "t-data"
182+
"Mathlib" / "Geometry" / "RingedSpace"] }
183+
| .«t-algebraic-topology» => {}
184+
| .«t-analysis» => {}
185+
| .«t-category-theory» => {}
186+
| .«t-combinatorics» => {}
187+
| .«t-computability» => {}
188+
| .«t-condensed» => {}
189+
| .«t-convex-geometry» => {
190+
dirs := #["Mathlib" / "Geometry" / "Convex"] }
191+
| .«t-data» => {
105192
dirs := #[
106193
"Mathlib" / "Control",
107-
"Mathlib" / "Data",] },
108-
{ label := "t-differential-geometry",
109-
dirs := #["Mathlib" / "Geometry" / "Manifold"] },
110-
{ label := "t-dynamics" },
111-
{ label := "t-euclidean-geometry",
112-
dirs := #["Mathlib" / "Geometry" / "Euclidean"] },
113-
{ label := "t-geometric-group-theory",
114-
dirs := #["Mathlib" / "Geometry" / "Group"] },
115-
{ label := "t-group-theory",
116-
dirs := #["Mathlib" / "GroupTheory"] },
117-
{ label := "t-linter",
194+
"Mathlib" / "Data"] }
195+
| .«t-differential-geometry» => {
196+
dirs := #["Mathlib" / "Geometry" / "Manifold"] }
197+
| .«t-dynamics» => {}
198+
| .«t-euclidean-geometry» => {
199+
dirs := #["Mathlib" / "Geometry" / "Euclidean"] }
200+
| .«t-geometric-group-theory» => {
201+
dirs := #["Mathlib" / "Geometry" / "Group"] }
202+
| .«t-group-theory» => {}
203+
| .«t-linter» => {
118204
dirs := #[
119205
"Mathlib" / "Tactic" / "Linter",
120206
"scripts" / "lint-style.lean",
121207
"scripts" / "lint-style.py",
122-
] },
123-
{ label := "t-logic",
208+
] }
209+
| .«t-logic» => {
124210
dirs := #[
125211
"Mathlib" / "Logic",
126-
"Mathlib" / "ModelTheory"] },
127-
{ label := "t-measure-probability",
212+
"Mathlib" / "ModelTheory"] }
213+
| .«t-measure-probability» => {
128214
dirs := #[
129215
"Mathlib" / "MeasureTheory",
130216
"Mathlib" / "Probability",
131-
"Mathlib" / "InformationTheory"] },
132-
{ label := "t-meta",
217+
"Mathlib" / "InformationTheory"] }
218+
| .«t-meta» => {
133219
dirs := #[
134220
"Mathlib" / "Lean",
135221
"Mathlib" / "Mathport",
136222
"Mathlib" / "Tactic",
137223
"Mathlib" / "Util"],
138-
exclusions := #["Mathlib" / "Tactic" / "Linter"] },
139-
{ label := "t-number-theory" },
140-
{ label := "t-order" },
141-
{ label := "t-ring-theory",
142-
dirs := #["Mathlib" / "RingTheory"] },
143-
{ label := "t-set-theory" },
144-
{ label := "t-topology",
145-
dirs := #["Mathlib" / "Topology"] },
146-
{ label := "CI",
224+
exclusions := #["Mathlib" / "Tactic" / "Linter"] }
225+
| .«t-number-theory» => {}
226+
| .«t-order» => {}
227+
| .«t-ring-theory» => {}
228+
| .«t-set-theory» => {}
229+
| .«t-topology» => {}
230+
| .«CI» => {
147231
dirs := #[
148232
".github",
149233
"scripts",
234+
"scripts" / "nolints.json",
235+
"scripts" / "nolints-style.txt",
236+
"scripts" / "nolints_prime_decls.txt",
150237
],
151238
exclusions := #[
152239
"scripts" / "lint-style.lean",
@@ -155,11 +242,11 @@ def mathlibLabels : Array Label := #[
155242
"scripts" / "nolints.json",
156243
"scripts" / "nolints-style.txt",
157244
"scripts" / "nolints_prime_decls.txt",
158-
] },
159-
{ label := "IMO",
160-
dirs := #["Archive" / "Imo"] },
161-
{ label := "dependency-bump",
162-
dirs := #["lake-manifest.json"] } ]
245+
] }
246+
| .«IMO» => {
247+
dirs := #["Archive" / "Imo"] }
248+
| .«dependency-bump» => {
249+
dirs := #["lake-manifest.json"] }
163250

164251
/-- Exceptions inside `Mathlib/` which are not covered by any label. -/
165252
def mathlibUnlabelled : Array FilePath := #[
@@ -174,20 +261,21 @@ def _root_.System.FilePath.isPrefixOf (dir path : FilePath) : Bool :=
174261
(dir / "").normalize.toString.isPrefixOf (path / "").normalize.toString
175262

176263
/--
177-
Return all names of labels in `mathlibLabels` which match
264+
Return all labels in `mathlibLabels` which match
178265
at least one of the `files`.
179266
180267
* `files`: array of relative paths starting from the mathlib root directory.
181268
-/
182-
def getMatchingLabels (files : Array FilePath) : Array String :=
269+
def getMatchingLabels (files : Array FilePath) : Array Label :=
183270
let applicable := mathlibLabels.filter fun label ↦
184271
-- first exclude all files the label excludes,
185272
-- then see if any file remains included by the label
273+
let data := mathlibLabelData label
186274
let notExcludedFiles := files.filter fun file ↦
187-
label.exclusions.all (!·.isPrefixOf file)
188-
label.dirs.any (fun dir ↦ notExcludedFiles.any (dir.isPrefixOf ·))
189-
-- return sorted list of label names
190-
applicable.map (·.label) |>.qsort (· < ·)
275+
data.exclusions.all (!·.isPrefixOf file)
276+
data.dirs.any (fun dir ↦ notExcludedFiles.any (dir.isPrefixOf ·))
277+
-- return sorted list of labels
278+
applicable |>.qsort (·.toString < ·.toString)
191279

192280
/-!
193281
Testing the functionality of the declarations defined in this script
@@ -202,22 +290,22 @@ section Tests
202290

203291
#guard getMatchingLabels #[] == #[]
204292
-- Test default value for `label.dirs` works
205-
#guard getMatchingLabels #["Mathlib" / "SetTheory" / "ZFC"] == #["t-set-theory"]
293+
#guard getMatchingLabels #["Mathlib" / "SetTheory" / "ZFC"] == #[.«t-set-theory»]
206294
-- Test exclusion
207-
#guard getMatchingLabels #["Mathlib" / "Tactic"/ "Abel.lean"] == #["t-meta"]
208-
#guard getMatchingLabels #["Mathlib" / "Tactic"/ "Linter" / "Lint.lean"] == #["t-linter"]
295+
#guard getMatchingLabels #["Mathlib" / "Tactic"/ "Abel.lean"] == #[.«t-meta»]
296+
#guard getMatchingLabels #["Mathlib" / "Tactic"/ "Linter" / "Lint.lean"] == #[.«t-linter»]
209297
#guard getMatchingLabels #[
210298
"Mathlib" / "Tactic"/ "Linter" / "Lint.lean",
211-
"Mathlib" / "Tactic" / "Abel.lean" ] == #["t-linter", "t-meta"]
299+
"Mathlib" / "Tactic" / "Abel.lean" ] == #[.«t-linter», .«t-meta»]
212300

213301
-- Test targeting a file instead of a directory
214-
#guard getMatchingLabels #["lake-manifest.json"] == #["dependency-bump"]
302+
#guard getMatchingLabels #["lake-manifest.json"] == #[.«dependency-bump»]
215303

216304
-- Test linting of specific changes touching linting and CI.
217-
#guard getMatchingLabels #["scripts" / "add_deprecations.sh"] == #["CI"]
218-
#guard getMatchingLabels #["scripts" / "lint-style.lean"] == #["t-linter"]
305+
#guard getMatchingLabels #["scripts" / "add_deprecations.sh"] == #[.«CI»]
306+
#guard getMatchingLabels #["scripts" / "lint-style.lean"] == #[.«t-linter»]
219307
#guard getMatchingLabels #["Mathlib" / "Tactic" / "Linter" / "TextBased.lean",
220-
"scripts" / "lint-style.lean", "scripts" / "lint-style.py"] == #["t-linter"]
308+
"scripts" / "lint-style.lean", "scripts" / "lint-style.py"] == #[.«t-linter»]
221309
#guard getMatchingLabels #["scripts" / "noshake.json"] == #[]
222310

223311
/-- Testing function to ensure the labels defined in `mathlibLabels` cover all
@@ -282,24 +370,25 @@ unsafe def main (args : List String): IO UInt32 := do
282370
return 1
283371
let prNumber? := args[0]?
284372

285-
-- test: validate that all paths in `mathlibLabels` actually exist
373+
-- test: validate that all paths in `mathlibLabelData` actually exist
286374
let mut valid := true
287375
for label in mathlibLabels do
288-
for dir in label.dirs do
376+
let data := mathlibLabelData label
377+
for dir in data.dirs do
289378
unless ← FilePath.pathExists dir do
290379
-- print github annotation error
291380
println <| AutoLabel.githubAnnotation "error" "scripts/autolabel.lean"
292-
s!"Misformatted `{ ``AutoLabel.mathlibLabels }`"
293-
s!"directory '{dir}' does not exist but is included by label '{label.label}'. \
294-
Please update `{ ``AutoLabel.mathlibLabels }`!"
381+
s!"Misformatted `{ ``AutoLabel.mathlibLabelData }`"
382+
s!"directory '{dir}' does not exist but is included by label '{label}'. \
383+
Please update `{ ``AutoLabel.mathlibLabelData }`!"
295384
valid := false
296-
for dir in label.exclusions do
385+
for dir in data.exclusions do
297386
unless ← FilePath.pathExists dir do
298387
-- print github annotation error
299388
println <| AutoLabel.githubAnnotation "error" "scripts/autolabel.lean"
300-
s!"Misformatted `{ ``AutoLabel.mathlibLabels }`"
301-
s!"directory '{dir}' does not exist but is excluded by label '{label.label}'. \
302-
Please update `{ ``AutoLabel.mathlibLabels }`!"
389+
s!"Misformatted `{ ``AutoLabel.mathlibLabelData }`"
390+
s!"directory '{dir}' does not exist but is excluded by label '{label}'. \
391+
Please update `{ ``AutoLabel.mathlibLabelData }`!"
303392
valid := false
304393
unless valid do
305394
return 2
@@ -311,7 +400,7 @@ unsafe def main (args : List String): IO UInt32 := do
311400
-- note: only emitting a warning because the workflow is only triggered on the first commit
312401
-- of a PR and could therefore lead to unexpected behaviour if a folder was created later.
313402
println <| AutoLabel.githubAnnotation "warning" "scripts/autolabel.lean"
314-
s!"Incomplete `{ ``AutoLabel.mathlibLabels }`"
403+
s!"Incomplete `{ ``AutoLabel.mathlibLabelData }`"
315404
s!"the following paths inside `Mathlib/` are not covered \
316405
by any label: {notMatchedPaths} Please modify `AutoLabel.mathlibLabels` accordingly!"
317406
-- return 3
@@ -339,12 +428,12 @@ unsafe def main (args : List String): IO UInt32 := do
339428
cmd := "gh"
340429
args := #["pr", "view", n, "--json", "labels", "--jq", ".labels .[] .name"]}
341430
let labels := labelsPresent.splitToList (· == '\n')
342-
let autoLabels := mathlibLabels.map (·.label)
431+
let autoLabels := mathlibLabels.map (·.toString)
343432
match labels.filter autoLabels.contains with
344433
| [] => -- if the PR does not have a label that this script could add, then we add a label
345434
let _ ← IO.Process.run {
346435
cmd := "gh",
347-
args := #["pr", "edit", n, "--add-label", label] }
436+
args := #["pr", "edit", n, "--add-label", label.toString] }
348437
println s!"::notice::added label: {label}"
349438
| t_labels_already_present =>
350439
println s!"::notice::Did not add label '{label}', since {t_labels_already_present} \

0 commit comments

Comments
 (0)