RFC(Shake): split public and private imports when shaking

Proposal

There should be a clear standard way to order imports across the community. Since the advent of the module system, we have many ways to sort imports, for example:

import A
public import B
import C

vs

public import B
-- A space here? Don't know!
import A
import C

vs

import A
import C
-- A space here? Don't know!
public import B

The former looks ragged, but has the advantage of being the easiest to edit when privatising or publicising an import, although this is an uncommon operation to perform.

I have the opinion that public and private imports should be separated by a blank line, with the public ones coming first, and sorted alphabetically within each, ie

module

public import A
public import C

import B
import D

I do not yet have an opinion of where meta imports should go. Possibly public meta should go before public non-meta, and private meta before private non-meta?

Indeed, the procedure to reduce imports is to first reduce the public imports, potentially adding more private imports doing so, then reduce the private imports. Within mathlib, the public and private imports usually come from widely different strata (the public ones being much earlier ), so it basically never happens that you privatise an existing public import, except when you're trying to reduce imports (meaning that a PR diff should basically never contain some pure unprivatising).

I suggest this is soft-enforced as the community standard, and in particular that shake by default outputs imports in this format.

The user experience will be improved by making import statements more readable and grouping the imports of similar depth together, as welll as by reducing time wasted by mathlib reviewers pushing forward their own interpretation of what the best way to format imports is.

Beneficiaries will mostly be contributors to large libraries like mathlib.

I don't foresee this change as having a large maintenance cost. One must however spend some time figuring out what the best behavior is when the existing imports aren't sorted and shake is run with an option to preserve the existing imports as much as possible.

Community Feedback

This was discussed on Zulip.

Impact

Add 👍 to issues you consider important. If others benefit from the changes in this proposal being added, please ask them to add 👍 to it.

No files, tests, or entry points are named; start by reading the proposal and its linked Zulip discussion to understand the intended Shake behavior. Done means establishing the handling of public, private, and meta imports, including behavior when preserving existing imports, then implementing the proposed default format.