Coq should support *trace* buffer for idtac output

[coquser]

When debugging proof search, it's often useful to use idtac for printf debugging. Unfortunately, we can't do this in ProofGeneral, because it only gives us the last idtac output. It would be really nice if ProofGeneral worked more like coqtop in this respect.

[David Aspinall]

It sounds like this would be useful, could you give a bit more description and example please so a non-Coq user can understand? Also, please add more info to #430 if that's a different case.

[coquser]

Consider the following Coq proof script:

Goal False.
  idtac 1; idtac 2; idtac 3; fail.

In coqtop, each idtac invocation gives us output:

ezyang@javelin:~$ coqtop
Welcome to Coq 8.3pl1 (June 2011)

Coq < Goal False.
1 subgoal
  
  ============================
   False

Unnamed_thm < idtac 1; idtac 2; idtac 3; fail.
1
2
3
Error: Tactic failure.

We would expect ProofGeneral to give us something similar, but instead we only get the error message "Tactic failure."

In the wild, I ran into cases where I only got the last idtac output; but I can't seem to construct a minimal test-case where this shows up.

[David Aspinall]

Hmm, I see. PG has a tracing facility designed exactly for this kind of debugging output, but it isn't configured in Coq (to be fair, it ought to be documented: #432). What we'd like is for Coq to add special marker characters around its tracing output automatically to support this smoothly like is done with prompt outputs when -emacs option is given. Perhaps somebody can propose a patch to the Coq developers to do this.

Meanwhile, if you try some code like this in your .emacs you can add tags to your debugging messages manually (make the tags unlikely to match other output and make the starting tag less than 12 characters):

(defconst my-idtac-tag-start "***"
  "Used to start tracing messages for PG *trace* buffer in Coq")

(defconst my-idtac-tag-end "***"
  "Used to finish tracing messages for PG *trace* buffer in Coq")

(eval-after-load "proof-site"
  '(progn
     (setq proof-shell-trace-output-regexp (regexp-quote my-idtac-tag-start))
     (add-hook 'coq-shell-mode-hook
	       '(lambda () 
		  (setq proof-shell-eager-annotation-start
			(concat proof-shell-eager-annotation-start
				"\\|"
				(regexp-quote my-idtac-tag-start)))
		  (setq proof-shell-eager-annotation-end
			(concat proof-shell-eager-annotation-end
				"\\|"
				(regexp-quote my-idtac-tag-end)))))))

This will send the messages to a dedicated *trace* buffer.

A simpler work around is to disable the "swallowing" of output (which is done deliberately for efficiency) and disable cleaning the *response* buffer:

  (setq proof-shell-silent-threshold 200)
  (setq proof-tidy-response nil)

You can customize either of these variables if you want the settings to persist.

[coquser]

​http://www.lix.polytechnique.fr/coq/bugs/show_bug.cgi?id=2644

[David Aspinall]

Waiting until Coq developers take note or someone supplies a patch to them (should be pretty easy, simply add tags like current <prompt> and <\prompt>), then can reopen here.

[coquser]

Upstream have now fixed it in trunk: ​https://coq.inria.fr/bugs/show_bug.cgi?id=2644

[coquser]

This could probably be closed; it works for me using the latest PG and Coq (though the output goes to *response*, not to *trace*).

-- Clément

[courtieu]

It works indeed better in the last versions because now that <infomsg> stuff are displayed even if they appear before the goal.

BUT for me it does not display when an error is raises, like in the example provided

Goal False.

idtac 1; idtac 2; idtac 3; fail.

I only see the error message, not the numbers.