An example of Coq plugin that defines some custom timing tactics. This plugin has beem compiled succesfully with Coq 8.3-pl4 and 8.4 beta INSTALL ================= coq_makefile -f arguments.txt -o Makefile make make install USAGE ================= This plugin defines a few new tactics: - [start_timer n] (with n being an string) starts the timer [n] - [stop_timer n] (with n being an string) stops the timer [n] - [reset_timer n] (with n being an string) reset the timer [n] - [print_current_time] prints the current time of the day (as a floating poing number) - [time n tac] (with n being a string and tac a tactic) compute the times spent in tac, and add it to the timer n This plugin defines two new vernacular commands: - [Print Timing Profile] which iterates through all the defined timers, and print the time they have been running - [Clear Timing Profile] clears the global state A few notes: - this plugin uses a global state that is _not_ kept in sync when moving bottom up in a PG buffer - if a timer is started inside a tactic, which later fails, then the timer is not implicitely stopped Timer may be stopped and started multiple times (in the following example, we denote starting a timer by 'a' and stoping it by 'b'). - t1 : a; t2 : b will increment the number of runs by 1, the total time by t2 - t1, and the mean and variance accordingly - t1 : a; t2 : a; t3 : b; t4 : b will increment the number of runs by 2, the total time by (t3 - t2) + (t4 - t1), and the mean and variance accordingly - t1 : a; t2 : a; t3 : b is legal, will increment the number of runs by 1, the total time by (t3 - t2).