Proof state not refreshed after Admitted

[tchajed]

In the following example,

Goal True.
Admitted.

If you process the sentences one at a time, the proof state remains at 1 subgoal of True. It seems Admitted is being treated the same as Qed, which is to do nothing. This isn't quite correct, though - for Admitted clearly the proof state has changed, and in a nested proof the *goals* window should be updated to show the outer proof again even for a Qed.

[psteckler]

Just to note, in my XML protocol fork of PG, for this example, the goal
window is updated after the Admitted has been processed.

-- Paul

On Wed, Aug 17, 2016 at 11:33 AM, Tej Chajed notifications@github.com
wrote:

In the following example,

Goal True.Admitted.

If you process the sentences one at a time, the proof state remains at 1
subgoal of True. It seems Admitted is being treated the same as Qed, which
is to do nothing. This isn't quite correct, though - for Admitted clearly
the proof state has changed, and in a nested proof the goals window
should be updated to show the outer proof again even for a Qed.

—
You are receiving this because you are subscribed to this thread.
Reply to this email directly, view it on GitHub
#103, or mute the thread
https://github.com/notifications/unsubscribe-auth/ACJAKI0u6n_y8lPkLjI3ugP4VxY2935zks5qgym5gaJpZM4JmlNt
.

[Blaisorblade]

FWIW, not refreshing after Qed. is also incorrect with nested proofs (this might be the real issue underlying #154)—it should update the screen to show the open goals. If you only execute Qed., refresh is only needed if there are nested proofs; but if you jump to after Qed. from a different state, the shown goal might even have been solved.

Is that also handled correctly in the XML fork?

[psteckler]

The PG/xml fork always updates the goal buffer after each individual statement, if single-stepping, or after a block of statements, if asserting to a point or running the whole buffer.

…

-- Paul

On Tue, Feb 21, 2017 at 9:03 AM, Paolo G. Giarrusso < ***@***.***> wrote: FWIW, not refreshing after Qed. is also incorrect with nested proofs (this might be the real issue underlying #154 <#154>)—it should update the screen to show the open goals. If you *only* execute Qed., refresh is only needed if there are nested proofs; but if you jump to after Qed. from a different state, the shown goal might even have been solved. Is that also handled correctly in the XML fork? — You are receiving this because you commented. Reply to this email directly, view it on GitHub <#103 (comment)>, or mute the thread <https://github.com/notifications/unsubscribe-auth/ACJAKOc9tqioBQiotWm27eZIxI-TyN47ks5reu6dgaJpZM4JmlNt> .