From c89323ce90b75749e604da0faaf32e8d3a20a802 Mon Sep 17 00:00:00 2001 From: David Aspinall Date: Thu, 28 Sep 2000 09:26:22 +0000 Subject: Dreams about testing --- README.devel | 15 ++++++++++++++- 1 file changed, 14 insertions(+), 1 deletion(-) 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/ as has been +done for Lego and Isabelle. ** Standards for each instance of PG -- cgit v1.2.3