## Stream: new members

### Topic: slow reduction

#### 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?

#### Mario Carneiro (Sep 28 2018 at 00:46):

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

#### Mario Carneiro (Sep 28 2018 at 00:46):

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

#### 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.

#### Mario Carneiro (Sep 28 2018 at 00:49):

this is also not unusual

#### Mario Carneiro (Sep 28 2018 at 00:49):

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

#### Mario Carneiro (Sep 28 2018 at 00:50):

it depends on what numerical functions you are calling

#### Scott Olson (Sep 28 2018 at 00:50):

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

#### Mario Carneiro (Sep 28 2018 at 00:51):

You should use #eval for that

#### 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

#### 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


#### Scott Olson (Sep 28 2018 at 01:07):

Perfect, thanks!

Last updated: May 14 2021 at 05:20 UTC