Zulip Chat Archive

Stream: general

Topic: bors build failure


view this post on Zulip Kyle Miller (Oct 06 2020 at 07:13):

Bors has failed building #4444 twice now, and it seems to be a deterministic timeout in mv_polynomial. The PR touches control/traversable, but only by adding documentation and reordering a definition.

/home/runner/work/mathlib/mathlib/src/data/mv_polynomial/basic.lean:414:0: error: (deterministic) timeout

view this post on Zulip Bryan Gin-ge Chen (Oct 06 2020 at 07:16):

I guess the first thing to do is to try merging master on that branch and letting the CI run

view this post on Zulip Bryan Gin-ge Chen (Oct 06 2020 at 07:20):

Here’s the line referenced in the error: https://github.com/leanprover-community/mathlib/blob/523bddb4f0cbfdc401b3b2f943ca6eba92ad90cc/src/data/mv_polynomial/basic.lean#L414

view this post on Zulip Kyle Miller (Oct 06 2020 at 07:25):

Ok, I've merged master and pushed it. Is the CI just to see if it can still build?

view this post on Zulip Johan Commelin (Oct 06 2020 at 07:26):

I'm having the same issue with #4461

view this post on Zulip Johan Commelin (Oct 06 2020 at 07:28):

The problem is coeff_mul

view this post on Zulip Johan Commelin (Oct 06 2020 at 07:29):

It's known to be slow... I guess we need to work on it

view this post on Zulip Kyle Miller (Oct 06 2020 at 07:32):

So it's not @Aaron Anderson's docstrings that broke the build? :upside_down:

view this post on Zulip Kyle Miller (Oct 06 2020 at 07:47):

Is the deterministic timeout actually nondeterministic? (at least when it comes to building all of mathlib?) It seems sort of improbable that a commit with only documentation comments would change much...

view this post on Zulip Bryan Gin-ge Chen (Oct 06 2020 at 07:59):

Yeah, I'm not sure what deterministic really means here. For what it's worth, I ran lean --make src/data/mv_polynomial/basic.lean on the #4444 branch of mathlib and didn't get a timeout when opening the file in VS Code, even though it should be enforcing the same -T100000 limit.

According to the profiler, the tactic execution in mv_polynomial.coeff_mul is taking 19.7 seconds, so it's definitely ripe for reworking. I don't know how to interpret the more detailed output though:

