Closed MichaelStollBayreuth closed 1 month ago
A first version of a document explaining how one can (try to) make a Mathlib file build faster. See this Zulip thread.
I have another comment, which is more of a wish "can you also answer this": do you know how I can address output "linting to "?
No idea. I don't even know what the linters do that run by default...
A first version of a document explaining how one can (try to) make a Mathlib file build faster. See this Zulip thread.