Zulip Chat Archive

Stream: general

Topic: my_polynomial performance


view this post on Zulip Reid Barton (Nov 17 2018 at 19:03):

I tried proving that the polynomial ring functor is left adjoint to the forgetful functor CommRing -> Set but I gave up because doing anything with mv_polynomial was so slow. @Kenny Lau you were having similar problems with mv_polynomial right?
I think something is wrong there, but I couldn't figure out what.

view this post on Zulip Kenny Lau (Nov 17 2018 at 19:07):

yes, something is wrong

view this post on Zulip Kenny Lau (Nov 17 2018 at 19:07):

@Mario Carneiro what do you think?

view this post on Zulip Mario Carneiro (Nov 17 2018 at 23:37):

I think something is wrong

view this post on Zulip Kenny Lau (Nov 17 2018 at 23:40):

...

view this post on Zulip Mario Carneiro (Nov 17 2018 at 23:41):

my impression is that lean is having to solve enormous typeclass problems, I'm not sure if that's the whole problem

view this post on Zulip Kenny Lau (Nov 17 2018 at 23:42):

would you know specifically what is the problem with mv_polynomial and polynomial?

view this post on Zulip Mario Carneiro (Nov 17 2018 at 23:43):

if you look at the pp.all versions of any of the theorem statements, what looks like five tokens fills several pages

view this post on Zulip Kenny Lau (Nov 17 2018 at 23:44):

I don't think pp.all tells us all about the situation

view this post on Zulip Kenny Lau (Nov 17 2018 at 23:45):

but sure it tells us a lot

view this post on Zulip Mario Carneiro (Nov 17 2018 at 23:45):

yeah it doesn't know when to shut up


Last updated: May 08 2021 at 04:14 UTC