Zulip Chat Archive

Stream: general

Topic: timeout


Kenny Lau (Nov 08 2018 at 21:15):

theorem is_noetherian_ring_mv_polynomial_fin {n : }
  (hnr : is_noetherian_ring R) : is_noetherian_ring (mv_polynomial (fin n) R) :=
begin
try_for 4000 {
  induction n with n ih,
  { refine is_noetherian_ring_of_equiv R _ _ hnr,
    { exact (mv_polynomial.pempty_equiv.symm.trans $ mv_polynomial.equiv_of_equiv
      pempty.elim, fin.elim0, λ x, pempty.elim x, λ x, fin.elim0 x) },
    { dsimp only [equiv.trans, equiv.symm, equiv.coe_fn_mk],
      exact @@is_ring_hom.comp _ _ _
        (mv_polynomial.C.is_ring_hom) _ _
        (@@mv_polynomial.eval₂.is_ring_hom _ _ _ _ _
          (mv_polynomial.C : R  mv_polynomial (fin 0) R) mv_polynomial.C.is_ring_hom
          (mv_polynomial.X  pempty.elim : pempty  mv_polynomial (fin 0) R)) } },
}, try_for 100000 {
  refine is_noetherian_ring_of_equiv (polynomial (mv_polynomial (fin n) R)) _ _ (is_noetherian_ring_polynomial ih),
  { exact mv_polynomial.option_equiv.symm.trans (mv_polynomial.equiv_of_equiv
      ⟨λ x, option.rec_on x 0 fin.succ, λ x, fin.cases none some x,
      by rintro none | x⟩; [refl, exact fin.cases_succ _],
      λ x, fin.cases rfl (λ i, show (option.rec_on (fin.cases none some (fin.succ i) : option (fin n))
        0 fin.succ : fin n.succ) = _, by rw fin.cases_succ) x) },
  { dsimp only [equiv.trans, equiv.symm, equiv.coe_fn_mk],
    exact is_ring_hom.comp _ _ }
}
end

Kenny Lau (Nov 08 2018 at 21:15):

Even 100 seconds is not enough

Kenny Lau (Nov 08 2018 at 21:15):

@Mario Carneiro I don't really know how to deal with this

Kenny Lau (Nov 08 2018 at 21:21):

(it's from https://github.com/leanprover/mathlib/pull/461/commits/b3f1efbe02638a2793b48e9a28a1d8f0df371690#diff-1f7cb4d661f00b6d887925434b41ad5dR286)

Kenny Lau (Nov 08 2018 at 22:49):

https://github.com/leanprover/mathlib/pull/461/commits/f80e9fce6b081cf26f551b3ae2e5c83327f9bd59#diff-1f7cb4d661f00b6d887925434b41ad5dR293

Kenny Lau (Nov 08 2018 at 22:49):

@Mario Carneiro more ridiculousness

Kenny Lau (Nov 09 2018 at 08:42):

@Sebastian Ullrich what do you think about this?

Sebastian Ullrich (Nov 09 2018 at 08:43):

not much

Mario Carneiro (Nov 09 2018 at 08:44):

good idea

Kenny Lau (Nov 09 2018 at 09:17):

I think it's a serious problem if I provided every implicit argument and it still takes 16 seconds to elaborate

Kenny Lau (Nov 09 2018 at 10:25):

I basically changed the definitions of polynomial and mv_polynomial and that cut down 6 seconds

Kevin Buzzard (Nov 09 2018 at 12:24):

Kenny can you make a MWE? It's hard to run your code.

Yaël Dillies (Jul 31 2021 at 15:04):

I got a timeout working on #8471, for no apparent reason: https://github.com/leanprover-community/mathlib/runs/3209267335
I'll just rerun the job, but please tell me if I actually did something wrong.

Bryan Gin-ge Chen (Jul 31 2021 at 15:28):

There might just be a slow proof at ring_theory/ideal/basic.lean:599:9 which is pushed over the limit by a change in imports?

Yaël Dillies (Jul 31 2021 at 15:36):

Yeah, probably

Eric Wieser (Jan 13 2023 at 15:36):

Bors is failing due to a timeout in ring_theory.is_tensor_product; presumably not due to a PR in the queue

David Loeffler (Jan 13 2023 at 15:52):

Maybe an effect of #18121 or #18140 (both merged yesterday, both involving tensor products)?

Eric Wieser (Jan 13 2023 at 15:53):

Possibly

Eric Wieser (Jan 13 2023 at 19:33):

#18169 helps a little, but not much

Eric Wieser (Jan 13 2023 at 22:42):

I won't have much time for Lean over the weekend; I think the queue might get quite stuck without a speedup there. Looking at the failure history, it's not obvious that #18121 or #18140 are related

Eric Wieser (Jan 13 2023 at 22:42):

I'm happy for anyone to push speedups to that PR

Eric Wieser (Jan 14 2023 at 08:18):

Thanks @Junyan Xu!

Yaël Dillies (Mar 01 2023 at 15:15):

#18529 for a timeout in analysis.inner_product_space.basic

Jireh Loreaux (Mar 01 2023 at 15:18):

I put it on the maintainer merge queue.

Yaël Dillies (Mar 18 2023 at 15:34):

#18614 for a timeout in group_theory.torsion

Yaël Dillies (Mar 23 2023 at 16:48):

docs#measure_theory.Lp.simple_func.normed_space times out. I couldn't fix it.

Eric Wieser (Mar 23 2023 at 21:58):

Where are you getting the timeout?

Eric Wieser (Mar 23 2023 at 21:58):

It's slow on master but doesn't seem disastrously so

Yaël Dillies (Mar 23 2023 at 21:59):

On the very innocent #18635

Eric Wieser (Mar 23 2023 at 22:05):

I would guess that the fact simple_func is a subgroup of Lp which is itself a subgroup of ae_eq_fun which is a quotient of a subtype is possibly causing some of the slowness

Eric Wieser (Mar 23 2023 at 22:05):

simple_func could just be a subgroup of ae_eq_fun

Eric Wieser (Mar 23 2023 at 22:16):

Hmm, I tried that and its not pleasant


Last updated: Dec 20 2023 at 11:08 UTC