Zulip Chat Archive

Stream: general

Topic: slow polynomial


view this post on Zulip Kenny Lau (Apr 07 2020 at 08:17):

import data.polynomial

open polynomial

noncomputable def eval₂h {α β : Type} [comm_ring α] [comm_ring β] (i : α →+* β) (r : β) : polynomial α →+* β :=
ring_hom.of $ eval₂ i r

view this post on Zulip Kenny Lau (Apr 07 2020 at 08:17):

why does this time out?

view this post on Zulip Kenny Lau (Apr 07 2020 at 08:17):

I thought making polynomial classical solved all polynomial problems

view this post on Zulip Kenny Lau (Apr 07 2020 at 08:26):

@Mario Carneiro

view this post on Zulip Mario Carneiro (Apr 07 2020 at 08:27):

it didn't

view this post on Zulip Johan Commelin (Apr 07 2020 at 08:29):

That's a tragic timeout

view this post on Zulip Kenny Lau (Apr 07 2020 at 08:30):

@Mario Carneiro how long does it take for you?

view this post on Zulip Kevin Buzzard (Apr 07 2020 at 08:30):

It's taking a very long time for me but it gets there

view this post on Zulip Kenny Lau (Apr 07 2020 at 08:30):

so let's call it a timeout

view this post on Zulip Kevin Buzzard (Apr 07 2020 at 08:31):

on my nice fast desktop it's taking 14 seconds to elaborate

view this post on Zulip Mario Carneiro (Apr 07 2020 at 08:32):

I've been more or less reduced to bellowing THIS IS RIDICULOUS every time this issue comes up. I don't want to think about polynomials anymore

view this post on Zulip Yury G. Kudryashov (Apr 07 2020 at 08:33):

I think I added eval₂_hom to avoid something like this.

view this post on Zulip Johan Commelin (Apr 08 2020 at 04:40):

So what do we do about this slowness? Is "simply" bundling everything the solution, or is there something else that needs to be addressed?

view this post on Zulip Yury G. Kudryashov (Apr 08 2020 at 04:41):

I'm going to bundle all ring_homs soon. Let's see if this will help.

view this post on Zulip Yury G. Kudryashov (Apr 08 2020 at 04:43):

Working on perfect_closure now.


Last updated: May 10 2021 at 00:31 UTC