From 129a482f636228243e440fbbe0f891284bf0ce4e Mon Sep 17 00:00:00 2001 From: David Aspinall Date: Tue, 3 Aug 2010 18:39:13 +0000 Subject: Resurrect autotest framework --- Makefile.devel | 2 +- generic/pg-autotest.el | 158 ++++++++++++++++++++++++++++++++++++++----------- isar/isar-autotest.el | 49 ++++++++++----- 3 files changed, 158 insertions(+), 51 deletions(-) diff --git a/Makefile.devel b/Makefile.devel index 8d8b244e..d386ff2a 100644 --- a/Makefile.devel +++ b/Makefile.devel @@ -211,7 +211,7 @@ tags: $(EL) $(TAGS_EXTRAS) # Run tests for a particular prover and particular Emacs # test.%: - if [ -f "$*/$*-autotest.el" ]; then if $(EMACS) $(EMACSFLAGS) -l generic/proof-site.el $*/$*-autotest.el -f eval-current-buffer; then echo "Autotests run successfully on `date`" > $*/.autotest.txt; else rm -f $*/autotest.txt; exit 1; fi; fi + 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 echo "Autotests for $* ran with failures (see $*/.autotest.log) on `date`"; exit 1; fi; fi testall.%: for prover in ${PROVERS}; do $(MAKE) test.$$prover EMACS=$*; done diff --git a/generic/pg-autotest.el b/generic/pg-autotest.el index 2aef7df8..6b3c6b4d 100644 --- a/generic/pg-autotest.el +++ b/generic/pg-autotest.el @@ -7,11 +7,9 @@ ;; ;; TODO: ;; -- fix failure handling for scriptfile -;; -- force re ;; -- add macros for defining test suites ;; -- add more precise functional tests to check results ;; -- add negative tests -;; -- output test results to stdout ;; ;; $Id$ @@ -20,9 +18,18 @@ ;;; Commentary: ;; +;; Support for running a series of scripted UI tests. +;; ;;; Code: -(defvar pg-autotest-success t) ;; success unless error caught + +(defvar pg-autotest-success t + "Flag indicating overall successful state of tests.") + +(defvar pg-autotest-log t + "Value for 'standard-output' during tests") + +(setq debug-on-error t) ;; enable in case a test goes wrong ;;; Some utilities @@ -42,26 +49,87 @@ (unless (proof-locked-region-empty-p) ;; Should retract and unregister if was completely full (proof-goto-point)) - (pg-autotest-assert-unprocessed file)) + (pg-autotest-test-assert-unprocessed file)) ;;; Invoke a test (defmacro pg-autotest (fn &rest args) - `(condition-case err - (apply (intern (concat "pg-autotest-" (symbol-name (quote ,fn)))) - (list ,@args)) - (error - (progn - (setq pg-autotest-success nil) - (princ (format "Error in test %s: %s" (symbol-name (quote ,fn)) - err)))))) ;; display-error stdout? - + `(unwind-protect + (progn + (setq standard-output pg-autotest-log) + (condition-case err + (let ((scaffoldfn + (intern (concat "pg-autotest-" + (symbol-name (quote ,fn)))))) + (if (fboundp scaffoldfn) + (apply scaffoldfn (list ,@args)) + (pg-autotest-message + (format "TEST: %s" (cons (quote ,fn) (quote ,args)))) + (apply (intern (concat "pg-autotest-test-" + (symbol-name (quote ,fn)))) + (list ,@args)))) + (error + (progn + (setq pg-autotest-success nil) + (pg-autotest-message + (format "ERROR %s: %s" (quote ,fn) + (prin1-to-string err))))))) + (setq standard-output t))) + + +;;; Test output and timing + +(defun pg-autotest-log (file) + (save-excursion + (find-file file) + (erase-buffer) + (setq pg-autotest-log (current-buffer)))) +(defun pg-autotest-message (msg) + "Give message MSG in log file output and on display." + (proof-with-current-buffer-if-exists + pg-autotest-log + (insert msg "\n")) + (message msg) + (redisplay t)) + +(defun pg-autotest-remark (msg) + (pg-autotest-message (concat "\n\nREMARK: " msg "\n"))) + +(defun pg-autotest-timestart (&optional clockname) + "Make a note of current time, named 'local or CLOCKNAME." + (put 'pg-autotest-time (or clockname 'local) + (current-time))) + +(defun pg-autotest-timetaken (&optional clockname) + "Report time since (startclock CLOCKNAME)." + (let* ((timestart (get 'pg-autotest-time (or clockname 'local))) + (timetaken + (time-subtract (current-time) timestart))) + (pg-autotest-message + (format "TIME: %f (%s)" (float-time timetaken) + (if clockname (symbol-name clockname) + "this test"))))) + +(defun pg-autotest-exit () + "Exit Emacs returning Unix success 0 if all tests succeeded." + (proof-with-current-buffer-if-exists + pg-autotest-log + (save-buffer 0)) + (kill-emacs (if pg-autotest-success 0 1))) -;;; The tests proper +;;; The test script functions proper + +(defun pg-autotest-test-process-wholefile (file) + "Load FILE and script in one go. +An error is signalled if scripting doesn't completely the whole buffer." + (pg-autotest-find-file-restart file) + (proof-process-buffer) + (pg-autotest-test-assert-processed file)) -(defun pg-autotest-script-wholefile (file) - "Load FILE and script line-by-line, waiting a second between each line. +(defun pg-autotest-test-script-wholefile (file) + "Load FILE and script line-by-line, using `proof-shell-wait' before sending +each line. An error is signalled if scripting doesn't complete." (pg-autotest-find-file-restart file) (save-excursion @@ -70,49 +138,69 @@ An error is signalled if scripting doesn't complete." (setq last-locked-end (proof-unprocessed-begin)) (goto-char last-locked-end) (save-current-buffer - (proof-assert-next-command-interactive) + (condition-case err + (proof-assert-next-command-interactive) + (error + (let ((msg (car-safe (cdr-safe err)))) + (unless (string-equal msg + ;; normal user error message at end of buffer + "At end of the locked region, nothing to do to!") + (pg-autotest-message + (format + "proof-assert-next-command-interactive hit an error: %s" + msg)))))) (proof-shell-wait)) (goto-char (proof-queue-or-locked-end)) - (setq making-progress (> (point) last-locked-end)) - (sit-for 1)))) - (pg-autotest-assert-processed file)) + (setq making-progress (> (point) last-locked-end))))) + (pg-autotest-test-assert-processed file)) -(defun pg-autotest-retract-file (file) +(defun pg-autotest-test-script-randomjumps (file jumps) + "Load FILE and process in it by jumping around randomly JUMPS times. +This should be robust against synchronization errors; we test this by +completely processing the buffer as the last step." + (pg-autotest-find-file-restart file) + (while (> jumps 0) + (let ((random-point (random (point-max)))) + ;; TODO: random use of retract whole buffer too + (goto-char random-point) + (proof-goto-point) + (proof-shell-wait) + ;; TODO: check no error from prover + (decf jumps))) + (proof-process-buffer) + (pg-autotest-test-assert-processed file)) + +(defun pg-autotest-test-retract-file (file) (save-excursion (pg-autotest-find-file file) (proof-retract-buffer) (sit-for 1))) -(defun pg-autotest-assert-processed (file) +(defun pg-autotest-test-assert-processed (file) "Check that FILE has been fully processed." (save-excursion (pg-autotest-find-file file) (unless (proof-locked-region-full-p) - (error (format "Locked region in file `%f' is not full" file))))) + (error (format "Locked region in file `%s' is not full" file))))) -(defun pg-autotest-assert-unprocessed (file) +(defun pg-autotest-test-assert-unprocessed (file) "Check that FILE has been fully unprocessed." (save-excursion (pg-autotest-find-file file) (unless (proof-locked-region-empty-p) - (error (format "Locked region in file `%f' is not empty" file))))) + (error (format "Locked region in file `%s' is not empty" file))))) -(defun pg-autotest-message (msg) - "Give message MSG on std out & on display." - (message msg) - ;; FIXME: can we send to std out even if emacs is not batch mode? - (print msg) - (sit-for 1)) +(defun pg-autotest-test-eval (body) + "Evaluate given expression for side effect." + (eval body)) -(defun pg-autotest-quit-prover () +(defun pg-autotest-test-quit-prover () "Exit prover process." (if (buffer-live-p proof-shell-buffer) (kill-buffer proof-shell-buffer) (error "No proof shell buffer to kill"))) -(defun pg-autotest-finished () - "Exit Emacs returning Unix success 0 if all tests succeeded." - (kill-emacs (if pg-autotest-success 0 1))) + diff --git a/isar/isar-autotest.el b/isar/isar-autotest.el index 4ea027be..d86dcdf6 100644 --- a/isar/isar-autotest.el +++ b/isar/isar-autotest.el @@ -8,35 +8,54 @@ (eval-when-compile (require 'cl)) -(eval-when (compile) - (require 'proof-utils) - (proof-ready-for-assistant 'isar)) - +(require 'proof-utils) (require 'pg-autotest) +(proof-ready-for-assistant 'isar) +(require 'isar) + (unless noninteractive - ;; The included test files - (pg-autotest message "Testing standard Example.thy, Example-Xsym.thy") + (pg-autotest log ".autotest.log") + (pg-autotest timestart 'total) + + (pg-autotest remark "Testing standard Example.thy, Example-Xsym.thy") (pg-autotest script-wholefile "isar/Example.thy") - (pg-autotest script-wholefile "isar/Example-Xsym.thy") + (pg-autotest script-wholefile "isar/Example-Tokens.thy") + + (pg-autotest remark "Testing random jumps") + (pg-autotest eval (isar-tracing:auto-quickcheck-toggle 0)) + (pg-autotest eval (isar-tracing:auto-solve 0)) ; autosolve hammers this! + (pg-autotest script-randomjumps "isar/Example.thy" 5) + (pg-autotest script-randomjumps "etc/isar/AHundredTheorems.thy" 10) -; These require Complex theory -;(pg-autotest script-wholefile "isar/Root2_Isar.thy") -;(pg-autotest script-wholefile "isar/Root2_Tactic.thy") + (pg-autotest remark "Testing restarting the prover") + (pg-autotest quit-prover) -;; The standard simple multiple file examples + (pg-autotest remark "Now in tokens mode") + (pg-autotest eval (proof-unicode-tokens-toggle)) + (pg-autotest script-wholefile "isar/Example-Tokens.thy") - (pg-autotest message "Simple test of multiple files...") + (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") (pg-autotest assert-processed "etc/isar/multiple/C.thy") (pg-autotest assert-processed "etc/isar/multiple/A.thy") (pg-autotest assert-processed "etc/isar/multiple/B.thy") - (pg-autotest retract-file "etc/isar/multiple/B.thy") + (pg-autotest retract-file "etc/isar/multiple/B.thy") (pg-autotest assert-unprocessed "etc/isar/multiple/B.thy") (pg-autotest assert-unprocessed "etc/isar/multiple/C.thy") (pg-autotest assert-processed "etc/isar/multiple/A.thy") - (pg-autotest-quit-prover) - (pg-autotest-finished)) + (pg-autotest quit-prover) + + (pg-autotest timetaken 'total) + + (pg-autotest exit) + + ) -- cgit v1.2.3