Zulip Chat Archive

Stream: general

Topic: slow polynomial

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

Kenny Lau (Apr 07 2020 at 08:17):

why does this time out?

Kenny Lau (Apr 07 2020 at 08:17):

I thought making polynomial classical solved all polynomial problems

Kenny Lau (Apr 07 2020 at 08:26):

@Mario Carneiro

Mario Carneiro (Apr 07 2020 at 08:27):

it didn't

Johan Commelin (Apr 07 2020 at 08:29):

That's a tragic timeout

Kenny Lau (Apr 07 2020 at 08:30):

@Mario Carneiro how long does it take for you?

Kevin Buzzard (Apr 07 2020 at 08:30):

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

Kenny Lau (Apr 07 2020 at 08:30):

so let's call it a timeout

Kevin Buzzard (Apr 07 2020 at 08:31):

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

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

Yury G. Kudryashov (Apr 07 2020 at 08:33):

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

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?

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.

Yury G. Kudryashov (Apr 08 2020 at 04:43):

Working on perfect_closure now.

Last updated: Dec 20 2023 at 11:08 UTC