1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 17 18 19 20 21 22 23 24 25 26 27 28 29 30 31 32 33 34 35 36 37 38 39 40 41 42 43 44 45 46 47 48 49 50 51 52 53 54 55 56 57 58 59 60 61 62 63 64 65 66 67 68 69 70 71 72 73 74 75 76 77 78 79 80 81 82 83 84 85 86 87 88 89 90 91 92 93 94 95 96 97 98 99 100 101 102 103 104 105 106 107 108 109 110 111 112 113 114 115 116
|
;;; pg-test.el --- Simple test framework for Proof General.
;; This file is part of Proof General.
;; Portions © Copyright 1994-2012 David Aspinall and University of Edinburgh
;; Portions © Copyright 2003-2018 Free Software Foundation, Inc.
;; Portions © Copyright 2001-2017 Pierre Courtieu
;; Portions © Copyright 2010, 2016 Erik Martin-Dorel
;; Portions © Copyright 2011-2013, 2016-2017 Hendrik Tews
;; Portions © Copyright 2015-2017 Clément Pit-Claudel
;;; Commentary:
;;
;;; Code:
(eval-when-compile (require 'cl-lib))
(defconst pg-test-buffer "** PG test output **")
(defvar pg-test-total-success-count 0)
(defvar pg-test-total-fail-count 0)
(defvar pg-test-suite-success-count 0)
(defvar pg-test-suite-fail-count 0)
;; A test suite is a list of tests.
(defvar pg-test-suite-table nil)
(defvar pg-current-test-suite nil)
(defun pg-set-test-suite (name)
(setq pg-current-test-suite name)
(unless (assoc name pg-test-suite-table)
(setq pg-test-suite-table
;; Add an empty subtable
(cons (cons name nil) pg-test-suite-table))))
(defun pg-clear-test-suite (name)
(setq pg-test-suite-table
(remassoc name pg-test-suite-table)))
(defmacro pg-test-eval (expr result)
"Add test (equal (eval EXPR) RESULT) to current test suite."
(let* ((suite (assoc pg-current-test-suite pg-test-suite-table))
(testnum (length suite))
(name (concat pg-current-test-suite "." (int-to-string testnum))))
(setcdr suite (cons (list name 'eval expr result) (cdr suite)))
;; Result is number of this test in suite
testnum))
(defun pg-execute-test (test)
(let ((name (car test))
(type (cadr test)))
(cond
((eq type 'eval)
(let ((expr (nth 2 test))
(goodresult (nth 3 test))
result errorresult exn)
(condition-case exn
(setq result (eval expr))
;; FIXME: add negative tests here, that exns _are_ raised.
(t (setq errorresult
(format " %s failed: error signalled: %s %s\n"
name (car exn) (cdr exn)))))
(or errorresult
(unless (equal goodresult result)
(setq errorresult
(format " %s failed: exprected result %s, got %s\n"
name goodresult result))))
(if errorresult
(cl-incf pg-test-suite-fail-count)
(cl-incf pg-test-suite-success-count)
(setq errorresult (format " %s succeeded.\n" name)))
;; Return string
errorresult))
;; No other types at the moment
(t
(error "Eek! unrecognized test type."))
)))
(defun pg-execute-test-suite (name)
(interactive (list
(completing-read "Run test suite: "
pg-test-suite-table)))
(setq pg-test-suite-success-count 0)
(setq pg-test-suite-fail-count 0)
(save-excursion
(set-buffer (get-buffer-create pg-test-buffer))
(insert "=================================================================\n")
(insert "TEST SUITE: " name "\n")
(insert "=================================================================\n")
(apply 'insert
(mapcar 'pg-execute-test
(reverse (cdr-safe
(assoc name pg-test-suite-table)))))
(insert (format
"\nTotal successful tests: %s, failed tests: %s\n\n"
pg-test-suite-success-count pg-test-suite-fail-count)))
(setq pg-test-total-success-count
(+ pg-test-suite-success-count pg-test-total-success-count))
(setq pg-test-total-fail-count
(+ pg-test-suite-fail-count pg-test-total-fail-count)))
(defun pg-execute-all-tests ()
(interactive)
(pop-to-buffer
(get-buffer-create pg-test-buffer))
(erase-buffer)
(sit-for 0)
(setq pg-test-total-success-count 0)
(setq pg-test-total-fail-count 0)
(mapcar 'pg-execute-test-suite (mapcar 'car pg-test-suite-table)))
;; End of `pg-test.el'
|