The long pole in mathlib

Stream: general

[Scott Morrison]

I recently computed "the long pole" in mathlib --- the longest chain of transitive imports, weighted by the compilation time of each file. Given arbitrary parallelism, this would give us the compilation time of the entirety of mathlib.

data/real/pi    34.9626
analysis/special_functions/integrals    50.0778
measure_theory/integral/interval_integral   88.211
measure_theory/measure/lebesgue 29.6158
measure_theory/constructions/pi 40.3023
measure_theory/constructions/prod   53.4363
measure_theory/integral/set_integral    39.7534
measure_theory/integral/bochner 70.9691
measure_theory/integral/set_to_l1   47.3601
measure_theory/function/simple_func_dense   72.6324
measure_theory/function/l1_space    51.5644
measure_theory/function/lp_space    147.01
measure_theory/integral/mean_inequalities   17.5914
analysis/mean_inequalities  36.4278
analysis/convex/specific_functions  11.9636
analysis/special_functions/pow  124.392
analysis/special_functions/trigonometric    172.476
analysis/special_functions/exp_log  24.8909
analysis/complex/real_deriv 16.6262
analysis/complex/conformal  24.4022
analysis/normed_space/conformal_linear_map  13.4382
analysis/normed_space/inner_product 225.452
analysis/special_functions/sqrt 8.66522
analysis/calculus/times_cont_diff   115.127
analysis/calculus/mean_value    24.793
analysis/calculus/local_extr    16.9887
analysis/calculus/deriv 87.9592
analysis/calculus/fderiv    114.51
analysis/analytic/basic 73.1241
analysis/calculus/formal_multilinear_series 6.70325
analysis/normed_space/multilinear   130.405
analysis/normed_space/operator_norm 97.637
analysis/normed_space/linear_isometry   6.22745
linear_algebra/finite_dimensional   58.8543
field_theory/finiteness 5.43609
ring_theory/finiteness  27.3561
ring_theory/algebra_tower   24.1719
ring_theory/adjoin/fg   6.21294
ring_theory/adjoin/polynomial   5.80635
ring_theory/polynomial/basic    72.7344
ring_theory/principal_ideal_domain  12.6089
ring_theory/unique_factorization_domain 42.9805
ring_theory/integral_domain 9.11644
data/polynomial/ring_division   16.6944
data/polynomial/div 12.952
data/polynomial/monic   13.6841
data/polynomial/reverse 6.24052
data/polynomial/eval    33.6065
data/polynomial/degree/definitions  21.1174
data/polynomial/monomial    10.8134
data/polynomial/coeff   10.6286
data/polynomial/basic   41.7989
algebra/monoid_algebra/basic    77.746
algebra/non_unital_alg_hom  5.13058
algebra/algebra/basic   37.5372
linear_algebra/tensor_product   45.8692
linear_algebra/bilinear_map 3.95732
linear_algebra/basic    92.5836
data/dfinsupp   59.9861
algebra/module/linear_map   7.07023
algebra/group_action_hom    4.23101
algebra/group_ring_action   3.2552
ring_theory/subring 10.4688
group_theory/subgroup   37.3691
group_theory/submonoid/center   2.91385
group_theory/submonoid/operations   8.3513
algebra/pointwise   8.32447
algebra/module/basic    6.11838
algebra/big_operators/basic 26.6518
tactic/abel 6.3525
tactic/norm_num 7.2906
data/rat/cast   8.50179
data/int/char_zero  1.92927
algebra/char_zero   3.30769
data/fintype/basic  26.5525
data/finset/powerset    3.87303
data/finset/lattice 6.63514
data/finset/fold    3.0229
data/finset/basic   34.6086
data/multiset/finset_ops    3.31185
data/multiset/erase_dup 2.25666
data/multiset/nodup 2.91105
data/multiset/powerset  4.57061
data/multiset/basic 25.7305
data/list/perm  11.7846
data/list/erase_dup 1.60637
data/list/nodup 3.45075
data/list/pairwise  3.81794
data/list/sublists  3.30711
data/list/basic 42.1169
data/nat/basic  9.98537
algebra/ordered_ring    17.1195
data/set/intervals/basic    16.4385
algebra/ordered_group   10.7727
algebra/ordered_monoid  10.291
algebra/group/prod  5.30827
algebra/opposites   2.50444
algebra/field   3.38681
algebra/ring/basic  6.85919
algebra/regular/basic   1.31733
logic/embedding 3.46166
data/equiv/basic    15.8946
data/set/function   3.41891
data/set/basic  18.229
order/boolean_algebra   11.0211
order/bounded_lattice   6.16343
order/lattice   2.56701
order/rel_classes   1.19856
order/basic 1.60228
data/prod   0.839731
tactic/basic    0.567406
tactic/obviously    0.494836
tactic/tidy 0.568107
tactic/norm_cast    1.24841
tactic/hint 0.558297
tactic/interactive  1.2318
tactic/dependencies 0.609335
tactic/core 1.68626
tactic/binder_matching  0.456182
meta/expr   1.04582
meta/rb_map 0.421523
data/list/defs  0.947617
logic/basic 1.61654
tactic/doc_commands 0.477453
tactic/fix_reflect_string   0.359337

