From 3cf72581c40e8700d40cc8d7e0022da991a04382 Mon Sep 17 00:00:00 2001 From: David Aspinall Date: Fri, 13 Aug 2010 10:49:03 +0000 Subject: More tests --- coq/coq-autotest.el | 41 +++++++++++++++++++++++++++++++++++++++-- 1 file changed, 39 insertions(+), 2 deletions(-) (limited to 'coq/coq-autotest.el') diff --git a/coq/coq-autotest.el b/coq/coq-autotest.el index 12869052..0d583b45 100644 --- a/coq/coq-autotest.el +++ b/coq/coq-autotest.el @@ -14,12 +14,49 @@ (require 'pg-autotest) -;; The included test files (unless noninteractive + + (pg-autotest log ".autotest.log") ; convention + + (pg-autotest timestart 'total) + (pg-autotest remark "Testing standard examples...") (pg-autotest script-wholefile "coq/example.v") - (pg-autotest script-wholefile "coq/example-tokens.v") + ; FIXME: currently broken + ;(pg-autotest script-wholefile "coq/example-tokens.v") (pg-autotest script-wholefile "coq/ex-module.v") + (pg-autotest remark "Testing prove-as-you-go (not replay)") + (find-file ".autotest.v") + (erase-buffer) ; just in case exists + (setq buffer-file-name nil) + (pg-autotest eval (proof-electric-terminator-toggle 1)) + (pg-autotest eval (insert "Module test")) ; no \n + (proof-electric-terminator) + (pg-autotest eval (insert " Goal forall (A B:Prop),(A /\\ B) -> (B /\\ A)")) + (proof-electric-terminator) + (pg-autotest eval (insert "\ntauto.")) +; FIXME: bug/test error +; (backward-char) +; (proof-electric-terminator) ; shouldn't insert another + (pg-autotest eval (insert " End test")) + (proof-electric-terminator) + (pg-autotest assert-full) + + ;; test switching active scripting buffer after + ;; an error (see cvs log for proof-script.el 10.68) + + (pg-autotest eval (insert " End test")) + (proof-electric-terminator) + (set-buffer-modified-p nil) + (kill-buffer ".autotest.v") + (proof-shell-wait) + (pg-autotest script-wholefile "coq/example.v") + (pg-autotest quit-prover) + + (pg-autotest remark "Complete.") + + (pg-autotest timetaken 'total) + (pg-autotest exit)) -- cgit v1.2.3