The "Time (tactic)." vernacular command no longer displays timings unless the tactic finishes the proof

[coquser]

It used to be the case (and still is the case in coqtop) that

Goal True /\ True.
  split.
  Time idtac.
  Time constructor.

  Time constructor.

would display the timings of all three Time toplevel vernacular commands. In PG-emacs, only the final Time command gives me a timing in the response panel.

[coquser]

Hi,

where do you expect to see the time info, below the goal or in the *response* buffer?

Can you tell a Proof General version that has the behavior you expect?

The timing is still there, you can see it in the *coq* buffer.

Bye,

Hendrik

[coquser]

It's good to know that it's present in the *coq* buffer, thanks.

I don't really care whether I see it below the goal in the *goals* buffer or in the *response* buffer. I want to see it without having to change what buffers I'm displaying; when I start Coq in PG, I have my file which takes up the top half of the screen, then *goals* below that, then *response* below that; *coq* is not displayed by default. This is ProofGeneral Version 4.2, in GNU Emacs 24.2.1 (i386-mingw-nt6.1.7601) of 2012-08-28 on MARVIN.

-Jason

[coquser]

OK, but do you remember a PG version that had the behavior you expect? Was it showing the time below the goal or in the response buffer?

Hendrik

[coquser]

If I recall correctly, PG used to only show one buffer in emacs by default, so I'm pretty sure it was in the *goals* buffer.

Btw, is it possible to get me added to the cc list for this bug? (jasongross9+PG AT gmail DOT com)

-Jason

[David Aspinall]

Just to respond to the BTW: sorry, email from this Trac is (probably) disabled. Hackers break into Trac with bots and do nasty things. The RSS feed should work though.

[coquser]

The menu entries are fixed now, such that, when you select "Time Commands", the timings are shown. As long as this is on one cannot enable "hide additional subgoals".

If you type the Time command yourself, you have to customize coq-end-goals-regexp-show-subgoals to nil and disable "Hide additional subgoals". Otherwise the timings are only visible in the *coq* buffer.

Hendrik