[Scott Morrison]

If anyone is interested I can post the longest chain starting at any given (or even all) files in mathlib.

[Scott Morrison]

If anyone sees something slow on that list that shouldn't really be needed for data/real/pi, feel free to PR changes that move things off this chain, or speed them up!

[Scott Morrison]

Here's a spanning tree of mathlib, for which each file's parent has been chosen as the slowest-to-compile-given-arbitrary-parallelism:

Screen-Shot-2021-09-19-at-8.44.03-pm.png

I have a version in mathematica with tooltips that actually show the files names, but I don't have an easy to share version of that.

[Johan Commelin]

It certainly looks like poor π needs to wait for a lot of stuff. Finite dimensional vector spaces, inner products, unique factorization domains.

[Eric Wieser]

How did you obtain the data? Is it something we should set up a CI bot to do?

[Scott Morrison]

I pulled the JSON file of mathlib build times from the CI stream (e.g. "https://mathlib-bench.limperg.de/commit/10a620163757cd2cf745db99c686e9721a1d0d3b/json"), and then parsed all the mathlib files for import statements.

[Scott Morrison]

It's written in mathematica, so not exactly deployable in CI, but it would be easy to translate if someone wanted to.

[Scott Morrison]

mathlib-imports.nb

[Bolton Bailey]

Seems like smul_eq_C_mul in data/polynomial/monomial is the only reason that file can't import data/polynomial/basic directly instead of data/polynomial/coeff. I remember there being some kind of awkward interdependency between those, but I guess it's resolved now.

[Scott Morrison]

#9289 was motivated by this analysis: we don't need the theory of finite dimensional vector spaces to develop pi.

[Scott Morrison]

It reduces the long pole from 54.6 minutes to 51.6 minutes.

[Bolton Bailey]

Does the longest pole switch to something completely different when you make this change, or is most of it the same?

[Scott Morrison]

No, this one is going to be the long pole for a long time.

[Scott Morrison]

After #9292 and #9293 the long pole is down to 46.5 minutes.

[Mario Carneiro]

Here's a script, based on get_axioms_used, that will print the files used in all dependents of a given list of target theorems. If you run this on all theorems in data.real.pi you should get a lower bound on the files that are needed to actually prove the theorems, assuming you don't split any files up:

import data.real.pi

meta def tactic.get_dependents_aux (env : environment) : name →
  name_set × name_set → tactic (name_set × name_set)
| n p@(fs, ns) := if ns.contains n then pure p else do
  let fs := match env.decl_olean n with
  | none := fs
  | some f := fs.insert f
  end,
  d ← env.get n,
  let ns := ns.insert n,
  let process (v : expr) : tactic (name_set × name_set) := (do
    v.fold (pure (fs, ns)) $ λ e _ r, r >>= λ p,
      if e.is_constant then tactic.get_dependents_aux e.const_name p else pure p),
  match d with
  | (declaration.defn _ _ _ v _ _) := process v
  | (declaration.thm _ _ _ v)      := process v.get
  | _ := pure (fs, ns)
  end

meta def tactic.get_dependents (ns : list name) : tactic name_set :=
do env ← tactic.get_env,
  prod.fst <$> ns.mfoldl (λ p n, tactic.get_dependents_aux env n p) (mk_name_set, mk_name_set)

#eval do
  s ← tactic.get_dependents [``real.pi_gt_3141592, ``real.pi_lt_3141593],
  s.fold (pure ()) $ λ e r, r >> tactic.trace e

[Mario Carneiro]

Taking the diff from the "long pole" above yields the following list of files, which are imported but for which none of the theorems are used transitively:

algebra/group_ring_action
algebra/monoid_algebra/basic
algebra/non_unital_alg_hom
algebra/opposites
algebra/ordered_group
algebra/ordered_monoid
algebra/ordered_ring
analysis/analytic/basic
analysis/calculus/local_extr
analysis/complex/conformal
analysis/convex/specific_functions
analysis/mean_inequalities
analysis/normed_space/conformal_linear_map
analysis/special_functions/integrals
analysis/special_functions/pow
analysis/special_functions/sqrt
data/finset/powerset
data/list/sublists
data/multiset/powerset
data/polynomial/basic
data/polynomial/coeff
data/polynomial/degree/definitions
data/polynomial/div
data/polynomial/eval
data/polynomial/monic
data/polynomial/monomial
data/polynomial/reverse
data/polynomial/ring_division
group_theory/submonoid/center
linear_algebra/tensor_product
measure_theory/constructions/pi
measure_theory/constructions/prod
measure_theory/function/l1_space
measure_theory/function/lp_space
measure_theory/function/simple_func_dense
measure_theory/integral/bochner
measure_theory/integral/interval_integral
measure_theory/integral/mean_inequalities
measure_theory/integral/set_integral
measure_theory/integral/set_to_l1
measure_theory/measure/lebesgue
meta/expr
meta/rb_map
ring_theory/adjoin/basic
ring_theory/integral_domain
ring_theory/polynomial/basic
ring_theory/subring
ring_theory/unique_factorization_domain
tactic/basic
tactic/binder_matching
tactic/core
tactic/dependencies
tactic/doc_commands
tactic/fix_reflect_string
tactic/hint
tactic/interactive
tactic/obviously
tactic/tidy

[Scott Morrison]

Very interesting! Taking the files appearing in the long pile to data.real.pi, subtracting out Mario's list (everything that is actually needed), we get:

algebra/group_ring_action
algebra/opposites
analysis/analytic/basic
analysis/calculus/inverse
analysis/calculus/local_extr
analysis/convex/specific_functions
analysis/mean_inequalities
analysis/special_functions/integrals
analysis/special_functions/pow
data/dfinsupp
data/finset/powerset
data/list/sublists
data/multiset/powerset
linear_algebra/tensor_product
measure_theory/constructions/pi
measure_theory/constructions/prod
measure_theory/function/l1_space
measure_theory/function/lp_space
measure_theory/function/simple_func_dense
measure_theory/integral/bochner
measure_theory/integral/interval_integral
measure_theory/integral/mean_inequalities
measure_theory/integral/set_integral
measure_theory/integral/set_to_l1
measure_theory/measure/lebesgue
meta/expr
meta/rb_map
ring_theory/subring
tactic/basic
tactic/binder_matching
tactic/core
tactic/dependencies
tactic/doc_commands
tactic/fix_reflect_string
tactic/hint
tactic/interactive
tactic/obviously
tactic/tidy
topology/algebra/infinite_sum
topology/instances/ennreal

[Mario Carneiro]

we got different lists :thinking:

[Scott Morrison]

These are the files that we are "uselessly importing" on the way to data.real.pi. In particular "most of measure theory".

[Scott Morrison]

No -- this complement is exactly what is interesting. It's the stuff that, by doing a bit of splitting so we can only import what we really need, can be removed from the import dependencies of data.real.pi.

[Mario Carneiro]

No, I mean I updated my list above to do basically the same calculation (I think) and got a different list of files

[Mario Carneiro]

mine doesn't have any topology

[Scott Morrison]

Oh! I missed the edit above, soory.

[Mario Carneiro]

Oh, maybe you are including the effect of those PRs

[Mario Carneiro]

I used latest master

[Scott Morrison]

Yes, I was using a local branch which was the sup of today's PRs on this.

[Scott Morrison]

So the difference between our lists is what I've already removed from the import dependencies of data.real.pi.

[Scott Morrison]

Of course, my PRs have not finished CI, so are probably still horribly broken by missing imports. :-)

[Mario Carneiro]

Also, I didn't include all of the theorems in data.real.pi, just the bound calculation

[Mario Carneiro]

Oh, and it makes a difference: all these files are added to the list when you add in the wallis product and leibniz series:

algebra/big_operators/finsupp
algebra/char_p/invertible
algebra/invertible
algebra/monoid_algebra/basic
algebra/opposites
analysis/calculus/extend_deriv
analysis/calculus/local_extr
analysis/convex/combination
analysis/convex/cone
analysis/convex/specific_functions
analysis/mean_inequalities
analysis/normed_space/dual
analysis/normed_space/extend
analysis/normed_space/hahn_banach
analysis/normed_space/indicator_function
analysis/normed_space/units
analysis/special_functions/integrals
analysis/special_functions/pow
data/equiv/encodable/lattice
data/equiv/local_equiv
data/equiv/nat
data/equiv/ring
data/nat/parity
data/opposite
data/polynomial/basic
data/polynomial/coeff
data/polynomial/derivative
data/polynomial/eval
data/polynomial/induction
data/real/conjugate_exponents
data/real/ereal
data/set/accumulate
data/set/intervals/disjoint
data/set/intervals/proj_Icc
data/set/pairwise
group_theory/perm/basic
linear_algebra/linear_pmap
logic/relator
measure_theory/constructions/borel_space
measure_theory/function/ae_eq_fun
measure_theory/function/ae_measurable_sequence
measure_theory/function/ess_sup
measure_theory/function/l1_space
measure_theory/function/lp_space
measure_theory/function/simple_func_dense
measure_theory/function/special_functions
measure_theory/group/arithmetic
measure_theory/integral/bochner
measure_theory/integral/integrable_on
measure_theory/integral/interval_integral
measure_theory/integral/lebesgue
measure_theory/integral/mean_inequalities
measure_theory/integral/set_integral
measure_theory/integral/set_to_l1
measure_theory/integral/vitali_caratheodory
measure_theory/measurable_space
measure_theory/measurable_space_def
measure_theory/measure/lebesgue
measure_theory/measure/measure_space
measure_theory/measure/measure_space_def
measure_theory/measure/outer_measure
measure_theory/measure/regular
measure_theory/measure/stieltjes
measure_theory/pi_system
order/disjointed
order/filter/archimedean
order/filter/cofinite
order/filter/countable_Inter
order/filter/ennreal
order/filter/extr
order/filter/germ
order/liminf_limsup
tactic/ring_exp
topology/algebra/group_with_zero
topology/algebra/infinite_sum
topology/algebra/ordered/liminf_limsup
topology/algebra/ordered/proj_Icc
topology/bases
topology/dense_embedding
topology/instances/ennreal
topology/instances/ereal
topology/local_extr
topology/local_homeomorph
topology/metric_space/cau_seq_filter
topology/semicontinuous
topology/sequences

[Mario Carneiro]

which brings the list of unnecessary imports down to:

algebra/group_ring_action
analysis/analytic/basic
analysis/calculus/inverse
data/dfinsupp
data/finset/powerset
data/list/sublists
data/multiset/powerset
linear_algebra/tensor_product
measure_theory/constructions/pi
measure_theory/constructions/prod
meta/expr
meta/rb_map
ring_theory/subring
tactic/basic
tactic/binder_matching
tactic/core
tactic/dependencies
tactic/doc_commands
tactic/fix_reflect_string
tactic/hint
tactic/interactive
tactic/obviously
tactic/tidy

[Mario Carneiro]

but it also suggests that maybe the two halves of data.real.pi shouldn't be in the same file

[Johan Commelin]

@Scott Morrison What is the difference between the length of the long pole and the length of an actual mathlib compile? Can we gain something by making lean aware of the long pole?

[Heather Macbeth]

The Wallis product argument could be rephrased to use the mean value theorem rather than the fundamental theorem of calculus (thus, no measure theory import), if we want to displace the precise position of the long pole.

[Scott Morrison]

I don't think it's particularly valuable to reduce the long pole at the cost of new mathematical arguments, unless they are independently "better".

[Scott Morrison]

I don't want to object to anyone using high powered maths to give easy proofs. :-)

[Scott Morrison]

But, like in real life, if someone gave me a long-winded introduction to subject X, then gave an argument that didn't use it at all, I would be annoyed!

[Scott Morrison]

Johan Commelin said:

Scott Morrison What is the difference between the length of the long pole and the length of an actual mathlib compile? Can we gain something by making lean aware of the long pole?

I guess potentially we could.

Currently the long pole analysis assumes infinite parallelism, in which case the build would be deterministic --- everything would compile as soon as it possibly could. In that idealisation the only way to speed things up is to shorten the long pole by changing the code.

With finite parallelism, every time a core come free you have to make a choice between the new compilation units that become available.

It's not immediately clear how to do a cheap computation on-the-fly to decide this. I guess at the beginning we could just assign each file a score "total compilation time remaining after this file, assuming infinite parallelism", and always pick the file with largest score. This would be pretty easy to implement. It would even be reasonable to simulate (e.g. and compare against the "random" and "smallest score" strategies to get a sense of value).

[Mario Carneiro]

Lean is also more finely parallelized than this - each proof is processed independently, although perhaps the advantage of this is dubious and I believe this is no longer done in lean 4. So this "long pole" model is maybe a little too coarse, although it's not entirely wrong to consider the cost of reading through the definitions and other objects involved in parsing a lean file (the single threaded part) since they contribute to this "long pole", but it is a bit untrue to put the elaboration cost of all the proofs in that metric.

[Scott Morrison]

The per-declaration parallelisation is gone in Lean4, and I'm not sure it actually crosses file boundaries in Lean3 anyway. (Does anyone know for sure on this? That is, if A imports B, does compilation of A start once all the definitions on B are done, even if there are still proofs to B being worked on? Or does A not start until the B is completely finished?)

[Johan Commelin]

Scott Morrison said:

With finite parallelism, every time a core come free you have to make a choice between the new compilation units that become available.

It's not immediately clear how to do a cheap computation on-the-fly to decide this. I guess at the beginning we could just assign each file a score "total compilation time remaining after this file, assuming infinite parallelism", and always pick the file with largest score. This would be pretty easy to implement. It would even be reasonable to simulate (e.g. and compare against the "random" and "smallest score" strategies to get a sense of value).

Right, I meant exactly this. The score is only an approximation of the "real 16-core parallelism score" because it makes a simplification in computing the score. But it might still be a better heuristic than "pick something random".

[Alex J. Best]

Scott Morrison said:

The per-declaration parallelisation is gone in Lean4, and I'm not sure it actually crosses file boundaries in Lean3 anyway. (Does anyone know for sure on this? That is, if A imports B, does compilation of A start once all the definitions on B are done, even if there are still proofs to B being worked on? Or does A not start until the B is completely finished?)

I made a simple test project to check whether lean does move on to lemmas in later files and it seems it does.
In https://github.com/alexjbest/pole-test there are two lean files a and b, each of which has two lemmas, the ones in a sleep for 10 and 20 seconds respectively. The ones in b just spam the CPU with dumb rfl statements. So running lean -j2 src/b.lean to check these files with 2 threads I see nothing happening to the CPU for 10 seconds, then 100% of one core, then 10 seconds later 200%, which I think shows lean is moving on to b with one thread while the longer lemma in a is still being processed. Of course this will look a bit different if your machine is fast enough to do the b lemmas in < 10s.

[Scott Morrison]

Good to know! Thank you. In any case this behaviour is disappearing in Lean4, so we shouldn't plan around it. :-)

[Bolton Bailey]

#9344 is a PR for a python implementation of this script.

[Scott Morrison]

@Bolton Bailey, I see you closed the PR in favour of a PR to mathlibtools. It's perfect if this functionality ends up in leanproject, but be aware the quality standards for leanproject are going to much higher than the scripts/ directory of mathlib. Perfect is the enemy of good: if this doesn't make it into leanproject, please do dump it into scripts/!

[Eric Wieser]

A middle ground would be to just import mathlibtools, as something like:

from mathlibtools.lib import LeanProject

