blob: 8be4bed91f6cd08647b91dc3fb97a0613badab62 (
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
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
|
;;; coq-autotest.el --- tests of Coq Proof General (in progress).
;; This file is part of Proof General.
;; Portions © Copyright 1994-2012 David Aspinall and University of Edinburgh
;; Portions © Copyright 2003-2018 Free Software Foundation, Inc.
;; Portions © Copyright 2001-2017 Pierre Courtieu
;; Portions © Copyright 2010, 2016 Erik Martin-Dorel
;; Portions © Copyright 2011-2013, 2016-2017 Hendrik Tews
;; Portions © Copyright 2015-2017 Clément Pit-Claudel
;;; Commentary:
;;
;; You can run these by issuing "make test.coq" in PG home dir.
;;
;;; Code:
(require 'pg-autotest)
(require 'proof-site)
(defvar coq-compile-before-require)
(unless (bound-and-true-p byte-compile-current-file)
(pg-autotest start 'debug)
;; new multiple file handling for Coq gives interactive queries
;; continually unless we set this.
(setq proof-auto-action-when-deactivating-scripting 'retract)
(setq proof-no-fully-processed-buffer t)
(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")
(pg-autotest script-wholefile "coq/ex-module.v")
(proof-shell-wait)
(pg-autotest remark "Regression testing bug cases...")
(pg-autotest script-wholefile "etc/coq/parsingcheck-410.v")
;(pg-autotest script-wholefile "etc/coq/parsingcheck-412.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)
;; Note: with new multiple-file code, above fires up process.
;; If we do (proof-shell-wait) here, we get a deadlock.
(pg-autotest eval (insert " Goal forall (A B:Prop),(A /\\ B) -> (B /\\ A)"))
(proof-electric-terminator)
(proof-shell-wait)
(pg-autotest eval (insert "\ntauto."))
(backward-char)
(proof-electric-terminator) ; shouldn't insert another or delete present
(proof-shell-wait)
;; FIXME: next test fails, why?
(pg-autotest assert-full)
;; TODO: test switching active scripting buffer after
;; an error (see cvs log for proof-script.el 10.68)
;; FIXME: bug, this causes "region is read only"
;; (pg-autotest eval (insert " End test"))
;; (proof-electric-terminator)
(set-buffer-modified-p nil)
(kill-buffer ".autotest.v")
(proof-shell-wait)
;; TODO: test indentation. E.g., to avoid regression of Trac #416
(pg-autotest script-wholefile "etc/coq/multiple-plain/a.v")
(pg-autotest script-wholefile "etc/coq/multiple-plain/b.v")
(pg-autotest script-wholefile "etc/coq/multiple-plain/c.v")
(pg-autotest script-wholefile "etc/coq/multiple-plain/a.v")
(pg-autotest remark "Testing multiple-file recompilation...")
(setq coq-compile-before-require t)
(pg-autotest script-wholefile "coq/ex/test-cases/multiple-files-single-dir/f.v")
(proof-shell-wait)
(find-file "d.v")
(set-buffer-modified-p t)
(save-buffer)
(pg-autotest-test-retract-file "coq/ex/test-cases/multiple-files-single-dir/f.v")
(proof-shell-wait)
(pg-autotest script-wholefile "coq/ex/test-cases/multiple-files-single-dir/f.v")
(pg-autotest remark "Complete.")
(pg-autotest timetaken 'total)
(pg-autotest exit))
(provide 'coq-autotest)
;;; coq-autotest.el ends here
|