elaboration: tactic execution took 19.7s
num. allocated objects:  7835
num. allocated closures: 10779
19748ms   100.0%   tactic.istep
19748ms   100.0%   _interaction
19748ms   100.0%   tactic.istep._lambda_1
19748ms   100.0%   scope_trace
19748ms   100.0%   _interaction._lambda_2
19748ms   100.0%   tactic.step
19667ms    99.6%   tactic.solve1
19525ms    98.9%   _interaction._lambda_19
19140ms    96.9%   tactic.interactive.propagate_tags
18716ms    94.8%   interaction_monad_orelse
18665ms    94.5%   _interaction._lambda_17
18615ms    94.3%   tactic.interactive.simp_core
18554ms    94.0%   tactic.interactive.simp_core_aux
18550ms    93.9%   tactic.simplify
18550ms    93.9%   tactic.try
18502ms    93.7%   tactic.interactive.simpa._lambda_6
18501ms    93.7%   tactic.interactive.simpa
17747ms    89.9%   tactic.simp_target
17747ms    89.9%   tactic.interactive.simp_core_aux._lambda_5
13118ms    66.4%   _interaction._lambda_16
13061ms    66.1%   _interaction._lambda_14
 5162ms    26.1%   _interaction._lambda_10
 1697ms     8.6%   interaction_monad.monad._lambda_9
  807ms     4.1%   tactic.interactive.simp_core_aux._lambda_4
  807ms     4.1%   tactic.interactive.simp_core_aux._lambda_2
  525ms     2.7%   rw_core
  524ms     2.7%   interactive.loc.apply
  521ms     2.6%   interaction_monad.orelse'
  492ms     2.5%   _private.3291397495.rw_goal._lambda_4
  481ms     2.4%   _private.3291397495.rw_goal._lambda_2
  415ms     2.1%   tactic.rewrite_target
  415ms     2.1%   tactic.rewrite
  414ms     2.1%   tactic.rewrite_core
  368ms     1.9%   tactic.mk_instance
  287ms     1.5%   _interaction._lambda_12
  286ms     1.4%   tactic.apply_instance
  268ms     1.4%   tactic.all_goals'
  268ms     1.4%   all_goals'_core
  268ms     1.4%   _private.3677394557.all_goals'_core._main._lambda_2
  268ms     1.4%   tactic.to_expr
  235ms     1.2%   _interaction._lambda_18
  147ms     0.7%   _interaction._lambda_7
  142ms     0.7%   _interaction._lambda_4
  139ms     0.7%   tactic.interactive.have._lambda_1
   99ms     0.5%   tactic.interactive.concat_tags._lambda_5
   98ms     0.5%   repeat_aux
   98ms     0.5%   tactic.try_core
   98ms     0.5%   tactic.repeat
   98ms     0.5%   _interaction._lambda_3
   98ms     0.5%   _private.1616170719.repeat_aux._main._lambda_1
   94ms     0.5%   _interaction._lambda_11
   93ms     0.5%   tactic.interactive.by_cases._lambda_2
   93ms     0.5%   tactic.interactive.by_cases
   84ms     0.4%   tactic.interactive.to_expr'
   83ms     0.4%   tactic.by_cases
   59ms     0.3%   tactic.mk_simp_set_core
   59ms     0.3%   tactic.mk_simp_set
   57ms     0.3%   tactic.interactive.convert
   57ms     0.3%   tactic.focus1
   54ms     0.3%   tactic.congr'
   52ms     0.3%   _interaction._lambda_13
   39ms     0.2%   _interaction._lambda_8
   39ms     0.2%   simp_lemmas.add_pexpr
   39ms     0.2%   simp_lemmas.append_pexprs
   39ms     0.2%   tactic.mk_simp_set_core._lambda_5
   36ms     0.2%   tactic.apply_eq_congr_core
   36ms     0.2%   tactic.congr_core'
   35ms     0.2%   tactic.congr'._main._lambda_3
   32ms     0.2%   tactic.mk_specialized_congr_lemma
   31ms     0.2%   rw_hyp
   30ms     0.2%   _private.859230899.rw_hyp._main._lambda_3
   23ms     0.1%   _private.859230899.rw_hyp._main._lambda_2
   23ms     0.1%   tactic.apply_core
   21ms     0.1%   tactic.rewrite_hyp
   21ms     0.1%   _interaction._lambda_5
   20ms     0.1%   tactic.seq'
   18ms     0.1%   tactic.join_user_simp_lemmas
   18ms     0.1%   simp_lemmas.mk_default
   17ms     0.1%   relation_tactic
   17ms     0.1%   _interaction._lambda_6
   16ms     0.1%   _private.1624076617.relation_tactic._lambda_1
   16ms     0.1%   tactic.exact
   15ms     0.1%   tactic.congr'._main._lambda_4
   14ms     0.1%   tactic.replace_target
   10ms     0.1%   tactic.interactive.simpa._lambda_1
   10ms     0.1%   tactic.replace_hyp
   10ms     0.1%   _private.3291397495.rw_goal._lambda_3
    9ms     0.0%   tactic.save_info_with_widgets
    8ms     0.0%   tactic.apply
    8ms     0.0%   tactic.mk_eq_mpr
    8ms     0.0%   tactic.save_widget
    7ms     0.0%   tactic.save_type_info
    6ms     0.0%   tactic.assert
    6ms     0.0%   tactic.interactive.apply._lambda_1
    5ms     0.0%   tactic.assumption._lambda_1
    5ms     0.0%   tactic.find_same_type
    5ms     0.0%   tactic.refine
    4ms     0.0%   tactic.apply_congr_core
    4ms     0.0%   tactic.mk_eq_mp
    3ms     0.0%   tactic.rintro
    3ms     0.0%   tactic.find_same_type._main._lambda_1
    3ms     0.0%   simp_lemmas.resolve_and_add
    3ms     0.0%   tactic.unify
    3ms     0.0%   tactic.assert_core
    3ms     0.0%   _private.3676539765.simp_lemmas.resolve_and_add._lambda_2
    3ms     0.0%   tactic.interactive.rintro
    3ms     0.0%   tactic.infer_type
    3ms     0.0%   tactic.rintro._lambda_3
    3ms     0.0%   simp_lemmas.add_simp
    2ms     0.0%   tactic.mk_app
    2ms     0.0%   simp_lemmas.erase
    2ms     0.0%   tactic.rcases_core._main._lambda_5
    2ms     0.0%   tactic.interactive.exact
    2ms     0.0%   tactic.rcases_core._main._lambda_9
    2ms     0.0%   tactic.rcases_core
    2ms     0.0%   tactic.mk_id_eq
    2ms     0.0%   tactic.rcases.continue
    2ms     0.0%   tactic.cases_core
    2ms     0.0%   _interaction._lambda_9
    1ms     0.0%   tactic.has_opt_auto_param._lambda_2
    1ms     0.0%   tactic.clear_goals._lambda_5
    1ms     0.0%   tactic.apply_congr_core._lambda_1
    1ms     0.0%   tactic.applyc
    1ms     0.0%   tactic.mk_const
    1ms     0.0%   tactic.has_opt_auto_param_for_apply._lambda_2
    1ms     0.0%   tactic.intro_core
    1ms     0.0%   tactic.get_eqn_lemmas_for
    1ms     0.0%   tactic.i_to_expr_for_apply
    1ms     0.0%   tactic.interactive.get_rule_eqn_lemmas
    1ms     0.0%   tactic.clear
    1ms     0.0%   format.join
    1ms     0.0%   environment.get_ext_eqn_lemmas_for
    1ms     0.0%   tactic.interactive.dsimp
    1ms     0.0%   tactic.save_info_thunk
    1ms     0.0%   tactic.dsimp_target
    1ms     0.0%   tactic.interactive.get_rule_eqn_lemmas._lambda_3
    1ms     0.0%   tactic.clear_goals
    1ms     0.0%   tactic.assertv
    1ms     0.0%   expr.get_app_fn
    1ms     0.0%   resolve_name'
    1ms     0.0%   tactic.clear'
    1ms     0.0%   expr.is_napp_of
    1ms     0.0%   list.foldl
    1ms     0.0%   tactic.mk_const._lambda_1
    1ms     0.0%   tactic.intro
    1ms     0.0%   expr.const
    1ms     0.0%   simp_lemmas.dsimplify
    1ms     0.0%   format.compose
    1ms     0.0%   expr.is_app_of
    1ms     0.0%   tactic.swap
    1ms     0.0%   tactic.instantiate_mvars
    1ms     0.0%   _interaction._lambda_15
    1ms     0.0%   tactic.assertv_core
    1ms     0.0%   tactic.congr'._main._lambda_2

