[coq] On goal display and silent mode.

[ejgallego]

Hi folks,

as noted by @JasonGross in https://coq.inria.fr/bugs/show_bug.cgi?id=5564 , upstream changes broke again PG's goal display in Coq. This is due to our decision to make all sentences part of the document "synchronous" as "document state" migrates towards a fully referentially-transparent model.

Thus, now, when you add to the document a sentence such as Set Silent, if you backtrack its effects will be undone.

Jason's bug has three different possible solutions AFAICS:

• adapt PG to emit Show everytime it'd like to display goals. In this case, I'd go even a bit further and support options in Show such as printing width or hypothesis limiting. This is the model newer protocols are following (with some caveats such as feedback/error printing).
• make PG emit Unset Silent after backtrack, as pointed out by Jason.
• add support to Coq for "document-wide" options. This is already planned for 8.8, however we could add support for a few options including Set Silent. They key part that distinguishes such options is that they won't be part of the document, and are likely to follow a different syntax, such as :set silent.

Let me know what you think.

Cheers, E.

[BTW, note that afb29a6 should probably be reverted]

[psteckler]

I like the first option. By default, PG would request the goal after submitting a statement or sequence of statements. There could be a PG option to disable the automatic goal requests, or a special way to submit statements without requesting the goal.

[ejgallego]

Well I guess @psteckler this is what you already do in PG-xml, correct? If so, you are the best one to judge how difficult implementing 1 is.

[psteckler]

Yes, that's what happens in PG/xml: a Goal call is made automatically after receiving the responses to all Add calls. In vanilla PG, you wouldn't even have to wait for the responses (and probably I could have done that in PG/xml).

[ejgallego]

Well in the (hopefully) 8.8 protocol you indeed don't need to wait, as you will specify the span_id, you can queue Goals sid anytime you want. This is how it works now in jsCoq for example.

[psteckler]

The Goal call doesn't contain a state id, so I could change that with the current protocol.

[ejgallego]

In order to have effective async processing you need to have that parameter, both in the query and in the answer, otherwise you need to implement painful waiting and state and even block user actions.

[ejgallego]

I think that the 8.8 protocol (if we ever get to finish it) will be basically a less capable XML version of the SerAPI protocol which is a mix of the original STM, the jsCoq protocol, and @cpitclaudel suggestions.

[psteckler]

A heady brew, that!

[ejgallego]

The main design goal is to require no global state in the client, thus all the state will be per-span and the client implements a simple automaton.

[Matafou]

I can make legacy/pg issue a Show after each (group of) commands, actually I alrady do that in some cases. It could be triggered with >8.7 versions. P. 2017-06-01 19:11 GMT+02:00 Emilio Jesús Gallego Arias < [email protected]>:

…

The main design goal is to require no global state in the client, thus all the state will be per-span and the client implements a simple automaton. — You are receiving this because you are subscribed to this thread. Reply to this email directly, view it on GitHub <#188 (comment)>, or mute the thread <https://github.com/notifications/unsubscribe-auth/AEsl6tTE12adLLM1jGPS_CZuNtrN1qMmks5r_vCmgaJpZM4NtAeT> .

[Matafou]

I just pushed a fix for this on PG side: When the user backtracks inside a proof, pg issues a "Unset Silent. Show.". when the backtrack is done outside a proof, it issues only "Unset Silent". P. 2017-06-02 2:38 GMT+02:00 Pierre Courtieu <[email protected]>:

…

I can make legacy/pg issue a Show after each (group of) commands, actually I alrady do that in some cases. It could be triggered with >8.7 versions. P. 2017-06-01 19:11 GMT+02:00 Emilio Jesús Gallego Arias < ***@***.***>: > The main design goal is to require no global state in the client, thus > all the state will be per-span and the client implements a simple automaton. > > — > You are receiving this because you are subscribed to this thread. > Reply to this email directly, view it on GitHub > <#188 (comment)>, > or mute the thread > <https://github.com/notifications/unsubscribe-auth/AEsl6tTE12adLLM1jGPS_CZuNtrN1qMmks5r_vCmgaJpZM4NtAeT> > . >

[ejgallego]

Thanks @Matafou , I think we should change the semantics for Show here as the check "inside a proof" seems a bit cumbersome. IMHO pushing this kind of complexity into PG is not what Coq should promote but the other way around.

Indeed, I think that the right semantics for Show outside a proof should be "show nothing" instead of giving an error. What do you think? This way, you could call Show at any time and don't worry about it.

(Maybe we should rename the new show as to avoid compatibility issues.)

[Matafou]

Yes it would be nice.

Again for efficiency reason on big goals I would rather not send Show blindly all the time. Ideally, at least in xml/protocol Show should return either the new goal or a reference to a previous goal already sent.

[ejgallego]

Ok, understood, thanks, will cook a patch.

