Email Gateway (May 20 2022 at 21:00): Email Gateway (May 20 2022 at 21:00):From: Manuel Eberl <manuel@pruvisto.org>
Hello,
I am currently working on a project where I have to plug a lot of
theorems together (using Thm.implies_elim). "A lot" is about 6 million.
I noticed that the larger propositions of the theorems get, the slower
everything gets. One optimisation I therefore did was to introduce local
definitions (with Local_Defs.define).
I then noticed that a lot of time was being spent taking care of the
hyps of the theorems when they are combined, so I did some preprocessing
to make sure that the "hyps" lists of all the theorems are
pointer-equal. That already helped a lot.
Now it seems that the majority (60%) of the time is spent in these two
functions:
13627 Proofterm.thm_ord-(2)
17530 Ord_List.union(3)unio(2)
I suspect that these both come from Proofterm.unions_thms, which in turn
probably comes from "Proofterm.fulfill_norm_proof".
Is there anything I can do to make this any faster?
If not, it's not a deal breaker (the code is still acceptably fast), but
I was still a bit perplexed at the factor 14 slowdown I got when I used
actual terms instead of just dummy variables for everything…
Cheers,
Manuel
Last updated: Apr 16 2024 at 16:19 UTC