blob: 20c1672711aaaa1885a919c2c9fa7ab4dec55d53 (
plain)
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
|
;; 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))
|
