timeout

Stream: general

[Kenny Lau]

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]

Even 100 seconds is not enough

[Kenny Lau]

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

[Kenny Lau]

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

[Kenny Lau]

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

[Kenny Lau]

@Mario Carneiro more ridiculousness

[Kenny Lau]

@Sebastian Ullrich what do you think about this?

[Sebastian Ullrich]

not much

[Mario Carneiro]

good idea

[Kenny Lau]

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

[Kenny Lau]

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

[Kevin Buzzard]

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

[Yaël Dillies]

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]

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]

Yeah, probably

[Eric Wieser]

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

[David Loeffler]

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

[Eric Wieser]

Possibly

[Eric Wieser]

#18169 helps a little, but not much

[Eric Wieser]

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]

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

[Eric Wieser]

Thanks @Junyan Xu!

[Yaël Dillies]

#18529 for a timeout in analysis.inner_product_space.basic

[Jireh Loreaux]

I put it on the maintainer merge queue.

[Yaël Dillies]

#18614 for a timeout in group_theory.torsion

[Yaël Dillies]

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

[Eric Wieser]

Where are you getting the timeout?

[Eric Wieser]

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

[Yaël Dillies]

On the very innocent #18635

[Eric Wieser]

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]

simple_func could just be a subgroup of ae_eq_fun

[Eric Wieser]

Hmm, I tried that and its not pleasant