The Coq mailing list

[Emilio Jesús Gallego Arias <e AT x80.org>]

Hendrik Tews 
<hendrik AT askra.de>
 writes:

>> 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.

IMHO this command can be resurrected, I don't have time to do the PR
now, please feel free to go ahead.

> 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.

I am not sure what you mean, but I'd suggest you open an issue on Github
and we continue the discussion there.

>> 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?

That's a good question, you could try for example some tools such as
coq-serapi, it does provide a nicer interaction model, however that
protocol is also not expected to stay like this for long; I'd like to do
a major revision soon.

On the other hand, getting feedback on what you folks would need would
be great as to be sure your use case is properly accounted in the next
revision.

E.