chore: bump toolchain to v4.24.0

[kim-em]

No description provided.

[chenson2018]

@kim-em I have changes required staged in another branch for this, give me just a minute.

[kim-em]

Hmm:

% lake exe lint-style
warning: nolints file could not be read; treating as empty: scripts/nolints-style.txt
error: `print-style-error.sh` exited with code 255
could not execute external process './scripts/print-style-errors.sh'
uncaught exception: no such file or directory (error code: 2)
  file: Mathlib.lean

is the local repro for this CI error. Was this ever working? It seems to be a problem in lake exe link-style, provided by Mathlib, which is mistakenly thinking that it is running in Mathlib.

[kim-em]

Hmm:

% lake exe lint-style
warning: nolints file could not be read; treating as empty: scripts/nolints-style.txt
error: `print-style-error.sh` exited with code 255
could not execute external process './scripts/print-style-errors.sh'
uncaught exception: no such file or directory (error code: 2)
  file: Mathlib.lean

is the local repro for this CI error. Was this ever working? It seems to be a problem in lake exe link-style, provided by Mathlib, which is mistakenly thinking that it is running in Mathlib.

Oh, interestingly this is actually two separate, unrelated errors.

error: `print-style-error.sh` exited with code 255
could not execute external process './scripts/print-style-errors.sh'

can be surpressed with weak.linter.pythonStyle = false in the lakefile: the problem is just that it's not even finding the python script to run!

[kim-em]

And the other one with weak.linter.checkInitImports = false.

But then there's one more!

[chenson2018]

Was this ever working?

In other open PRs this job does not have this error, I thought this problem had been fixed after I asked about it in this thread.