Zulip Chat Archive

Stream: general

Topic: slow proofs


view this post on Zulip 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

view this post on Zulip 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.

view this post on Zulip Yury G. Kudryashov (Dec 24 2019 at 01:04):

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

view this post on Zulip 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.

view this post on Zulip 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) :=
_

view this post on Zulip Yury G. Kudryashov (Dec 24 2019 at 01:11):

Is it possible to trace unfolding of definitions?

view this post on Zulip Yury G. Kudryashov (Dec 24 2019 at 01:11):

I don't see any definitions to unfold here.

view this post on Zulip 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

view this post on Zulip Joe (Dec 24 2019 at 01:14):

I think this should fix it.

view this post on Zulip Joe (Dec 24 2019 at 01:15):

Lean cannot find the function d in dist_le_tsum_of_dist_le_of_tendsto

view this post on Zulip Yury G. Kudryashov (Dec 24 2019 at 01:18):

Thanks @Joe!

view this post on Zulip Joe (Dec 24 2019 at 01:19):

No problem.

view this post on Zulip 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?

view this post on Zulip Jesse Michael Han (Dec 24 2019 at 04:02):

try enabling the profiler

view this post on Zulip Yury G. Kudryashov (Dec 24 2019 at 04:06):

lean --profile --json reports ... took ... s once for each begin ... end block.

view this post on Zulip Yury G. Kudryashov (Dec 24 2019 at 04:06):

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

view this post on Zulip 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