diff --git a/ci/simple-tests/coq-test-proof-stat.el b/ci/simple-tests/coq-test-proof-stat.el index d725d01e5..2db6a001c 100644 --- a/ci/simple-tests/coq-test-proof-stat.el +++ b/ci/simple-tests/coq-test-proof-stat.el @@ -36,7 +36,7 @@ Test that the report buffer contains the expected output." (find-file "proof_stat.v") ;; run check on file where all errors are in opaque parts - (proof-check-proofs) + (proof-check-proofs nil) ;; the result buffer should exist (should (buffer-live-p (get-buffer "*proof-check-report*"))) @@ -74,7 +74,7 @@ Check that `proof-check-proofs' signals an error with the expected message." ;; proof-check-proofs should abort now with an error (condition-case err-desc (progn - (proof-check-proofs) + (proof-check-proofs nil) ;; Still here? Make test fail! (should nil)) (error diff --git a/generic/pg-user.el b/generic/pg-user.el index 63a50d77f..f919a4b5c 100644 --- a/generic/pg-user.el +++ b/generic/pg-user.el @@ -603,34 +603,58 @@ last use time, to discourage saving these into the users database." ;; Check validity of proofs ;; -(defun proof-check-report (proof-results) +(defun proof-check-report (proof-results tap batch) "Report `proof-check-proofs' results in PROOF-RESULTS in special buffer. Report the results of `proof-check-proofs' in buffer -`proof-check-report-buffer' in human readable form." +`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 +the results to the file denoted by BATCH." (let* ((src-file (buffer-file-name)) (ok-fail (seq-group-by #'car proof-results)) (frmt " %-4s %s") - (frmt-face (propertize frmt 'face 'error))) + (frmt-face (propertize frmt 'face 'error)) + (count 1)) (with-current-buffer (get-buffer-create proof-check-report-buffer) (erase-buffer) - (insert - (propertize (concat "Proof check results for " src-file) 'face 'bold) - "\n\n") - (insert - (format - (propertize "%d opaque proofs recognized: %d successful " 'face 'bold) - (length proof-results) - (length (cdr (assoc t ok-fail))))) - (insert (format (propertize "%d FAILING" 'face 'error 'face 'bold) - (length (cdr (assoc nil ok-fail))))) - (insert "\n\n") + (if tap + (insert (format "TAP version 14\n1..%d\n" (length proof-results))) + ;; human output + (insert + (propertize (concat "Proof check results for " src-file) 'face 'bold) + "\n\n") + (insert + (format + (propertize "%d opaque proofs recognized: %d successful " 'face 'bold) + (length proof-results) + (length (cdr (assoc t ok-fail))))) + (insert (format (propertize "%d FAILING" 'face 'error 'face 'bold) + (length (cdr (assoc nil ok-fail))))) + (insert "\n\n")) (dolist (pr proof-results) - (insert (format (if (car pr) frmt frmt-face) - (if (car pr) "OK " "FAIL") - (cadr pr))) - (insert "\n")) - (goto-char (point-min)) - (display-buffer (current-buffer))))) + (if tap + (progn + (insert (format "%sok %d - %s\n" + (if (car pr) "" "not ") + count + (cadr pr))) + (setq count (1+ count))) + ;; human readable + (insert (format (if (car pr) frmt frmt-face) + (if (car pr) "OK " "FAIL") + (cadr pr))) + (insert "\n"))) + (if batch + (progn + (insert "\n\n") + (if (stringp batch) + (append-to-file (point-min) (point-max) batch) + (message "%s" + (buffer-substring-no-properties + (point-min) (point-max))))) + (goto-char (point-min)) + (display-buffer (current-buffer)))))) (defun proof-check-chunks (chunks) "Worker function for `proof-check-proofs for processing CHUNKS. @@ -716,12 +740,11 @@ as reported by `proof-get-proof-info-fn'." (setq chunks (cdr chunks)))) (nreverse proof-results))) -(defun proof-check-proofs () - "Generate overview about valid and invalid proofs in current buffer. +(defun proof-check-proofs (tap &optional batch) + "Generate overview about valid and invalid proofs. This command completely processes the current buffer and -generates an overview in the `proof-check-report-buffer' about -all the opaque proofs in it and whether their proof scripts are -valid or invalid. +generates an overview about all the opaque proofs in it and +whether their proof scripts are valid or invalid. This command makes sense for a development process where invalid proofs are permitted and vos compilation and the omit proofs @@ -729,6 +752,16 @@ feature (see `proof-omit-proofs-configured') are used to work at the most interesting or challenging point instead of on the first invalid proof. +Argument TAP, which can be set by a prefix argument, controls the +form of the generated overview. Nil, without prefix, gives an +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. + In the same way as the omit-proofs feature, this command only tolerates errors inside scripts of opaque proofs. Any other error is reported to the user without generating an overview. The @@ -737,7 +770,7 @@ scripts are classified as opaque by the omit-proofs feature. For Coq for instance, among others, proof scripts terminated with 'Defined' are not opaque and do not appear in the generated overview." - (interactive) + (interactive "P") (unless (and proof-omit-proofs-configured proof-get-proof-info-fn proof-retract-command-fn) @@ -762,7 +795,7 @@ overview." nil "proof-check: first chunk cannot be a proof") (setq proof-results (proof-check-chunks chunks)) (proof-shell-exit t) - (proof-check-report proof-results))) + (proof-check-report proof-results tap batch)))