Log tactic timings - Githubissues

au-ts / cogent

Cogent Project

https://trustworthy.systems/projects/TS/cogent.pml

Other

158 stars 26 forks source link

Log tactic timings #353

Closed emmet-m closed 4 years ago

emmet-m commented 4 years ago

Introduces timing logging to the Isabelle TypeProof tactics.

Enabled via the --type-proof-timing flag, will create a new file called TypeProofTactic.json next to the generated TypeProof.thy file, which can be fed into cogent/scripts/generate_tactic_statistics.py and after cogent/scripts/plotTacticTimingData.gnuplot to print statistics and graphs of tactic time usage.

zilinc commented 4 years ago

It looks good to me. When shall we merge? Are you waiting for any regression tests to pass or someone to review?

emmet-m commented 4 years ago

Happy to merge now, just wanted to see the tests pass!

zilinc commented 4 years ago

@emmet-m It has conflicts so I'll leave it to you :P