my_polynomial performance

Stream: general

[Reid Barton]

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.

[Kenny Lau]

yes, something is wrong

[Kenny Lau]

@Mario Carneiro what do you think?

[Mario Carneiro]

I think something is wrong

[Kenny Lau]

...

[Mario Carneiro]

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

[Kenny Lau]

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

[Mario Carneiro]

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

[Kenny Lau]

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

[Kenny Lau]

but sure it tells us a lot

[Mario Carneiro]

yeah it doesn't know when to shut up