search

ProofGeneral / PG

This repo is the new home of Proof General
https://proofgeneral.github.io
GNU General Public License v3.0
490 stars 87 forks source link

[coq] On goal display and silent mode. #188

Open ejgallego opened 7 years ago

ejgallego commented 7 years ago

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:

Let me know what you think.

Cheers, E.

[BTW, note that afb29a670c537412d09cec703da7e8821c658196 should probably be reverted]

psteckler commented 7 years ago

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 commented 7 years ago

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 commented 7 years ago

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 commented 7 years ago

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 commented 7 years ago

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

ejgallego commented 7 years ago

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 commented 7 years ago

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 commented 7 years ago

A heady brew, that!

ejgallego commented 7 years ago

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 commented 7 years ago

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 < notifications@github.com>:

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 https://github.com/ProofGeneral/PG/issues/188#issuecomment-305558889, or mute the thread https://github.com/notifications/unsubscribe-auth/AEsl6tTE12adLLM1jGPS_CZuNtrN1qMmks5r_vCmgaJpZM4NtAeT .

Matafou commented 7 years ago

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 pierre.courtieu@gmail.com:

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 < notifications@github.com>:

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 https://github.com/ProofGeneral/PG/issues/188#issuecomment-305558889, or mute the thread https://github.com/notifications/unsubscribe-auth/AEsl6tTE12adLLM1jGPS_CZuNtrN1qMmks5r_vCmgaJpZM4NtAeT .

ejgallego commented 7 years ago

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 commented 7 years ago

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 commented 7 years ago

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 commented 7 years ago

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 commented 7 years ago

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 commented 7 years ago

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

sarahzrf commented 6 years ago

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 commented 6 years ago

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 commented 6 years ago

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

Is there an ETA on the next version?

Matafou commented 6 years ago

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 notifications@github.com 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 https://github.com/ProofGeneral/PG/issues/188#issuecomment-344074703, or mute the thread https://github.com/notifications/unsubscribe-auth/AEsl6uqKwAcI_ZvzOPzogVjGcBexs6jWks5s2L0-gaJpZM4NtAeT .

sarahzrf commented 6 years ago

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 commented 5 years ago

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 commented 5 years ago

Pierre Courtieu notifications@github.com 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:

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 commented 5 years ago

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 commented 5 years ago

Pierre Courtieu notifications@github.com 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 commented 5 years ago

Here you go: https://github.com/ProofGeneral/PG/pull/429

P.

Le ven. 12 juil. 2019 à 19:59, hendriktews notifications@github.com a écrit :

Pierre Courtieu notifications@github.com 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 https://github.com/ProofGeneral/PG/issues/188?email_source=notifications&email_token=ABFSL2T27LY7QPQHWZOHEA3P7DA73A5CNFSM4DNUA6J2YY3PNVWWK3TUL52HS4DFVREXG43VMVBW63LNMVXHJKTDN5WW2ZLOORPWSZGODZ2OPOY#issuecomment-510977979, or mute the thread https://github.com/notifications/unsubscribe-auth/ABFSL2XUHQTUWH7PIMKGT33P7DA73ANCNFSM4DNUA6JQ .