From f64240abecf2fad75e3cc05759961bbce4cb4ddd Mon Sep 17 00:00:00 2001 From: David Aspinall Date: Fri, 10 Jun 2011 14:39:34 +0000 Subject: Deleted file --- etc/TESTS | 95 --------------------------------------------------------------- 1 file changed, 95 deletions(-) delete mode 100644 etc/TESTS (limited to 'etc') diff --git a/etc/TESTS b/etc/TESTS deleted file mode 100644 index 222e5958..00000000 --- a/etc/TESTS +++ /dev/null @@ -1,95 +0,0 @@ -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). - - - - - -- cgit v1.2.3