proj = LeanProject.from_path(Path("."))
graph = proj.import_graph

[Eric Wieser]

That might be the better choice anyway, in fact, as the json files this processes only really exist for mathlib

[Eric Wieser]

The only downside is that the install instructions for mathlibtools don't make the import available on all platforms

[Eric Wieser]

But if you use pip and not pipx it works fine

[Scott Morrison]

Ok, I cracked and wrote a mathlib scheduler simulator.

These graphs are based on a random scheduler.

Compile time as function of max cores:
Screen-Shot-2021-09-23-at-8.54.29-pm.png

Core usage with max 4/10/40 cores:
Screen-Shot-2021-09-23-at-8.50.31-pm.png Screen-Shot-2021-09-23-at-8.50.36-pm.png Screen-Shot-2021-09-23-at-8.50.43-pm.png

[Scott Morrison]

So far, trying different scheduling strategies gives no more than about a 10% variation. And "random" seems to be close to the best. :-)

[Johan Commelin]

hmmm, thanks a lot!

[Johan Commelin]

Even though it's a bit disappointing that "random" is good enough

[Alex J. Best]

@Scott Morrison what are these graphs/what is the scheduler simulator? is it just working at file level granularity?

[Mario Carneiro]

Here's another interesting way to cut the data: weight the files extra based on how much under-utilization there is. That is, if CPU utilization is 3 CPUs when 10 are available, then all three active files get 10/3 more "effective time" to their name. Files with the most effective time spent on them exist at cutpoints and decreases in the time spent there will have outsized benefits

[Scott Morrison]

@Alex J. Best, yes, it's just working at file level. I keep track of a set of files remaining. Each entry is a filename, a time to compile that file, and a list of remaining dependencies. Whenever there is a CPU available and at least one file with no remaining dependencies, I pass the list of such files to the "scheduler" function to pick which one to start work on.

[Scott Morrison]

Mario's suggestion, top 20 by utilisation-weighted compilation time:

measure_theory/integral/interval_integral   912.659
measure_theory/function/simple_func_dense   717.784
measure_theory/integral/bochner 698.796
measure_theory/integral/set_to_l1   535.138
measure_theory/constructions/prod   533.549
analysis/special_functions/integrals    511.95
analysis/special_functions/pow  417.861
measure_theory/integral/set_integral    400.362
measure_theory/function/lp_space    373.746
linear_algebra/quadratic_form   331.299
measure_theory/function/l1_space    255.831
measure_theory/measure/hausdorff    244.415
geometry/euclidean/circumcenter 236.834
analysis/normed_space/inner_product 227.198
geometry/manifold/times_cont_mdiff  221.865
linear_algebra/clifford_algebra/equivs  217.447
measure_theory/measure/lebesgue 207.226
analysis/special_functions/trigonometric    192.349
measure_theory/decomposition/lebesgue   181.744
measure_theory/measure/measure_space    166.835

[Scott Morrison]

I'm not sure that it is that interesting --- mostly we're just seeing that the rest of mathlib is done by the time we get to integration.

[Scott Morrison]

I think the measure space library generally opts to introduce a notion and prove everything about it all in one file, so it ends up being a long sequence of files, each depending on one file before it, and not much parallelism is possible.

[Scott Morrison]

