slow reduction

Stream: new members

[Scott Olson]

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]

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

[Mario Carneiro]

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

[Scott Olson]

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]

this is also not unusual

[Mario Carneiro]

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

[Mario Carneiro]

it depends on what numerical functions you are calling

[Scott Olson]

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

[Mario Carneiro]

You should use #eval for that

[Scott Olson]

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

[Mario Carneiro]

you can use run_cmd:

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

[Scott Olson]

Perfect, thanks!