testing of Cslib.lean and Cslib.Init

Stream: CSLib

[Chris Henson]

Thanks to @Jesse Alama, we now have testing in place around our imports. Here is a brief summary of what folks should be aware of:

• There is now a Cslib.Init module, similar to (and including) Mathlib.Init which you should always have imported. CI will now check transitive imports for this.
• CI now runs lake exe mk_all --check, ensuring that Cslib.lean and CslibTests.lean have all imports

Some more details: a primary motivation for Cslib.Init is to ensure that linters (ours and Mathlib's) are available everywhere. Currently there some files that are unable to import Cslib.Init due to compatibility issues with Mathlib. These are marked as an exception here and have open issues cslib#138, cslib#139, and cslib#140.

[Fabrizio Montesi]

Thanks @Jesse Alama :)

[Jesse Alama]

Fabrizio Montesi said:

Thanks Jesse Alama :)

My pleasure! CSLib is a very exciting initative; happy to be involved.