Gaëtan Gilbert edited this page Apr 12, 2018 · 9 revisions


There are some hints here (dead link)

Try Typeclasses eauto.

Be careful with coercions. They're incredibly useful, but can lead to a great deal of unnecessary work during the convertibility check. Take a look at Print Graph and try to prune it down to the minimum amount you need.

Try using the abstract tactic.

Memory Consumption

See also this thread regarding memory consumption.

If you have your development in a single large file, try breaking it into multiple files.

Even if your machine has ample memory, reducing memory consumption can speed up proof checking (due to garbage collection?)

Opaque Proofs

The Opaque/Transparent distinction is important for keeping memory consumption under control. Subproofs wrapped in the abstract tactic and proofs which end with Qed are opaque; all others are transparent (unless made opaque with the Opaque command).

Clone this wiki locally
You can’t perform that action at this time.
You signed in with another tab or window. Reload to refresh your session. You signed out in another tab or window. Reload to refresh your session.
Press h to open a hovercard with more details.