Footex needs revision #3271
Description
I would like footex to be revisioned or splitted into less time-draining theorems. Most of the reasoning is already explained in #3269. Here I provide a little bit of data.
I made a script that executes the commands:
SHOW PROOF <label> /COMPRESSED SHOW ELAPSED_TIME
For every theorem in main. From this I extracted the time-spans between two subsequent SHOW ELAPSED_TIME commands to get the duration of the corresponding show proof command.
This is the resulting graph. The x-axis represents the Nth theorem in main, while the y-axis shows the elapsed time (in seconds) from the previous SHOW ELAPSED_TIME command:
This doesn't show much... let's make it logarithmic instead:
That's better. In this one the y-axis represents the elapsed time expressed in centiseconds (so in this graph 100 means 1 second).
That big spike that you see towards the end is indeed footex. That means that I waited 3028.67 seconds before getting an answer from it, which is around 50 minutes. The big spike of footex appears for other commands as well such as prove <label> or for the minimize command (I chose show proof because it's the quickest to work with, but my guess it's that the elapsed times for these commands are correlated).
Thanks to my minimization in #3269 footex's proof decreased from 2178 to 2161 steps (in the compressed format, with wff and repeated steps included), and as I already mentioned I think they are not enough to explain its time-draining property. For the record the highest amount of steps in main belongs to theorem 2503lem2, which has 5279 of them (the website shows a smaller count because it doesn't include wff and repeated steps), but it required only 0.51 seconds to output show proof 2503lem2 /compressed.
So the properties that make some theorems more time-challenging than others are an open question to me, I'm looking forward to hear your thoughts about it.