golfing the longest chain

Stream: mathlib4

[Heather Macbeth]

Scott Morrison said:

That long initial sequence of lines beginning with - was irresistible: #19041.

After #19041 the longest chain was back to continous_functional_calculus:

  analysis.normed_space.bounded_linear_maps
  analysis.calculus.fderiv.basic
  analysis.calculus.fderiv.linear
  analysis.calculus.fderiv.prod
  analysis.calculus.fderiv.bilinear
  analysis.calculus.fderiv.mul
  analysis.calculus.deriv
- analysis.calculus.local_extr
  analysis.calculus.mean_value
  analysis.calculus.cont_diff
- analysis.calculus.inverse
  analysis.special_functions.exp_deriv
- analysis.special_functions.complex.log_deriv
- analysis.special_functions.pow.deriv
- analysis.convex.specific_functions.deriv
- analysis.special_functions.trigonometric.complex
- analysis.special_functions.trigonometric.arctan
- analysis.special_functions.trigonometric.arctan_deriv
- analysis.special_functions.integrals
  analysis.special_functions.non_integrable
  measure_theory.integral.circle_integral
  analysis.complex.cauchy_integral
  analysis.complex.liouville
- analysis.complex.polynomial
  analysis.normed_space.spectrum
  analysis.normed_space.star.spectrum
  analysis.normed_space.star.gelfand_duality
  analysis.normed_space.star.continuous_functional_calculus

[Heather Macbeth]

So I split out the obvious part, #19047. Now the longest chain is in number theory:

- ring_theory.polynomial_algebra
- linear_algebra.matrix.charpoly.basic
- linear_algebra.matrix.charpoly.coeff
- linear_algebra.matrix.charpoly.linear_map
- ring_theory.integral_closure
- field_theory.minpoly.basic
- field_theory.minpoly.field
- ring_theory.power_basis
- ring_theory.adjoin_root
- ring_theory.adjoin.field
- field_theory.splitting_field
- field_theory.adjoin
- field_theory.normal
- field_theory.is_alg_closed.basic
- field_theory.primitive_element
- field_theory.galois
- ring_theory.trace
- ring_theory.dedekind_domain.integral_closure
- number_theory.number_field.basic
- number_theory.cyclotomic.basic
- number_theory.cyclotomic.primitive_roots
- number_theory.legendre_symbol.add_character
- number_theory.legendre_symbol.gauss_sum
- number_theory.legendre_symbol.quadratic_char
- number_theory.legendre_symbol.quadratic_reciprocity
  number_theory.legendre_symbol.gauss_eisenstein_lemmas
  number_theory.wilson

[David Loeffler]

What exactly is the significance of the minus signs here?

[Heather Macbeth]

I believe it means that no declaration from that file is used in a connected chain of declarations leading to something in the (fully elaborated) final file. So in principle that file (or sequence of files) could be split out.

[Eric Wieser]

Note that the splits it encourage benefit only the file at the end of the chain, and not necessarily mathlib as a whole

[Heather Macbeth]

Eh ... I think that a split such as #19047 benefits mathlib as a whole -- it's not just golfing the path to continuous_functional_calculus but to all of complex analysis.

[Heather Macbeth]

And, it's mathematically more elegant not to "depend" on tons of irrelevant stuff!

[David Loeffler]

I think nobody's claiming that splits are never beneficial for mathlib as a whole, just that it isn't always so.

[David Loeffler]

IMHO (as a number theorist), any split here is going to be temporary in effect at best. A split might help with the port, but its effects will be gone again pretty soon after, when someone adds some other file which depends on everything in this chain and more.

[Scott Morrison]

If we want to explicitly prohibit such "joins" happening again later, there is #assert_not_exists (which still needs porting, but you can for now just port as a comment).