There's a chance we can get a decent speed improvement by avoiding several recomputations of hashes even for the simplest universes and expressions.
The caching can be achieved with RBMaps from the original Lean objects to their respective compilation results. We'd need, however, implementations of fast ordering instances for them.
Desirable: let's not use Lean's original hashes in the final version to avoid stacking risks of hash collisions
arthurpaulino
commented
2 years ago
There's a chance we can get a decent speed improvement by avoiding several recomputations of hashes even for the simplest universes and expressions.
The caching can be achieved with
RBMaps from the original Lean objects to their respective compilation results. We'd need, however, implementations of fast ordering instances for them.Desirable: let's not use Lean's original hashes in the final version to avoid stacking risks of hash collisions