hol-light/hol-light-autotest.el


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

;; 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))

(require 'proof-site)
(proof-ready-for-assistant 'hol-light)

(require 'pg-autotest)

(unless (bound-and-true-p byte-compile-current-file)
  
  (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))