From 35f05f9f85e02ff7f03f73d884983289c5f4bebb Mon Sep 17 00:00:00 2001
From: David Aspinall <da@inf.ed.ac.uk>
Date: Tue, 3 Aug 2010 23:08:39 +0000
Subject: Separate profiling from testing

---
 Makefile.devel         |  5 +++-
 isar/isar-autotest.el  | 13 ++++++-----
 isar/isar-profiling.el | 63 ++++++++++++++++++++++++++++++++++++++++++++++++++
 3 files changed, 74 insertions(+), 7 deletions(-)
 create mode 100644 isar/isar-profiling.el

diff --git a/Makefile.devel b/Makefile.devel
index dca47219..a9e9e881 100644
--- a/Makefile.devel
+++ b/Makefile.devel
@@ -213,6 +213,9 @@ tags:	$(EL) $(TAGS_EXTRAS)
 test.%:	
 	if [ -f "$*/$*-autotest.el" ]; then if $(EMACS) $(EMACSFLAGS) -l generic/proof-site.el $*/$*-autotest.el -f eval-current-buffer; then echo "Autotests for $* run successfully on `date`"; else cat $*/.autotest.log; echo "Autotests for $* ran with failures on `date`"; exit 1; fi; fi
 
+profile.%:	
+	if [ -f "$*/$*-profiling.el" ]; then if $(EMACS) $(EMACSFLAGS) -l generic/proof-site.el $*/$*-profiling.el -f eval-current-buffer; then echo "Profiling for $* run successfully on `date`"; else echo "Profiling for $* ran with failures on `date`"; exit 1; fi; cat $*/.profile.log; fi
+
 testall.%: 
 	for prover in ${PROVERS}; do $(MAKE) test.$$prover EMACS=$*; done
 
@@ -251,7 +254,7 @@ devclean: FORCE
 #
 distclean: devclean clean
 	@echo "***** CLEANING UP ALL JUNK FILES ****"
-	find . \( -name '*~' -o -name '#*#' -o -name '\.\#*' \) -print | xargs rm -f
+	find . \( -name '*~' -o -name '#*#' -o -name '\.\#*' -o -name '\.*\.log' \) -print | xargs rm -f
 	(cd doc; $(MAKE) distclean)
 
 ############################################################
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)
+
+  )
-- 
cgit v1.2.3