The Coq mailing list

[Hendrik Tews <hendrik AT askra.de>]

Emilio,

thanks for your quick answer.

Emilio Jesús Gallego Arias 
<e AT x80.org>
 writes:

> I'm not sure there's a new syntax, see the removal PR
> https://github.com/coq/coq/pull/765

I was afraid of that. Proof General was using Show Goal "id"
since the proof tree branch was merged in 2012. When the removal
PR was discussed, I did unfortunately not have the time to follow
any discussions around Coq or Proof General in 2017.

> I guess that command could be re-instantiated, or you could use

I find prooftree really useful. It helps to maintain the overview
in mid-size or bigger proofs. I would therefore really appreciate
if the command would be supported again.

If it is not too difficult, a command that prints a goal in a
certain state, would even be more useful. That would permit to
print a goal in the state before certain existential variables
have been instantiated. In turn, this would permit to move more
of the proof tree logic and data from Proof General to prooftree
and to decouple both application even more, with benefits for
performance. Proof General tries to parallelise Coq and the
command queue handling by sending the next command to Coq before
the output from the previous has been fully processed. Because
one cannot print a goal at a previous state, all the code that
decides about what goals need to be printed must be located in
Proof General, must run before Proof General sends the next
command to Coq and does therefore run sequentially with Coq.

> Goal identifiers,

Could somebody point me to the documentation of goal identifiers?
I cannot find them with google.

> however, I am not sure if using the toplevel protocol to
> implement proof tree display will be robust enough as to
> survive for long.

What would you suggest instead?

Thanks,

Hendrik