diff options
| -rw-r--r-- | etc/TESTS | 16 | ||||
| -rw-r--r-- | etc/testing-log.txt | 11 |
2 files changed, 27 insertions, 0 deletions
@@ -5,6 +5,22 @@ 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] =========================================== diff --git a/etc/testing-log.txt b/etc/testing-log.txt index 0e86e183..4447e73e 100644 --- a/etc/testing-log.txt +++ b/etc/testing-log.txt @@ -1,3 +1,14 @@ +Wed Mar 22 13:45:34 GMT 2000 da + + Tested file name quoting problem with Coq, Isabelle, LEGO. + + \ quoting triggers bug in Isabelle (complaint about pathname) + " quoting not allowed in LEGO, \ quoting not needed. + Coq works well with either. + + +-------- + Wed Nov 17 13:43:11 GMT 1999 Tested compiled version. Seems to work well for XEmacs! |