The Coq mailing list

[Jonathan <jonikelee AT gmail.com>]

Interesting!  So, as long as I start each idtac with that 254 string and 
end it with that 255 string, I can use idtac as usual to print arbitrary 
terms visibly in PG, even without converting them to strings first:

Goal False.
  let s1 := eval vm_compute in (String "254" "") in
  let s2 := eval vm_compute in (String "255" "") in
  let x := constr:(1+1) in
  idtac s1 "hello" "there" x s2.
Abort.

Thanks, Kazuhiko!

However, one thing I noticed is that this construction, when used in 
CoqIDE, not only doesn't print, it causes CoqIDE to hang.  Of course, 
the motivation for its use is to not need CoqIDE for debugging tactics 
using idtac.

-- Jonathan

On 12/15/2014 11:10 AM, Kazuhiko Sakaguchi wrote:
> Hi Jonathan,
>
> I solved a part of the issue by this code:
>
> Require Import Coq.Strings.String.
> Open Scope string.
>
> Definition newline := String "010" "".
> Definition line s := s ++ newline.
>
> Definition show_pg s := String "254" s ++ String "255" "".
>
> Goal False.
>    let s := eval vm_compute in (show_pg (line "foo" ++ line "bar")) in
>      idtac s.
> Abort.
>
> Regards,
> Kazuhiko
>
> 2014-12-14 1:26 GMT+09:00 Jonathan 
> <jonikelee AT gmail.com>:
> > For a while now I've been flipping back and forth between using PG and
> > CoqIDE, mostly because for some reason PG no longer shows idtac messages
> > (and other non-failure messages, such as from the Time command) in most
> > cases.  It only shows them when the message-producing tactic also solves the
> > goal.
> >
> > I'm wondering if anyone else has this issue with idtac in PG, or if I
> > somehow have it misconfigured.
> >
> > I'm using a recent trunk version of Coq and the most recent development
> > version of PG (which is more than a year old).
> >
> > -- Jonathan