-
Notifications
You must be signed in to change notification settings - Fork 83
New issue
Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.
By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.
Already on GitHub? Sign in to your account
Document how to debug slowness of the proof #3041
Comments
Hi @Kixunil , thanks for opening the issue!
Unfortunately, we don't have at the moment any documentation or resources to help debugging slow harnesses. What follows is what we recommend doing in most cases:
I hope this helps you to figure out the source of the performances issues you're seeing. Also, if the code you're working on is or can be made public, feel free to open a bug report pointing to the specific branch/example so we can further advise. |
Thanks! I will look into it. I suspect loops are what made my private experiment slow. There's another public code we have that implements
Is there any way to do this that doesn't decrease the power of the proof? The linked issue suggests that it's better to just exhaustively test some values (bools?). |
Thanks for sharing your code! Please feel free to participate in issues related to slow operations or open new ones if they don't match your experience.
I can't think of any, assuming that "power" refers to the "generality" of the proof. But it's OK to decompose one proof into multiple harnesses (where one input gets fixed to a different value each time) to make the individual harnesses more efficient. Of course, the more general proof would be preferred in most cases, but that might not be feasible in some of them. |
The documentation says:
However I was not able to find any documentation on how to do such debugging. I've encountered some slow tests and would love to learn how to make them faster.
The text was updated successfully, but these errors were encountered: