diff options
| author |  David Aspinall <da@inf.ed.ac.uk> | 2000-09-28 09:26:22 +0000 |
|---|---|---|
| committer | David Aspinall <da@inf.ed.ac.uk> | 2000-09-28 09:26:22 +0000 |
| commit | c89323ce90b75749e604da0faaf32e8d3a20a802 (patch) | |
| tree | a5907f028744a26927e1eb6fe289eb04a35ecf22 /README.devel | |
| parent | 7461ed40c038d7088bc05c4a705ea5f9ee9a2c74 (diff) | |
Dreams about testing
Diffstat (limited to 'README.devel')
| -rw-r--r-- | README.devel | 15 |
1 files changed, 14 insertions, 1 deletions
diff --git a/README.devel b/README.devel index 5b082c47..869daaa8 100644 --- a/README.devel +++ b/README.devel @@ -34,7 +34,20 @@ proof assistant then has its own todo file. When writing your modes, please follow the Emacs Lisp Conventions See the Emacs Lisp reference manual, node Style Tips. - +** Testing + +Ideally, we would have an automated test suite for Proof General. +Emacs Lisp is certainly flexible to have such a thing, but it would +take some effort to set it up. Although automated tests could test +functions and states for the right values, a user interface ultimately +needs some human checks that visible appearances and user-input behave +as expected. + +At the moment, we rely on the tiny example files included for each +proof system as simple tests that basic scripting works. Multiple +file scripting is more complex (involving cooperation with the +prover). Some test cases should be provided in etc/<PA> as has been +done for Lego and Isabelle. ** Standards for each instance of PG |