The Coq mailing list

[Jim Fehrle <jim.fehrle AT gmail.com>]

Hendrik, I'd be happy to investigate what's needed to make prooftree work again and look at providing more useful information as you suggest.  If there is a reasonable solution that needs only a small effort, I will implement it, too.  Would you open an issue for this in GitHub and send me the link?  That would be a better place to discuss it.

Regards,

Jim

First questions to answer in the issue:  You want to use goal numbers, such as the 41 in this output (From: coqtop -emacs <test3.v)?  Or the 9 (not sure what to call it)?  Maybe provide a short example proof showing what you want.  What info do you want to get back if there are multiple open goals--just the usual output from Coq or more or less?

<prompt>ev_even_firsttry < 9 |ev_even_firsttry| 0 < </prompt><infomsg>

This subproof is complete, but there are some unfocused goals.

Focus next goal with bullet -.

</infomsg>

1 subgoal (ID 41)

subgoal 1 (ID 41) is:

 exists k : nat, S (S n') = double k

On Tue, Jun 4, 2019 at 10:06 PM Hendrik Tews <hendrik AT askra.de> wrote:

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