Merge conflicts now

Stream: mathlib4

[Martin Dvořák]

Why do all PRs have merge conflicts now?

[Johan Commelin]

Because we just merged the module system change into master

[Johan Commelin]

Although it doesn't seem to have affected the #queue that much

[Nailin Guan]

How should I shift to the module system? Any written down instructions?

[Rémy Degenne]

There will be an announcement about it soon.

[Nailin Guan]

Just to confirm, adding module infront of imports then use public import replacing import should work?

[Michael Rothgang]

If it compiles, that good enough for now. (In the future, we may decide to switch to more fine-grained imports. That will be a separate policy change and announcement.)

[Nailin Guan]

Cache has nothing usable, so I have no idea whether it compile...

[Riccardo Brasca]

It will surely take some time to rebuild all the PRs, so just be patient

[Kim Morrison]

There's some information and links available at #mathlib4 > Mathlib has moved to the new module system now.

But yes, every file needs to start with module (most of Mathlib now does), and the first step to getting something working is changing every import to public import. After that, if you have a new file, try adding @[expose] public section at the top of the file (like most of Mathlib right now).

[Kim Morrison]

There's no need for now to "get the imports right", i.e. to avoid using public where possible, etc. We will have tooling soon that will help with this.

[Kenny Lau]

Could I have a short explanation of what all three of those magic formulas mean? (1. module, 2. public import, 3. expose public section)

[Michael Rothgang]

The documentation linked in the announcement explains it well. If you don't want to ignore these magic words, the simplest way is to just read that.

[Michael Rothgang]

In short: the module keyword says this file uses the module system (now mandatory within mathlib); the others allow mathlib to adapt the module system with minimal changes (and will, perhaps, go away in the long term).

[Nailin Guan]

Maybe not an appropriate place, but can we have this kind of big shift in announce priorior to the change itself? Also is it possible to to have auto fix for these kind of updates for PR?