Zulip Chat Archive

Stream: new members

Topic: slow reduction


view this post on Zulip Scott Olson (Sep 28 2018 at 00:26):

I have a #reduce that's leading to "(deterministic) timeout" and I'm wondering what I can do to find out what's taking so long. Can I #reduce step-by-step?

view this post on Zulip Mario Carneiro (Sep 28 2018 at 00:46):

Unfortunately no. #reduce is not really intended for serious use

view this post on Zulip Mario Carneiro (Sep 28 2018 at 00:46):

It turns out that unfolding a proof down to axioms is actually kind of expensive :)

view this post on Zulip Scott Olson (Sep 28 2018 at 00:48):

Hmm, well it's also breaking my examples/tests, since it can't even prove things by rfl at very small input sizes, and I can't figure out why, because the code seems fairly straightforward.

view this post on Zulip Mario Carneiro (Sep 28 2018 at 00:49):

this is also not unusual

view this post on Zulip Mario Carneiro (Sep 28 2018 at 00:49):

I think theorem nat.prime 5 := dec_trivial times out

view this post on Zulip Mario Carneiro (Sep 28 2018 at 00:50):

it depends on what numerical functions you are calling

view this post on Zulip Scott Olson (Sep 28 2018 at 00:50):

I guess it would be nice to have bytecode-based tests for quick dumb sanity checks

view this post on Zulip Mario Carneiro (Sep 28 2018 at 00:51):

You should use #eval for that

view this post on Zulip Scott Olson (Sep 28 2018 at 00:51):

I do, I just wish I could write something that asserts on the result rather than simply printing it

view this post on Zulip Mario Carneiro (Sep 28 2018 at 01:06):

you can use run_cmd:

run_cmd guard (2 + 2 = 4)
run_cmd guard (2 + 2 = 5) -- failed

view this post on Zulip Scott Olson (Sep 28 2018 at 01:07):

Perfect, thanks!


Last updated: May 14 2021 at 05:20 UTC