mv_polynomial

Stream: maths

[Chris Hughes]

I'm considering an mv_polynomial refactor to get rid of the slow elaboration problems. @Kenny Lau what are the problems?

[Kenny Lau]

@Chris Hughes no idea at all. Lean doesn't have the greatest debugging tools.

[Kenny Lau]

but if you want some indicators, you can look at how slow pempty_ring_equiv is

[Kenny Lau]

and the related lemmas

[Andrew Ashworth]

if you're highly motivated you can build your own version of lean and step though / profile the C++ code

[Andrew Ashworth]

would not recommend unless you want to learn a lot about computer programming

[Chris Hughes]

I had a bit of a play around. Changing all the Type*s to Type approximately halved the time, but it's still slow.

[Kenny Lau]

if you're highly motivated you can build your own version of lean and step though / profile the C++ code

so you mean, Lean doesn't have good debugging tools, and won't have, and if I want to debug I should go through a lot of pain

[Andrew Ashworth]

This is why I mentioned the highly motivated part