# Zulip Chat Archive

## Stream: general

### Topic: slow proofs

#### Yury G. Kudryashov (Dec 24 2019 at 01:03):

Hi, the following files have largest compile times as counted by running something like `for f in $(find . -name *.lean); do time lean -j1 --profile $f; done`

after `leanpkg build`

:

./src/data/complex/exponential.time!1:01.78 ./src/data/polynomial.time!1:57.13 ./src/data/real/ennreal.time!1:01.25 ./src/group_theory/congruence.time!1:03.07 ./src/linear_algebra/basic.time!1:58.68 ./src/ring_theory/power_series.time!1:18.62 ./src/topology/algebra/infinite_sum.time!1:37.40 ./src/category_theory/limits/shapes/binary_products.time!2:04.08 ./src/data/multiset.time!2:01.77 ./src/analysis/complex/exponential.time!3:50.83

#### Yury G. Kudryashov (Dec 24 2019 at 01:03):

And the longest-running proof is

lemma dist_le_tsum_dist_of_tendsto [metric_space α] {f : ℕ → α} (h : summable (λn, dist (f n) (f n.succ))) {a : α} (ha : tendsto f at_top (𝓝 a)) (n) : dist (f n) a ≤ ∑ m, dist (f (n+m)) (f (n+m).succ) := dist_le_tsum_of_dist_le_of_tendsto (λ n:ℕ, dist (f n) (f n.succ)) (λ n:ℕ, le_refl (dist (f n) (f n.succ))) h ha n

in `infinite_sum.lean`

.

#### Yury G. Kudryashov (Dec 24 2019 at 01:04):

Any idea what makes it so hard to elaborate this proof?

#### Simon Hudon (Dec 24 2019 at 01:07):

The two things I can think of are 1. how long is the path to the type class instances that it needs (and the number of candidates being considered) 2. and the amount of definition unfolding required to check that functions are applied to arguments of the right type.

#### Yury G. Kudryashov (Dec 24 2019 at 01:09):

lemma dist_le_tsum_of_dist_le_of_tendsto [metric_space α] {f : ℕ → α} (d : ℕ → ℝ) (hf : ∀ n, dist (f n) (f n.succ) ≤ d n) (hd : summable d) {a : α} (ha : tendsto f at_top (𝓝 a)) (n : ℕ) : dist (f n) a ≤ ∑ m, d (n + m) := _

#### Yury G. Kudryashov (Dec 24 2019 at 01:11):

Is it possible to trace unfolding of definitions?

#### Yury G. Kudryashov (Dec 24 2019 at 01:11):

I don't see any definitions to unfold here.

#### Joe (Dec 24 2019 at 01:14):

lemma dist_le_tsum_dist_of_tendsto [metric_space α] {f : ℕ → α} (h : summable (λn, dist (f n) (f n.succ))) {a : α} (ha : tendsto f at_top (𝓝 a)) (n) : dist (f n) a ≤ ∑ m, dist (f (n+m)) (f (n+m).succ) := show dist (f n) a ≤ ∑ m, (λx, dist (f x) (f x.succ)) (n + m), from dist_le_tsum_of_dist_le_of_tendsto (λ n, dist (f n) (f n.succ)) (λ _, le_refl _) h ha n

#### Joe (Dec 24 2019 at 01:14):

I think this should fix it.

#### Joe (Dec 24 2019 at 01:15):

Lean cannot find the function `d`

in `dist_le_tsum_of_dist_le_of_tendsto`

#### Yury G. Kudryashov (Dec 24 2019 at 01:18):

Thanks @Joe!

#### Joe (Dec 24 2019 at 01:19):

No problem.

#### Yury G. Kudryashov (Dec 24 2019 at 03:13):

Is there any way to understand which tactic in a long `begin...end`

block slows down the elaboration?

#### Jesse Michael Han (Dec 24 2019 at 04:02):

try enabling the profiler

#### Yury G. Kudryashov (Dec 24 2019 at 04:06):

`lean --profile --json`

reports `... took ... s`

once for each `begin ... end`

block.

#### Yury G. Kudryashov (Dec 24 2019 at 04:06):

Or maybe more than once but each time it points to the position of `end`

.

#### Simon Hudon (Dec 24 2019 at 04:08):

It might be more convenient if you use `set_option profiler`

to turn it on

Last updated: May 14 2021 at 22:15 UTC