refactor(*): scrub imports (#17568)
For each file, we read each declaration and find the files containing each referenced declaration. This is the "needed" set. We then replace the imports with
* imports which are needed
* other needed files which would not otherwise be transitively imported
Thus we don't remove any imports merely because they are transitively redundant. Instead we remove imports only if they are genuinely unnecessary. We also have to add back in imports (because they have been removed from higher up the import hierarchy).
I've committed the Lean script (thanks Mario!) that generates the underlying data, but not the Mathematica notebook that does that import calculations and text replacement (because it's a mess, and I want this merged quickly before it rots).
* We try not to reorder imports unnecessarily.
* But we don't sort: anything new that needs to be added just comes after the existing imports.
* This drops a few comments on `import` lines.
* It replaces a few `import X` with `import X.default`. (I think this is not bad: we probably want to remove all the .default files anyway at some point.)
Co-authored-by: Scott Morrison <scott.morrison@gmail.com>
