Feature request: proof script profiling

[msaaltink]

I have some proof scripts that take a very long time to run. It might be useful to have some way to find out which steps or which subgoals are taking the longest, as I could then try to make things run faster. It is hard to explore alternative scripts when it takes several minutes for each experiment, so some indication of where the hotspots are would be useful. Among the questions I might hope to answer are: Is my simpset inefficient? Am I unfolding too many names? Does my simplify step even accomplish anything? So, not exactly profiling (although timing would be useful), but some additional outputs when I want them, such as the list of names that are unfolded in a goal_eval, goal_eval_unint, or smt proving command, and maybe some idea of how much rewriting got done.

[robdockins]

Easy idea: have a version of time that works in the ProofScript monad, so at least you can do things like this manually

[kquick]

Various thoughts:

• Printing elapsed time since saw started may be more useful than absolute times for easier comparison of successive runs.
• Also elapsed time for just this step helps against previous step skew.
• Ability to call the print command in the middle of a proof would provide general usage as well as the timestamp via the top-level monad (may need to be able to force the thunk; most evaluation is strict, but not everywhere).
• Implicitly wrap each in time without needeing to modify the proof script (via the proof script monad).
• Also: nice to print out the current goal name to give a progress indication.