Skip to content

HTTPS clone URL

Subversion checkout URL

You can clone with HTTPS or Subversion.

Download ZIP
A Coq plugin that allows a user to start and stop timers.
OCaml Coq
branch: master

Fetching latest commit…

Cannot retrieve the latest commit at this time

Failed to load latest commit information.
src
test-suite
.gitignore
Makefile
README
arguments.txt

README

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).  



Something went wrong with that request. Please try again.