Zulip Chat Archive

Stream: maths

Topic: mv_polynomial


view this post on Zulip Chris Hughes (Mar 02 2019 at 20:39):

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

view this post on Zulip Kenny Lau (Mar 02 2019 at 20:53):

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

view this post on Zulip Kenny Lau (Mar 02 2019 at 20:54):

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

view this post on Zulip Kenny Lau (Mar 02 2019 at 20:55):

and the related lemmas

view this post on Zulip Andrew Ashworth (Mar 02 2019 at 22:32):

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

view this post on Zulip Andrew Ashworth (Mar 02 2019 at 22:32):

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

view this post on Zulip Chris Hughes (Mar 02 2019 at 22:33):

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

view this post on Zulip Kenny Lau (Mar 02 2019 at 22:34):

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

view this post on Zulip Andrew Ashworth (Mar 02 2019 at 22:36):

This is why I mentioned the highly motivated part


Last updated: May 18 2021 at 07:19 UTC