Zulip Chat Archive

Stream: triage

Topic: issue #3097: `squeeze_simp` produces invalid result


view this post on Zulip Random Issue Bot (Nov 05 2020 at 14:16):

Today I chose issue 3097 for discussion!

squeeze_simp produces invalid result
Created by @Gabriel Ebner (@gebner) on 2020-06-17
Labels: bug, meta

Is this issue still relevant? Any recent updates? Anyone making progress?

view this post on Zulip Gabriel Ebner (Nov 05 2020 at 14:19):

I'd be happy to close this as wontfix, blocked-on-:lucky: since nobody runs into this accidentally from what it seems.

view this post on Zulip Johan Commelin (Nov 05 2020 at 14:24):

How hard would it be to make squeeze_simp use the lemmas that set_option trace.simplify.rewrites lists?

view this post on Zulip Johan Commelin (Nov 05 2020 at 14:24):

I guess that needs changes to the C++. But is it hard?

view this post on Zulip Gabriel Ebner (Nov 05 2020 at 14:29):

Main issue is that there's no way to get trace messages from the Lean side at the moment.

view this post on Zulip Gabriel Ebner (Nov 05 2020 at 14:30):

But if you're doing that, you might as well have the C++ record the list of lemmas used and return that.

view this post on Zulip Johan Commelin (Nov 05 2020 at 14:36):

Just to be clear: I don't think this is something that I can do. I'm just wondering how hard it is to get those trace messages from within the tactic state. Does it mean changing 5 lines of C++ or 500? Or even 5000?

view this post on Zulip Gabriel Ebner (Nov 05 2020 at 14:53):

Between 5-50, I'd guess.

view this post on Zulip Johan Commelin (Nov 05 2020 at 14:58):

Ok, I think that could (i) make squeeze_simp more reliable, and (ii) give it a significant speed-up.

(ii), because as I understand it, currently squeeze_simp is quadratic in the number of lemmas that are used, and this change would just drop that part completely.

view this post on Zulip Patrick Massot (Nov 05 2020 at 15:14):

Can anyone recommend a good C++ book to Johan?

view this post on Zulip Johan Commelin (Nov 05 2020 at 15:16):

/me is using >50% of his work week on teaching, another 20% on seminars, another 20% on reviewing PRs.... so there is 5-10% left for research...

view this post on Zulip Johan Commelin (Nov 05 2020 at 15:17):

/me :sad:

view this post on Zulip Simon Hudon (Nov 05 2020 at 15:26):

You could start here: https://www.codecademy.com/learn/learn-c-plus-plus

view this post on Zulip Simon Hudon (Nov 05 2020 at 15:26):

And this book looks good to me but I haven't used it: link

view this post on Zulip Johan Commelin (Nov 09 2020 at 21:59):

lean#497

view this post on Zulip Johan Commelin (Nov 09 2020 at 21:59):

/me has to go back to teaching Lie algebras now

view this post on Zulip Random Issue Bot (Dec 19 2020 at 14:26):

Today I chose issue 3097 for discussion!

squeeze_simp produces invalid result
Created by @Gabriel Ebner (@gebner) on 2020-06-17
Labels: bug, meta

Is this issue still relevant? Any recent updates? Anyone making progress?


Last updated: May 09 2021 at 15:11 UTC