From 39b2499da290056f4f26f419da8048f1732c5b7b Mon Sep 17 00:00:00 2001
From: David Aspinall <da@inf.ed.ac.uk>
Date: Wed, 8 Feb 2012 17:41:57 +0000
Subject: Add autotest

---
 hol-light/hol-light-autotest.el | 36 ++++++++++++++++++++++++++++++++++++
 1 file changed, 36 insertions(+)
 create mode 100644 hol-light/hol-light-autotest.el

(limited to 'hol-light')

diff --git a/hol-light/hol-light-autotest.el b/hol-light/hol-light-autotest.el
new file mode 100644
index 00000000..20c16727
--- /dev/null
+++ b/hol-light/hol-light-autotest.el
@@ -0,0 +1,36 @@
+;; hol-light-autotest.el: tests of HOL Light Proof General.
+;;
+;; You can run these by issuing "make test.hol-light" in PG home dir.
+;;
+;; $Id$
+;;
+
+(eval-when-compile
+  (require 'cl))
+
+(eval-when (compile)
+  (require 'proof-site)
+  (proof-ready-for-assistant 'coq)
+  (defvar coq-compile-before-require nil))
+
+(require 'pg-autotest)
+
+(unless noninteractive
+  
+  (pg-autotest start 'debug)
+  (pg-autotest log ".autotest.log")  ; convention
+
+  (pg-autotest timestart 'total)
+
+  (pg-autotest remark "Testing standard examples...")
+
+  (pg-autotest script-wholefile "hol-light/example.ml")
+
+  (proof-shell-wait)
+
+
+  (pg-autotest remark "Complete.")
+
+  (pg-autotest timetaken 'total)
+
+  (pg-autotest exit))
-- 
cgit v1.2.3