prooftree is broken with 8.5 syntax

[Matafou]

Regexp are outdated, I tried to fix it but I don't get the exact things to be matched. I guess we need Hendrik Tews for this. I will try to reach him.

[jonleivent]

If the plan is to revive prooftree, then there is much more to fix. For instance, it doesn't understand any of the various ways the focus might change in 8.5, such as with proof bullets, braces, goal selectors, goal reorderings (revgoals, cycle, swap), unshelve, etc. Is the provenance of subgoals, which would be needed to make the tree really reflect the proof, even something Coq keeps track of?

[Matafou]

I have somewhere a branch that shows all subgoals, even those that are not
under focus. That would help I suppose. But it is not in 8.5.

Maybe we should write in the CHANGE that it is currently broken for 8.5.

P.

2016-01-14 17:04 GMT+01:00 Jonathan Leivent notifications@github.com:

If the plan is to revive prooftree, then there is much more to fix. For
instance, it doesn't understand any of the various ways the focus might
change in 8.5, such as with proof bullets, braces, goal selectors, goal
reorderings (revgoals, cycle, swap), unshelve, etc. Is the provenance of
subgoals, which would be needed to make the tree really reflect the proof,
even something Coq keeps track of?

—
Reply to this email directly or view it on GitHub
#30 (comment).

[jonleivent]

I won't discourage you from trying to fix it! I was once a PVS user, and so miss this feature. However, I think if the tree doesn't really mirror goal provenance properly, then it might end up confusing users in 8.5. For instance, if a tactic shelves some subgoals which then are unshelved later, what will prooftree show? What will it show in the case of Grab Existential Variables? Especially in these cases where the origin of the goals isn't obvious, the user would rely on prooftree to help them out. If in one goal, the user unifies something with an evar, causing the other goal corresponding to that evar to morph somehow, what would prooftree show? Should prooftree show the dependencies between goals as well as the parent-child relationship? OK - well maybe I just did discourage you...

[Matafou]

I think this debate already happened between Hendrik and Arnaud, the goal
of prooftree is to show the tree of the script more than the one of the
proof engine. But you are right prooftree would probably not support easily
shelve/unshelve. But if it works when the user avoids shelve/unshelve (the
tactical unshelve would probably be ok) I consider it ok.

Let us add Hendrik to this discussion.

P.

2016-01-14 18:58 GMT+01:00 Jonathan Leivent notifications@github.com:

I won't discourage you from trying to fix it! I was once a PVS user, and
so miss this feature. However, I think if the tree doesn't really mirror
goal provenance properly, then it might end up confusing users in 8.5. For
instance, if a tactic shelves some subgoals which then are unshelved later,
what will prooftree show? What will it show in the case of Grab Existential
Variables? Especially in these cases where the origin of the goals isn't
obvious, the user would rely on prooftree to help them out. If in one goal,
the user unifies something with an evar, causing the other goal
corresponding to that evar to morph somehow, what would prooftree show?
Should prooftree show the dependencies between goals as well as the
parent-child relationship? OK - well maybe I just did discourage you...

—
Reply to this email directly or view it on GitHub
#30 (comment).

[jonleivent]

That is an interesting point - I had always thought prooftree was there to show the proof engine's tree, while the proof bullets/braces show the script's tree (now that they can in 8.5). Who is the consumer of prooftree's output, the user doing the proof or later users inspecting the proof by stepping through it? Probably the right answer is "Yes" (both). But they might wish for different behaviors.

[Matafou]

Dear all,

I am very happy to see ProofGeneral development is continuing now
on github! My role in FireEye has changed a bit now and I hope I
can contribute again to ProofGeneral in the future. I might not
make it to the next Coq release but I plan to look at prooftree
soon.

About the concrete problems discussed here:

• Bullets, braces, Focus work in 8.4 please try it. The same
  approach should work with new goal selectors or reorderings.
• Grab Existential Variables works in 8.4, just try it
• evars work in 8.4, just try it
• not all evar dependencies are shown in prooftree, but
  appearance and instantiations can be investigated
• unshelve seems to be new, I have to look into this
• the proof tree display is for people writing or investigating
  the proof, I don't see a conflict here.

Bye,

Hendrik

[hendriktews]

I got a lot of prooftree working now, I hope that I can open a
pull request soon. Support for existential variables will remain
broken for a while, see Coq bug 4504.

I am not sure I understand the purpose of the new shelve/unshelve
tactics. Are they just for capturing the goals of existential
variables?

[cpitclaudel]

I got a lot of prooftree working now

Great! That's exciting :)

I am not sure I understand the purpose of the new shelve/unshelve tactics. Are they just for capturing the goals of existential variables?

@jonleivent Is the expert on this, but my understanding is that they create explicit goals from existential variables that would have been moved to Grab Existential Variables back in 8.4.

[jonleivent]

Clement is correct. For example, one common tactic in Coq is eapply - which when used on the conclusion will create subgoals for the eapply'ed lemma's arguments. However, some of those subgoals may be shelved because they are "unifiable" with others - meaning that they are present in other goals as dependencies. Usually these shelved subgoals correspond to implicit args, but not always (explicit args can also be "unifiable" with later ones). Often, this shelving is just what the user wants - as those shelved "unifiable" subgoals will get solved as a side-effect of solving the remaining visible ones. But this is not always the case, and so various users requested an unshelve tactic so it can be used in combo with eapply (and other tactics that do similar shelving of implicit args) to force all resulting subgoals to remain visible regardless of their dependencies.

[Matafou]

I just filled a bug report for coq: the tactical unshelve is not documented
anywhere (the command Unshelve is but they are different).

"unshelve tac." performs tactic tac and then unshelve anything shelved by
tac. Shelved things are those explained by Jonathan, and they become
explicit goals.

P.

2016-01-22 17:50 GMT+01:00 Jonathan Leivent notifications@github.com:

Clement is correct. For example, one common tactic in Coq is eapply -
which when used on the conclusion will create subgoals for the eapply'ed
lemma's arguments. However, some of those subgoals may be shelved because
they are "unifiable" with others - meaning that they are present in other
goals as dependencies. Usually these shelved subgoals correspond to
implicit args, but not always (explicit args can also be "unifiable" with
later ones). Often, this shelving is just what the user wants - as those
shelved "unifiable" subgoals will get solved as a side-effect of solving
the remaining visible ones. But this is not always the case, and so various
users requested an unshelve tactic so it can be used in combo with eapply
(and other tactics that do similar shelving of implicit args) to force all
resulting subgoals to remain visible regardless of their dependencies.

—
Reply to this email directly or view it on GitHub
#30 (comment).

[hendriktews]

I just created a pull request that fixes basic proof-tree
functionality for 8.5. If you want to test it you need to
checkout the latest proof tree sources from
https://github.com/hendriktews/proof-tree. I created issues
hendriktews/proof-tree#1 and hendriktews/prooftree#2 for the
problems with Unshelve and evars. If you see more problems,
please file issues.

[hendriktews]

@jonleivent thanks for the explanation! My understanding is that
shelved goals are goals corresponding to existential variables
that could only made visible with Grab Existantial Variables in
8.4. Do you have an example with a shelved subgoal that one would
not get via Grab Existential Variables? (Of course other than
shelving something manually with Shelve.)

[jonleivent]

Using Grab Existential Variables, when it is allowed, will always get the remaining shelved goals. Even goals shelved manually. In other words, at any point in time (other than when Focus is being used), one can do "all:shelve. Grab Existential Variables." and the result will be that all goals will become visible and focused.

[hendriktews]

fixed by commit 8c4d991