question on module system

Stream: general

[Asei Inoue]

I have two questions

When using the module system, all names become private by default. Does that mean the private modifier no longer has any meaning?

At the moment, the module system is not enabled unless you write module at the beginning of the file. Is there a plan to enable the module system by default in the future?

[Moritz Doll]

If you have a public section then everything not tagged private is public.

[Kim Morrison]

Asei Inoue said:

At the moment, the module system is not enabled unless you write module at the beginning of the file. Is there a plan to enable the module system by default in the future?

Probably, but there are no definite plans here. We haven't yet encouraged anyone downstream of Mathlib to move to the module system yet, but will begin doing so on the next release (when the experimental.module flag will no longer be needed). Once we've had a chance to see how that goes we will start thinking about long term defaults.

[Asei Inoue]

Thank you! my questions are resolved

[Yaël Dillies]

I am personally very eager to try the module system out in my (many) projects!

[Chris Henson]

CSLib has an PR (cslib#243) ready to move to the module system, we are also looking forward to trying it out!

[Chris Henson]

(This is now merged, and with a -5.2% improvement to performance!)