PR summary 94cc620d6d

Import changes for modified files

No significant changes to the import graph

Declarations diff

No declarations were harmed in the making of this PR! 🐙

## 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.

./scripts/technical-debt-metrics.sh pr_summary

I'm going to assume that this is not good

Thanks for the quick fix! The new code looks plausible. I'd like to test that it really works, and pushed an intentional error.
Once CI comes back with an error, this is good to me (i.e., reverting the error, waiting for the dependent PR to land, with the fix there picked up). Assuming no surprises:
maintainer delegate

🚀 Pull request has been placed on the maintainer queue by grunweg.

That was fast. I think the check-mark is mis-leading, as the "build" job hasn't been run yet.
If it passes, that is indeed bad (and in that case, please ask for re-review once you found a fix).

It fails 🎉

In other words: I think this is "good to go", once the above things are done.

Actually, there is one last detail I just remembered: not any natural number is a valid exit code. lint-style.lean has code for this, which you can crib from. (The fix flag is not relevant here, variables are named differently etc.):

  -- If run with the `--fix` argument, return a zero exit code.
  -- Otherwise, make sure to return an exit code of at most 125,
  -- so this return value can be used further in shell scripts.
  if args.hasFlag "fix" then
    return 0
  else return min numberErrors 125

Thanks for testing (and resolving) so quickly!

(For the record, since the test commit has disappeared from this PR branch due to a force-push, here's a link to the log of the workflow failing: https://github.com/leanprover-community/mathlib4/actions/runs/12695129220/job/35386640197#step:19:8)

This is ready-to-go as far as I'm concerned too now.

bors merge

Pull request successfully merged into master.

Build succeeded:

• Lint style
• Build