From 64da00694c65af10da343f8ffad4a0088c8bb845 Mon Sep 17 00:00:00 2001 From: David Aspinall Date: Wed, 18 Aug 2010 11:19:04 +0000 Subject: Clean flag settings for profiling. Add AHundredProofs. --- isar/isar-profiling.el | 14 ++++++-------- 1 file changed, 6 insertions(+), 8 deletions(-) (limited to 'isar/isar-profiling.el') diff --git a/isar/isar-profiling.el b/isar/isar-profiling.el index 22777c5b..8984f1b0 100644 --- a/isar/isar-profiling.el +++ b/isar/isar-profiling.el @@ -12,8 +12,9 @@ (require 'proof-site) (proof-ready-for-assistant 'isar)) -(declare-function isar-tracing:auto-quickcheck-toggle "isar.el") (declare-function isar-tracing:auto-solve-toggle "isar.el") +(declare-function isar-tracing:auto-quickcheck-toggle "isar.el") +(declare-function isar-proof:parallel-proofs-toggle "isar.el") (require 'pg-autotest) (require 'pg-dev) @@ -26,8 +27,8 @@ (pg-autotest-find-file "etc/isar/AHundredTheorems.thy") (pg-autotest eval (proof-shell-ready-prover)) - (pg-autotest eval (isar-tracing:auto-quickcheck-toggle 0)) (pg-autotest eval (isar-tracing:auto-solve-toggle 0)) ; autosolve hammers this! + (pg-autotest eval (isar-tracing:auto-quickcheck-toggle 0)) (pg-autotest eval (isar-proof:parallel-proofs-toggle 0)) (pg-autotest eval (proof-full-annotation-toggle 0)) (proof-shell-wait) @@ -36,12 +37,6 @@ (pg-autotest timestart) (pg-autotest process-wholefile "etc/isar/AHundredTheorems.thy") (pg-autotest timetaken) - (pg-autotest timestart) - (pg-autotest process-wholefile "etc/isar/AHundredTheorems.thy") - (pg-autotest timetaken) - (pg-autotest timestart) - (pg-autotest process-wholefile "etc/isar/AHundredTheorems.thy") - (pg-autotest timetaken) ;; Same again with profiling (profile-pg) @@ -51,6 +46,9 @@ (pg-autotest timestart) (pg-autotest process-wholefile "etc/isar/AHundredTheorems.thy") (pg-autotest timetaken) + (pg-autotest timestart) + (pg-autotest process-wholefile "etc/isar/AHundredProofs.thy") + (pg-autotest timetaken) (elp-results) (let ((results (with-current-buffer "*ELP Profiling Results*" -- cgit v1.2.3