[nongnu] elpa/proof-general 065d5e8ba7 1/4: proof-stat: correct TAP output; create files in batch mode

[ELPA Syncer]

branch: elpa/proof-general
commit 065d5e8ba79ac253d9a2cabae4f175d3f00785f7
Author: Hendrik Tews <hendrik@askra.de>
Commit: hendriktews <hendrik@askra.de>

    proof-stat: correct TAP output; create files in batch mode
---
 ci/simple-tests/.gitignore                                   |  3 +++
 ci/simple-tests/Makefile                                     |  8 ++++----
 .../{proof_stat.exp-out => proof_stat.human.exp-out}         |  7 -------
 ci/simple-tests/proof_stat.tap.exp-out                       |  7 +++++++
 doc/ProofGeneral.texi                                        |  8 ++++----
 generic/pg-user.el                                           | 12 ++++++------
 6 files changed, 24 insertions(+), 21 deletions(-)

diff --git a/ci/simple-tests/.gitignore b/ci/simple-tests/.gitignore
index 67f5cfcffe..e418346307 100644
--- a/ci/simple-tests/.gitignore
+++ b/ci/simple-tests/.gitignore
@@ -1 +1,4 @@
 *.success
+proof_stat.human.gen-out
+proof_stat.tap.gen-out
+coq-proof-stat-batch-test
diff --git a/ci/simple-tests/Makefile b/ci/simple-tests/Makefile
index 70b15a1fd9..c8a506f482 100644
--- a/ci/simple-tests/Makefile
+++ b/ci/simple-tests/Makefile
@@ -30,12 +30,12 @@ qrhl-all: $(QRHL_SUCCESS)
 # proof_stat.v and compares it with the expected output in file
 # proof_stat.exp-out.
 coq-proof-stat-batch-test:
-       rm -rf proof_stat.gen-out
        emacs -batch -l ../../generic/proof-site.el proof_stat.v \
-             --eval '(proof-check-proofs nil "proof_stat.gen-out")'
+             --eval '(proof-check-proofs nil "proof_stat.human.gen-out")'
        emacs -batch -l ../../generic/proof-site.el proof_stat.v \
-             --eval '(proof-check-proofs t "proof_stat.gen-out")'
-       cmp proof_stat.gen-out proof_stat.exp-out && \
+             --eval '(proof-check-proofs t "proof_stat.tap.gen-out")'
+       cmp proof_stat.human.gen-out proof_stat.human.exp-out && \
+               cmp proof_stat.tap.gen-out proof_stat.tap.exp-out && \
                touch coq-proof-stat-batch-test
 
 .PHONY: clean
diff --git a/ci/simple-tests/proof_stat.exp-out 
b/ci/simple-tests/proof_stat.human.exp-out
similarity index 63%
rename from ci/simple-tests/proof_stat.exp-out
rename to ci/simple-tests/proof_stat.human.exp-out
index 9f4f0aa5d2..82346b541f 100644
--- a/ci/simple-tests/proof_stat.exp-out
+++ b/ci/simple-tests/proof_stat.human.exp-out
@@ -7,10 +7,3 @@ Proof check results for proof_stat.v
   FAIL b2_equal_6
 
 
-TAP version 13
-1..3
-not ok 1 - a1_equal_4
-ok 2 - b_equal_6
-not ok 3 - b2_equal_6
-
-
diff --git a/ci/simple-tests/proof_stat.tap.exp-out 
b/ci/simple-tests/proof_stat.tap.exp-out
new file mode 100644
index 0000000000..7903afc6aa
--- /dev/null
+++ b/ci/simple-tests/proof_stat.tap.exp-out
@@ -0,0 +1,7 @@
+TAP version 13
+1..3
+not ok 1 a1_equal_4
+ok 2 b_equal_6
+not ok 3 b2_equal_6
+
+
diff --git a/doc/ProofGeneral.texi b/doc/ProofGeneral.texi
index de74c7c1d5..d9a29a164a 100644
--- a/doc/ProofGeneral.texi
+++ b/doc/ProofGeneral.texi
@@ -2290,9 +2290,9 @@ human readable overview, otherwise it's test anything
 protocol (@var{tap}). Argument @var{batch} controls where the overview goes
 to. If nil, or in an interactive call, the overview appears in
 @samp{@code{proof-check-report-buffer}}. If @var{batch} is a string, it should 
be a
-filename and the overview is appended there. Otherwise the
-overview is output via @samp{message} such that it appears on stdout
-when this command runs in batch mode.
+filename to write the overview to. Otherwise the overview is
+output via @samp{message} such that it appears on stdout when this
+command runs in batch mode.
 
 In the same way as the omit-proofs feature, this command only
 tolerates errors inside scripts of opaque proofs. Any other error
@@ -2326,7 +2326,7 @@ where @code{<tap>} should be @code{nil} for human 
readable output and
 @code{t} for test anything protocol. If @code{<output>} is @code{t}
 the proof status appears in the standard output of the Emacs process.
 Otherwise @code{<output>} should be a filename as string in double
-quotes. Then the proof status is appended to this file. (If
+quotes. Then the proof status is written to this file. (If
 @code{output} is @code{nil} or omitted, the proof status is only put
 into the @code{*proof-check-report*} buffer, which does not make much
 sense in a batch command as the one above.)
diff --git a/generic/pg-user.el b/generic/pg-user.el
index 05b3c46f88..2818c8ca52 100644
--- a/generic/pg-user.el
+++ b/generic/pg-user.el
@@ -616,7 +616,7 @@ Report the results of `proof-check-proofs' in buffer
 `proof-check-report-buffer' in human readable form or, if TAP is
 not nil, in test anything protocol (TAP). If BATCH is not nil,
 report the results via message, such that they appear on stdout
-when Emacs runs in batch mode or, when BATCH is a string, append
+when Emacs runs in batch mode or, when BATCH is a string, write
 the results to the file denoted by BATCH."
   (let* ((ok-fail (seq-group-by #'car proof-results))
          (frmt "  %-4s %s")
@@ -655,7 +655,7 @@ the results to the file denoted by BATCH."
       (dolist (pr proof-results)
         (if tap
             (progn
-              (insert (format "%sok %d - %s\n"
+              (insert (format "%sok %d %s\n"
                               (if (car pr) "" "not ")
                               count
                               (cadr pr)))
@@ -669,7 +669,7 @@ the results to the file denoted by BATCH."
           (progn
             (insert "\n\n")
             (if (stringp batch)
-                (append-to-file (point-min) (point-max) batch)
+                (write-region (point-min) (point-max) batch)
               (message "%s"
                        (buffer-substring-no-properties
                         (point-min) (point-max)))))
@@ -779,9 +779,9 @@ human readable overview, otherwise it's test anything
 protocol (TAP). Argument BATCH controls where the overview goes
 to. If nil, or in an interactive call, the overview appears in
 `proof-check-report-buffer'. If BATCH is a string, it should be a
-filename and the overview is appended there. Otherwise the
-overview is output via `message' such that it appears on stdout
-when this command runs in batch mode.
+filename to write the overview to. Otherwise the overview is
+output via `message' such that it appears on stdout when this
+command runs in batch mode.
 
 In the same way as the omit-proofs feature, this command only
 tolerates errors inside scripts of opaque proofs. Any other error