-
Notifications
You must be signed in to change notification settings - Fork 21
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
Improve the performance of the proofs in the Lean backend #250
Comments
I made some experiments with the proofs of the hashmap and the avl. Something I noticed is that by default the Generally speaking, I believe we need a general tactic to simplify the context, and I also made some measurements (before doing the modifications above). For instance, the graph below shows the accumulated time spent on evaluating the tactics of the proofs of the hashmap, when ranking the tactic times from the most expensive to the least expensive. There are some caveats (the times were printed with ![]() |
simp
A tactic which is also worth investigating is |
Another big issue is the theorems which use |
The proofs in the Lean backend are a bit slow for my taste. For instance, until recently, the proofs of the hashmap and the AVL took ~200s each, which is quite a lot. A more reasonable target (according to my intuition) would be less than a minute.
One issue for instance is the simplifier.
The simplifier can be slow at times especially when using
simp_all
in contexts with big goals. I did some preliminary diagnostics which indicate that it can sometimes perform up to ~10k simplification lemma attempts, which is not reasonable. We should investigate this.In parallel, this seems to indicate that
simp_all
is maybe not the best way of "blasting" a proof: for instance, I often use it when what I actually need to do is some sort of congruence closure. Maybe we should investigate other proof styles in consequence.The text was updated successfully, but these errors were encountered: