trace a failed tidy

Stream: general

[Bhavik Mehta]

I'm getting a deterministic timeout with tidy, and I'm trying to diagnose why - is there a trace I can print? I can write the proof myself (it's short) but tidy times out... tidy? doesn't work because the tidy doesn't complete.

[Mario Carneiro]

You should be able to increase the timeout

[Bhavik Mehta]

Ah that would work. Thanks!

[Scott Morrison]

I usually see extremely bad performance from tidy when it does lots of case bashing on hypotheses. It you add local attribute [tidy] case_bash it gets way worse.

[Scott Morrison]

Does this sound like your situation? Perhaps there's a way of either making it faster, or otherwise more conservative about case bashing.

[Bhavik Mehta]

Yeah case bashing was in there

[Bhavik Mehta]

It was an idea I wasn't expecting to work anyway, I just wanted to figure out why exactly it didn't work