mathlib

d6814c58 - feat(*): Reduce imports to only those necessary in the entire library (#10349)

feat(*): Reduce imports to only those necessary in the entire library (#10349) We reduce imports of many files in the library to only those actually needed by the content of the file, this is done by inspecting the declarations and attributes used by declarations in a file, and then computing a minimal set of imports that includes all of the necessary content. (A tool to do this was written by @jcommelin and I for this purpose). The point of doing this is to reduce unnecessary recompilation when files that aren't needed for some file higher up the import graph are changed and everything in between gets recompiled. Another side benefit might be slightly faster simp / library_searches / tc lookups in some files as there may be less random declarations in the environment that aren't too relevant to the file. The exception is that we do not remove any tactic file imports (in this run at least) as that requires more care to get right. We also skip any `default.lean` files as the point of these is to provide a convenient way of importing a large chunk of the library (though arguably no mathlib file should import a default file that has no non-import content). Some OLD statistics (not 100% accurate as several things changed since then): The average number of imports of each file in the library reduces by around 2, (this equals the average number of dependencies of each file) raw numbers are `806748 / 2033` (total number of transitive links/total number files before) to `802710 / 2033` (after) The length of the longest chain of imports in mathlib decreases from 139 to 130. The imports (transitively) removed from the most from other files are as follows (file, decrease in number of files importing): ``` data.polynomial.degree.trailing_degree 13 linear_algebra.quotient 13 ring_theory.principal_ideal_domain 13 data.int.gcd 14 data.polynomial.div 14 data.list.rotate 15 data.nat.modeq 15 data.fin.interval 17 data.int.interval 17 data.pnat.interval 17 ``` The original script generated by an import-reducing tool is at https://github.com/alexjbest/dag-tools though I did clean up the output and some weirdness after running this script In touched files the imports are put into alphabetical order, we tried not to touch too many files that don't have their imports changed, but some were in the many merges and iterations on this. There are a couple of changes to mathlib not to an import line (compared to master) that I couldn't resist doing that became apparent when the tool recommended deletions of imports containing named simp lemmas in the file, that weren't firing and so the tool was right to remove the import. Another sort of issue is discussed in https://github.com/leanprover-community/mathlib/blob/master/src/algebraic_geometry/presheafed_space/has_colimits.lean#L253, this is discussed at https://leanprover.zulipchat.com/#narrow/stream/113488-general/topic/Reordering.20ext.20lemmas/near/261581547 and there seems to be currently no good way to avoid this so we just fix the proof. One can verify this with the command ` git diff origin/master -I import` At a later point we hope to modify this tooling to suggest splits in long files by their prerequisites, but getting the library into a more minimal state w.r.t file imports seems to be important for such a tool to work well. Co-authored-by: Johan Commelin <johan@commelin.net> Co-authored-by: Reid Barton <rwbarton@gmail.com> Co-authored-by: Reid Barton <rwbarton@gmail.com>