I am not so sure about the efficiency gain of avoiding to re-send goals, IMO bandwidth is pretty cheap (I am told that Isabelle's protocol uses several MiB/s) and if you have a multi MiB goal then you have some other problems. It is true that the toplevel could keep a cache of printed goals, but again I regard this as a minor item.

I think this could indeed be controlled by the printing depth / limiting parameters, which indeed have been requested by users many times (so you can have dynamic piecewise display of goals).

[Matafou]

Experience will tell.
By the way is there a priority system in the protocol? Like "stop this heavy computation of a part of the file I am not currently looking at and answer this Show immediately". Isabelle is full of such things as far as I know.

[ejgallego]

By the way is there a priority system in the protocol?

We cannot really do it now due to the current threading architecture, the only way to interrupt Coq is by sending a signal and that has some problems (specially on windows).

However there are plans to re-engineer the current code so the main thread would be control-only, when this sees the light of the day (or OCaml gets non-cooperative multithreading) we may be able indeed to implement something similar.

[ejgallego]

Well, you have some limited support for priority hints with Stm.set_perspective

[sarahzrf]

This seems to be an issue for me—sometimes my goal window mysteriously goes blank if I do stuff like editing a line without backtracking first. It seems like Unset Silent. fixes that, but why is it a problem in the first place?

[Matafou]

PG sets/unsets silent when scripting several commands at a time. This avoids the heavy useless outputs from coq (which emacs then reads) when scripting big chunks of files.

This problem should disappear in the next vrsion (which uses xml protocol, which is silent by construction).
Therefore I don't think I will investigate this.

[sarahzrf]

Alright. For now I'm coping by disabling silencing entirely, which is working 90% fine.

Is there an ETA on the next version?

[Matafou]

You can probably just script back one line and and then forward to make things appear again. Le lun. 13 nov. 2017 à 23:05, benzrf <[email protected]> a écrit :

…

Alright. For now I'm coping by disabling silencing entirely, which is working 90% fine. Is there an ETA on the next version? — You are receiving this because you were mentioned. Reply to this email directly, view it on GitHub <#188 (comment)>, or mute the thread <https://github.com/notifications/unsubscribe-auth/AEsl6uqKwAcI_ZvzOPzogVjGcBexs6jWks5s2L0-gaJpZM4NtAeT> .

[sarahzrf]

I think that sometimes worked and sometimes didn't, but if it's gonna be changed in the next version, I don't think it's too critical to work out the details :)

[Matafou]

Coming back to this.

I already fixed a few cases where the goal would not show up by inserting a "Show." command.

But there is still an annoying case where this does not work: when several commands are stopped by one of them giving an error. Since groups of commands are sent silently, when the error occurs there is no goal printed and the architecture of pg make it very difficult to insert a "Show." command at this particular point. For now I did not manage to do that.

@hendriktews it seems you needed quite heavy stuff to insert commands at the place you needed it. How did you do it please?

Of course the problem disappears if we remove the silencing. This would have drawbacks:

1. I remember efficiency problems when doing that... But it was long ago.

and advantages:

1. goals shown eveywhere
2. goals stored in spans everywhere

I feel the legacy pg code is slowly bitroting and this is the kind of problems we will face more and more I guess.

[hendriktews]

Pierre Courtieu <[email protected]> writes:

@hendriktews it seems you needed quite heavy stuff to insert commands at the place you needed it. How did you do it please?

Most of the time, the head of `proof-action-list` has already been sent to the proof assistant and waits there only for getting retired - that is running its ACTION and then being removed from `proof-action-list`. Therefore, it won't work, if push to `proof-action-list`. What could work, but what I have never investigated, if you insert behind the first element of `proof-action-list`... What I instead did for prooftree, was to find the place in `proof-shell-exec-loop`, where it was save to push to `proof-action-list`. This is now marked with a comment starting with ;; This is the point where old items have been removed from and after the comment I inserted the call to `proof-tree-urgent-action`, which pushes all the necessary `Show` commands for prooftree into proof-action-list. Instead of following that approach as well, I would suggest to consider something more generic: - add a variable `proof-action-list-pending-to-be-injected-next` - always push the content of `proof-action-list-pending-to-be-injected-next` to the front of `proof-action-list` at that place in `proof-shell-exec-loop` that I indicated - then you can everywhere push to `proof-action-list-pending-to-be-injected-next`... - maybe you find a name shorter than `proof-action-list-pending-to-be-injected-next` For the next version of prooftree I would like to use this generic mechanism as well, because then I plan to asynchronously receive commands from the external prooftree program that need to be injected into `proof-action-list`. Hendrik

[Matafou]

Thanks @hendriktews. I will try that. But the problem is that it is during the treatment of an error message that we detect that we should send a "Show" to the prover. I managed to put the action in action-list and have it executed, but not to have its result displayed in goals buffer.

[hendriktews]

Pierre Courtieu <[email protected]> writes:

I managed to put the action in action-list and have it executed, but not to have its result displayed in goals buffer.

Can you point me to an example and a patch or PR to try?

[Matafou]

Here you go: #429 P. Le ven. 12 juil. 2019 à 19:59, hendriktews <[email protected]> a écrit :

…

Pierre Courtieu ***@***.***> writes: > I managed to put the action in action-list and have it > executed, but not to have its result displayed in goals buffer. Can you point me to an example and a patch or PR to try? — You are receiving this because you were mentioned. Reply to this email directly, view it on GitHub <#188?email_source=notifications&email_token=ABFSL2T27LY7QPQHWZOHEA3P7DA73A5CNFSM4DNUA6J2YY3PNVWWK3TUL52HS4DFVREXG43VMVBW63LNMVXHJKTDN5WW2ZLOORPWSZGODZ2OPOY#issuecomment-510977979>, or mute the thread <https://github.com/notifications/unsubscribe-auth/ABFSL2XUHQTUWH7PIMKGT33P7DA73ANCNFSM4DNUA6JQ> .