feat: move to the module system

[chenson2018]

Closes #172. This PR moves CSLib to the module system, mostly following Mathlib's pattern of using @[expose] public section liberally for the simplest transition. This removes a few uses of private that conflicted:

• LTS.noε
• the HasTau instance in Cslib.Computability.Automata.EpsilonNA.Basic
• grind lemmas about ReductionSystem
• FinFun.fromFun

I also think it might be less confusing if we move some meta sections to their own files, but will leave this for a future PR.

[chenson2018]

For the moment I have moved lake exe mk_all --check --module into its own step, because lean-action does not yet have a parameter for this. (I can make a PR for this later, but don't want it to hold up this one)

[chenson2018]

I have also removed the shake step, as my understanding is that this is not yet compatible with the module system. (Though I think we can still encourage people to use #min_imports until the replacement is in effect.)

[arademaker]

I have also removed the shake step, as my understanding is that this is not yet compatible with the module system. (Though I think we can still encourage people to use #min_imports until the replacement is in effect.)

This is confusing to me. In one of Lean office hours, @Kha mentioned a version of Shake compatible with the new module system. Here I am using a particular version that @Kha mentioned and I copied to this repo. But I now seens to be moved to https://github.com/leanprover/lean4/blob/master/src/lake/Lake/CLI/Shake.lean.

[chenson2018]

My understanding is that this will be available downstream in the next release candidate (and currently in nightly testing), now accessed directly via lake shake. As soon as this happens, I will restore this step in CI.