1 files changed, 95 insertions, 0 deletions
diff --git a/etc/TESTS b/etc/TESTS
new file mode 100644
index 00000000..222e5958
--- /dev/null
+++ b/etc/TESTS
@@ -0,0 +1,95 @@
+Some test cases for Proof General.
+==================================
+
+See testing-log.txt for log of tests conducted.
+Please add to that file!
+
+
+22.3.00 FILENAME ESCAPES PROBLEM [All provers, probably]
+========================================================
+
+  Filename substitution %s in settings including proof-shell-cd-cmd,
+  proof-shell-inform-file-{retracted,processed}-cmd, may need
+  to add escape characters peculiar to the proof assistant syntax.
+
+  Test cases:
+
+     ln -s ProofGeneral \\backslash  
+     ln -s ProofGeneral \"quote
+
+  Then try scripting with example files for each prover,
+  i.e.  \"quote/coq/example.v, etc.
+
+
+1.2.99 FILE RECOGNITION PROBLEM  [Isabelle]
+===========================================
+
+  Bug in regexp caused ML files to be recognized as
+  theory files when "thy" appeared in path.
+  Test case in etc/isa/thy/test.ML.
+
+
+15.1.99  LONG-LINE AND BACKSLASH PROBLEM ON SOLARIS
+===================================================
+
+  Test that etc/isa/long-line-backslash.ML can be processed
+  successfully.
+
+
+16.12.98 KILLING THE PROOF PROCESS
+==================================
+
+  Process some proof script buffer. Invoke 
+
+    M-x proof-shell-exit
+
+  Process should exit cleanly.
+  
+11.12.98  RUDELY KILLING THE ACTIVE SCRIPTING BUFFER
+====================================================
+
+  Start scripting with some buffer, after
+  having processed another buffer.
+
+  Kill it when scripting is only partly finished.
+
+  Scripting should be cleanly turned off and it
+  should be possible to resume retraction in the 
+  first buffer.
+
+  Moreover, this ensures that if the file is on the included
+  files list, yet has been only partly processed (e.g. because
+  Undo steps were taken), then it will be retracted and
+  removed from the included files list.
+
+  FIXME: Using C-x C-v to revert to saved version doesn't
+  seem to work because it renames the buffer or something.
+
+8.12.98  INHIBIT VARIABLES
+==========================
+
+  Test with proof-splash-inhibit=t
+
+  Test with proof-toolbar-inhibit=t
+  
+
+8.12.98  SCRIPTING FOR BUFFERS WITHOUT FILES.
+=============================================
+
+  Switch to a fresh buffer FOO which doesn't visit a file.
+  Do  M-x isa-mode RET.
+  Should succeed.
+  Try asserting commands, e.g. Goal "P-->P";
+
+  Switch to another fresh buffer BAR, turn on isa-mode.
+  Should succeed again.
+  Try asserting commands here, e.g. Goal "Q&Q --> Q";
+  Should give error "Cannot have more than one active scripting buffer".
+
+  Exit emacs.  Should query whether we want to save these
+  scripting buffers (maybe XEmacs only).
+
+
+    
+  
+