As an example, I found it pretty surprising that the file in which we define a product measure already imports "everything" about Lebesgue measure. I would have thought that the basic construction would come much earlier. (e.g. even in a context where integration isn't set up, so Fubini/Tonelli would happen in a later file).

[Mario Carneiro]

What can we do to detect such "short poles" in mathlib? That is, linear sequences of files with high compile time

[Scott Morrison]

This is a version of the spanning tree, where the y-coordinate of a node gives the time to reach that file under infinite parallelism, and the parent of each node is the last-to-start import.

mathlib-spanning-tree.png

[Heather Macbeth]

Part of the problem is that Bochner integration imports L1 space which imports Lp space, which imports the function of raising a real number to the p-th power, which imports all of calculus.

We have a construction of the exponential which doesn't use calculus:
docs#data.complex.exponential
Would it be worth adding the definition of powers to this file, too? Then measure theory could be compiled in parallel to calculus rather than after it.

[Scott Morrison]

This sounds great! It does seem like we should be able to do a lot of integration theory without calculus.

[Eric Wieser]

Is the correct version of that link docs#complex.exp?

[Johan Commelin]

I think Heather wanted to link to a file. I guess we could potentially have file#data.complex.exponential ?

[Scott Morrison]

It seems a reasonable first step might be to break analysis/mean_inequalities into separate files, so it's easier to pinpoint exactly which lemmas about has_pow ℝ ℝ are really needed.

[Heather Macbeth]

Yes -- note that it's possible that some proofs currently use calculus but wouldn't have to, like I wouldn't be surprised if there's a more direct proof of convexity.

[Heather Macbeth]

Another possibility is

• define [Lp_class f g] where f and g are a pair of inverse functions from ℝ≥0∞ to itself satisfying ... some list of properties
• define Lp_space to take (f : ℝ≥0∞ → ℝ≥0∞) (g : ℝ≥0∞ → ℝ≥0∞) [Lp_class f g] rather than p
• check that [Lp_class id id] and define $L^1$ to be Lp_space id id
• much later in the hierarchy, check that [Lp_class (λ x, x ^ p) (λ x, x ^ (1 / p))]

[Scott Morrison]

Hmm, I feel like this is too far a compromise. Mathlib compiling fast is nice, and I don't mind changing from one mathematically plausible definition to another to achieve this, but [Lp_class] doesn't really have a leg to stand on mathematically. :-)

[Heather Macbeth]

There would actually be one other use for Lp_class. It is rather a pain currently that when people work with $L^2$, the squaring involved is raising to the (2:ℝ≥0∞) power rather than the nat-2 power. One has to mess around with power-cast lemmas, usually explicitly because it's a bit beyond the capabilities of norm_cast. This would let $L^2$ be defined with nat-2 powers.

[Rémy Degenne]

I feel like changing the proof of convexity of the exponential (and rpow) to use a direct computation (like the first answer there: https://math.stackexchange.com/questions/1583000/convexity-of-exponential-function) and isolating the use of calculus in analysis.special_functions.pow is the simpler approach.

[Rémy Degenne]

But I agree that the ennreal power in L2 is a pain :)

[Heather Macbeth]

OK, let's do that! Maybe we just need to sit down and figure out the right simp-lemmas to improve working in L2.

[Scott Morrison]

I'd thought I could try working on this today, but I seem to be in a no-ssh-allowed internet environment for a little while, and working on mathlib may just be too painful.

[Rémy Degenne]

I have started working on isolating calculus in analysis/special_functions. Currently, all proofs of continuity of exp, log and the trigonometric functions use the existence of derivatives. Then continuity of exp is used for the definition of the real log, which is used in the definition of complex log, cpow, etc.
I am replacing the proofs of continuity by direct ones in order to get a definition of all those objects without using derivatives.

[Heather Macbeth]

Do we need the continuity for Lp spaces, though?

[Rémy Degenne]

i don't know? i am not sure that I get what you ask.
I have observed that in order to define log (and everything that depends on it), we currently use continuity of the exponential: docs#real.log uses docs#real.exp_order_iso, whose surjectivity is proven through continuity. Hence I have made that continuity derivative-free. You want to avoid talking about continuity in those definitions?

[Kevin Buzzard]

What is our proof that a function defined by a power series $\sum_n a_nz^n$ is continuous where the power series converges? [I mean, what does it use?]

[Heather Macbeth]

I see, you're right, continuity seems like the easiest proof of surjectivity. I can think of three approaches to get continuity:

• directly as you've done
• via docs#analytic_at.continuous_at as @Kevin Buzzard suggests
• prove that convex implies continuous (useful to have in any case)

[Yaël Dillies]

Oh, do we not have the last one?

[Scott Morrison]

@Rémy Degenne, please note I have #9340 open, which splits the development of trigonometry across several files. This seems likely to conflict with what you're doing, so perhaps you could either have a look at my PR, or base your work on top of it?

[Rémy Degenne]

Indeed, I now have a big pile of conflicts because I split that file in a different way. That merge will be fun.

[Scott Morrison]

