Data-encoding: optimize proof time by using only 'Resolve' hints (!165) · Merge requests · Formal Land / Coq Tezos of OCaml 💫 · GitLab

Guillaume Claret requested to merge clarus@optimize-data-encoding-proofs into master Dec 13, 2021

@deepmindster This should optimize your MR https://gitlab.com/nomadic-labs/coq-tezos-of-ocaml/-/merge_requests/162 for the data-encoding part. This went from 25s on my machine to 5s for balance_encoding_is_valid. I found this change to do using https://coq.inria.fr/refman/proof-engine/ltac.html#profiling-ltac-tactics which showed that most of the time was spent on Hint Extern commands.