blob: 0d583b4573b95ee22fddd413c16be854f03f1ae9 (
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
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
|
;; coq-autotest.el: tests of Coq Proof General (in progress).
;;
;; You can run these by issuing "make test.coq" in PG home dir.
;;
;; $Id$
;;
(eval-when-compile
(require 'cl))
(eval-when (compile)
(require 'proof-site)
(proof-ready-for-assistant 'coq))
(require 'pg-autotest)
(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")
; 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))
|
