move to the module system

Stream: CSLib

[Chris Henson]

I have opened cslib#243 moving CSLib to the module system. I mostly followed Mathlib's example of using @[expose] public section which seemed straightforward for a first pass, but would welcome a second look from someone with more experience with modules.

[Sebastian Ullrich]

I haven't looked at the code in detail, but from your description it sounds good to me

[Ching-Tsun Chou]

Is there a tutorial on the new module system? As usual, the Lean language reference is not the easiest thing to read.

[Chris Henson]

@Fabrizio Montesi They are not hard to fix, but every PR that lands before this accumulates merge conflicts, so it would be nice to prioritize this for review.

[Chris Henson]

(I would also like to make sure there's at least one day of nightly testing with this before the release that includes this PR to keep that process smooth)

[Ching-Tsun Chou]

I agree with Chris that we should get this over with ASAP. It impacts all outstanding and future PRs.

[Fabrizio Montesi]

good point, done

[Chris Henson]

Great, thank you! I will follow up soon with a PR re-enabling the new module aware shake and splitting out some meta code into new files. (I felt it was simpler to split this out than try doing everything at once)

[Chris Henson]

As a practical matter, for contributors any PRs in progress should merge main and in any new files you likely want to follow the pattern of files beginning with

module

public import ...

@[expose] public section

As we use the module system further, we will refine what needs to be public and/or exposed.

[Chris Henson]

Also, this gave a nice performance boost!

radar said:

feat: move to the module system (cslib#243)
Large changes (1:check:)

• :check: build//instructions: -94.8G (-5.2%)

[Ching-Tsun Chou]

It seems that lake exe mk_all still generates the old formats for Cslib.lean and CslibTests.lean.

[Chris Henson]

You have to add a --module option now.

[Ching-Tsun Chou]

I see. Thanks!