Sorry. :-( If it is too painful I can abandon mine. I'd prefer that content-ful PRs get priority over merely re-arranging PRs, of course.

[Rémy Degenne]

No problem. I'll deal with it.

[Rémy Degenne]

And #9340 is already merged into master anyway, so it's a bit late to abandon it :)

[Rémy Degenne]

Looks like @Yury G. Kudryashov is also modifying those files in #9405 and #9406 . I'll come back to this in a few days, when the special_functions folder stabilizes a bit.

[Yury G. Kudryashov]

Hi, did I miss some refactoring going on?

[Yaël Dillies]

A big sweepy swoop!

[Yury G. Kudryashov]

#9405 and #9406 are small PRs, I can redo them on top of any large refactor (though if the refactor is not ready yet, then I'd prefer to merge these, then help merging master).

[Rémy Degenne]

The refactor is not ready yet, because I did not see another PR that got merged recently and split many files. I will need time to fix my branch. You should go ahead with your PRs.

The story is that I want to remove the dependence on derivatives in the definitions of the various special functions, which means removing derivatives from some proofs of continuity. Then all the files should be split into two, one of which does not import calculus.

[Rémy Degenne]

The end goal, which relates this to the title of the thread, is to remove calculus from the imports of lp_space in measure theory

[Yury G. Kudryashov]

Note that I'd like to have exp redefined in terms of power series from analytic_at some day.

[Yury G. Kudryashov]

And use the same definition for real numbers, complex numbers, and any Banach algebra.

[Yury G. Kudryashov]

Though others may not agree.

[Eric Rodriguez]

previous discussion on this: https://leanprover.zulipchat.com/#narrow/stream/113488-general/topic/exponential.20in.20banach.20algebras/near/248773988

[Rémy Degenne]

@Scott Morrison would it be possible to produce the same kind of spanning tree you showed above in that thread, applied to branch#pow_split ? In that branch, most of measure theory does not import derivatives.

[Scott Morrison]

Sure!

[Scott Morrison]

Ah, maybe not, https://mathlib-bench.limperg.de/commit/ab7d25193590b63a2380632018cfb3c8616accdf is down, and I don't have a local copy.

[Scott Morrison]

(These are the build times for files on master --- this won't really be accurate for analysing a different branch: we'll just use a different import graph, and pretend the compile times of individual files haven't changed.)

[Rémy Degenne]

I created and deleted files in that branch

[Scott Morrison]

@Jannis Limperg, any idea why the build time bot logs are offline?

[Scott Morrison]

@Rémy Degenne, it may not actually matter that much --- it will be a matter of whether you've shortened the long pole, rather than sped up individual files.

[Scott Morrison]

i.e. you will still see all the benefit of removing imports, when we look at the cumulative time to reach a given file.

[Rémy Degenne]

Right, having an inaccurate time for a few changed files won't matter much.

[Scott Morrison]

But if you want that level of meaningfulness, we'd have to ask Jannis if he can run the bot on your branch.

[Scott Morrison]

I'll check tomorrow if his site has come back online, but probably won't have further time tonight.

[Jannis Limperg]

Scott Morrison said:

Jannis Limperg, any idea why the build time bot logs are offline?

They occasionally die for unknown reasons. I've restarted the service; thanks for the ping!

I've also started a build of bc09898fabb811d5da516a854aff52eaa98a14e7 for comparison. @Rémy Degenne is this the right commit?

[Rémy Degenne]

yes, that's the right one. Thanks!

[Scott Morrison]

Okay, subject to the timing data being dodgy as described above, branch#pow_split should reduce the infinite-core compile time from 45.9 minutes to 43.6 minutes!

[Scott Morrison]

Nice!

[Rémy Degenne]

Thanks for the computation. I expected a bigger effect than a 2min improvement :)

[Scott Morrison]

Call it a 5% improvement? That sounds pretty good!

[Scott Morrison]

When Jannis' build comes back I can give you a more accurate number.

[Jannis Limperg]

Ah wait do you need per-file timings from the branch build?

[Scott Morrison]

Yes, that's what would let me do something more accurate.

[Jannis Limperg]

Okay, then I'll have to set that up real quick.

[Scott Morrison]

But I don't think it matters too much. In any case, I'm off to bed for today.

[Jannis Limperg]

@Scott Morrison Here are the timings for the pow_split branch: pow-split-timings.txt