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.

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

feat: rewrite update-style-exceptions.sh as a Lean executable #13245

Closed
wants to merge 5 commits into from
Closed
Show file tree
Hide file tree
Changes from all commits
Commits
File filter

Filter by extension

Filter by extension


Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
2 changes: 1 addition & 1 deletion .github/workflows/nolints.yml
Original file line number Diff line number Diff line change
Expand Up @@ -57,7 +57,7 @@ jobs:
shell: bash
run: |
env LEAN_ABORT_ON_PANIC=1 lake exe runLinter --update Mathlib
./scripts/update-style-exceptions.sh
lake exe update_style_exceptions

- name: configure git setup
run: |
Expand Down
4 changes: 4 additions & 0 deletions lakefile.lean
Original file line number Diff line number Diff line change
Expand Up @@ -68,6 +68,10 @@ lean_exe shake where
root := `Shake.Main
supportInterpreter := true

/-- `lake exe update_style_exceptions` updates the style exceptions file. -/
lean_exe update_style_exceptions where
srcDir := "scripts"

/--
`lake exe pole` queries the Mathlib speedcenter for build times for the current commit,
and then calculates the longest pole
Expand Down
40 changes: 40 additions & 0 deletions scripts/update_style_exceptions.lean
Original file line number Diff line number Diff line change
@@ -0,0 +1,40 @@
/-
Copyright (c) 2024 Michael Rothgang. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Authors: Michael Rothgang
-/

import Mathlib.Util.GetAllModules

/-!
# Style exception file generator

This script completely regenerates the `scripts/style-exceptions.txt` file.
Typically this should only be run by automation. Human contributors shouldn't need to run this
unless they are making changes to the linting script.
-/

/-- The entry point to the `lake exe update_style_exceptions` command.
Regenerate the `scripts/style-exceptions.txt` file. -/
def main : IO UInt32 := do
-- Find all files in the mathlib, archive and counterexamples directories.
let mut allFiles ← getAllFiles false "Mathlib"
let archive ← getAllFiles false "Archive"
let cex ← getAllFiles false "Counterexamples"
allFiles := (allFiles.append archive).append cex
-- Run the linter on all of them; gather the resulting exceptions and sort them.
-- Call xargs, to avoid spawning a new python process for each file.
-- `IO.Process.output` passes empty standard input, so this actually works.
-- `-s` specifies the maximum size of the command line (including the initial argument):
-- since we pass all input files as initial arguments to xargs, this small hack is necessary.
-- As of May 2024, the limit 200 000 suffices; therefore, we pass 300 000 to be future-proof.
let args := #["-s", "300000", "./scripts/lint-style.py"].append
(allFiles.map System.FilePath.toString)
let out ← IO.Process.output { cmd := "xargs", args := args }
if out.exitCode != 0 then
println! "error {out.exitCode} on updating style exceptions : {out.stderr}"
return out.exitCode
let lines := out.stdout.splitOn "\n"
let final := "\n".intercalate (lines.toArray.qsort (· < ·)).toList
Copy link
Collaborator Author

Choose a reason for hiding this comment

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

I'm not too happy about the list->array->list conversion: this is because

  • splitOn returns a List String
  • qsort requires an Array to sort
  • intercalate requires a List String again

Suggestions for avoiding this as welcome. It seems this difference isn't important for speed; this is purely an aesthetic thing.

IO.FS.writeFile (System.mkFilePath ["scripts", "style-exceptions.txt"]) final
return 0
Loading