weak in lakefile

Stream: CSLib

[Chris Henson]

Following some revisited discussion in #general > weak.linter.mathlibStandardSet and lint-style-action, I am questioning the use of weak in our lakefile.

The problem is that this opens us to the possibility of files not depending on Mathlib being silently not linted. I identified such a case and opened and cslib#113. The alternative is to remove the weak from our options, which would enforce that all files must import Mathlib.Init for linters (transitively or directly). The tradeoffs here seem to be removing the chance of accidental non-linting in exchange for a dependency.

[Chris Henson]

Also with talk of writing linters (see #CSLib > namespacing), it seems like we might end up with an equivalent Cslib.Init anyway? If this imports Mathlib.Init, it seems reasonable to drop the weak and require importing this.

[Fabrizio Montesi]

Having our own Cslib.Init looks like the right choice to me. It can just be an import Mathlib.Init for now.