view this post on Zulip Scott Morrison (Oct 06 2020 at 08:03):

I think that is saying simpa is the culprit.

view this post on Zulip Bryan Gin-ge Chen (Oct 06 2020 at 08:05):

Indeed, changing the two simpas to simpa only speeds it up to 2.64 seconds!

view this post on Zulip Johan Commelin (Oct 06 2020 at 08:07):

I almost have a PR ready

view this post on Zulip Johan Commelin (Oct 06 2020 at 08:07):

I'm restructuring it a bit more

view this post on Zulip Bryan Gin-ge Chen (Oct 06 2020 at 08:08):

Ah, OK. I was just about to submit one myself (with just the simpa only change).

view this post on Zulip Johan Commelin (Oct 06 2020 at 08:10):

#4469

view this post on Zulip Johan Commelin (Oct 06 2020 at 08:10):

It's below 2s on my box now

view this post on Zulip Scott Morrison (Oct 06 2020 at 08:21):

oops, I did it as well...

view this post on Zulip Scott Morrison (Oct 06 2020 at 08:22):

I'll close.

view this post on Zulip Bryan Gin-ge Chen (Oct 06 2020 at 08:34):

Hmm, coeff_mul just caused the most recent bors batch to fail again: https://github.com/leanprover-community/mathlib/runs/1213623252

So maybe we should see if we can try and merge that first.

view this post on Zulip Johan Commelin (Oct 06 2020 at 08:36):

Yup, we might want to cancel everything, and squeeze this in first.

view this post on Zulip Bryan Gin-ge Chen (Oct 06 2020 at 08:43):

I just added #4469 to the queue. Even if the currently running batch fails, #4469 should be in the next batch and then everything should be good, I think.

view this post on Zulip Eric Wieser (Oct 06 2020 at 09:14):

bors r+ p=10 will give it higher priority

view this post on Zulip Bryan Gin-ge Chen (Oct 06 2020 at 09:16):

I considered doing that but since #4469 won't conflict with any of the other PRs, it should be more efficient just to have it run in a batch.

view this post on Zulip Bryan Gin-ge Chen (Oct 06 2020 at 09:18):

Also, the batch including #4469 is now running, since the batch that was running failed again. I went ahead and reconsolidated those PRs along with #4444 into a new batch.

view this post on Zulip Johan Commelin (Oct 06 2020 at 09:36):

#4472 is not critical for bors, but it brings coeff_mul down into the 1.0s - 1.2s range, and shortens the proof.


Last updated: May 08 2021 at 03:17 UTC