Separate profiling from testing

2 files changed, 70 insertions, 6 deletions

diff --git a/isar/isar-autotest.el b/isar/isar-autotest.el
index cc3d6640..398b6942 100644
--- a/isar/isar-autotest.el
+++ b/isar/isar-autotest.el
@@ -27,11 +27,16 @@
   (pg-autotest script-wholefile "isar/Example.thy")
   (pg-autotest script-wholefile "isar/Example-Tokens.thy")
 
-  (pg-autotest remark "Testing random jumps")
+  (pg-autotest remark "Larger files...")
   (pg-autotest eval (isar-tracing:auto-quickcheck-toggle 0))
   (pg-autotest eval (isar-tracing:auto-solve-toggle 0)) ; autosolve hammers this!
+  (pg-autotest eval (proof-full-annotation-toggle 0))
+  (pg-autotest script-wholefile "etc/isar/AHundredTheorems.thy")
+  (pg-autotest script-wholefile "isar/ex/Tarski.thy")
+
+  (pg-autotest remark "Testing random jumps")
   (pg-autotest script-randomjumps "isar/Example.thy" 5)
-  (pg-autotest script-randomjumps "etc/isar/AHundredTheorems.thy" 10)
+  (pg-autotest script-randomjumps "isar/ex/Tarski.thy" 10) ; better test?
 
   (pg-autotest remark "Testing restarting the prover")
   (pg-autotest quit-prover)
@@ -40,10 +45,6 @@
   (pg-autotest eval (proof-unicode-tokens-toggle))
   (pg-autotest script-wholefile "isar/Example-Tokens.thy")
 
-  (pg-autotest remark "A larger file:")
-  (pg-autotest timestart)
-  (pg-autotest script-wholefile "isar/ex/Tarski.thy")
-  (pg-autotest timetaken)
 
   (pg-autotest remark	         "Simple test of multiple file behaviour:")
   (pg-autotest script-wholefile  "etc/isar/multiple/C.thy")
diff --git a/isar/isar-profiling.el b/isar/isar-profiling.el
new file mode 100644
index 00000000..1f648628
--- /dev/null
+++ b/isar/isar-profiling.el
@@ -0,0 +1,63 @@
+;; isar-profiling.el: simple profiling Isar Proof General.
+;;
+;; You can run these tests by issuing "make profile.isar" in PG home dir.
+;;
+;; $Id$
+;;
+
+(eval-when-compile
+  (require 'cl))
+
+(eval-when (compile)
+  (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")
+
+(require 'pg-autotest)
+
+(unless noninteractive
+
+  (pg-autotest log ".profile.log")  ; convention
+
+  (pg-autotest timestart 'total)
+
+  (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 (proof-full-annotation-toggle 0))
+  (proof-shell-wait)
+
+  ;; Simple profiling test.  Cf TRAC #324
+  (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
+  (elp-instrument-package "proof")
+  (elp-instrument-package "pg")
+  (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)
+  (elp-results)
+  (let ((results 
+	 (with-current-buffer "*ELP Profiling Results*"
+	   (buffer-string))))
+    (with-current-buffer pg-autotest-log
+      (goto-char (point-min))
+      (insert "ELP Profiling Results: \n" results "\n\n")))
+
+  (pg-autotest exit)
+
+  )