Skip to content

Conversation

@kim-em
Copy link
Collaborator

@kim-em kim-em commented Oct 14, 2025

No description provided.

@chenson2018
Copy link
Collaborator

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

@kim-em
Copy link
Collaborator Author

kim-em commented Oct 14, 2025

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
Copy link
Collaborator Author

kim-em commented Oct 14, 2025

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
Copy link
Collaborator Author

kim-em commented Oct 14, 2025

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

But then there's one more!

@chenson2018
Copy link
Collaborator

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.

@fmontesi fmontesi merged commit e1fea78 into main Oct 14, 2025
3 checks passed
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Labels

None yet

Projects

None yet

Development

Successfully merging this pull request may close these issues.

4 participants