Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Jump to bottom

Never send two commands at once #563

Closed
hendriktews opened this issue Mar 19, 2021 · 5 comments · Fixed by #564
Closed

Never send two commands at once #563

hendriktews opened this issue Mar 19, 2021 · 5 comments · Fixed by #564

Comments

@hendriktews
Copy link
Collaborator

We should never send two commands at once to Coq as it is currently done here:

PG/coq/coq.el

Line 2157 in 56ee4eb

(let ((res (format "Remove Search Blacklist %s. \nAdd Search Blacklist %s. "

Via :setting, coq-search-blacklist (search for defpacustom search-blacklist) appears in proof-assistant-settings, which causes to evaluate coq-set-search-blacklist when Coq starts at the end of proof-shell-config-done.

Sending two commands at once (of course) causes Coq to return two prompts. In rare cases in automated tests, proof-shell-exec-loop just sees the first prompt and sends the next command directly after the first prompt, such that there is one additional prompt pending for quite a while. While debugging a sporadic test error for a new test for #559, I captured the following content from *coq*:

Welcome to Coq 8.12.0 (November 2020)

<prompt>Coq < 1 || 0 < </prompt>Add Search Blacklist "Private_" "_subproof". 

<prompt>Coq < 2 || 0 < </prompt>Set Suggest Proof Using. 

<prompt>Coq < 3 || 0 < </prompt>Set Diffs "off". 

<prompt>Coq < 4 || 0 < </prompt>Set Printing Depth 50 . 

<prompt>Coq < 5 || 0 < </prompt>Remove Search Blacklist "Private_" "_subproof".  Add Search Blacklist "Private_" "_subproof". 

<prompt>Coq < 6 || 0 < </prompt>Set Printing Width 9.

<prompt>Coq < 7 || 0 < </prompt>Set Silent. 

<prompt>Coq < 8 || 0 < </prompt>Definition classical_logic : Prop := forall(P : Prop), ~~P -> P.

<prompt>Coq < 9 || 0 < </prompt>Lemma classic_excluded_middle :   (forall(P : Prop), P \/ ~ P) -> classical_logic.

<prompt>Coq < 10 || 0 < </prompt>Proof using.

<prompt>classic_excluded_middle < 11 |classic_excluded_middle| 0 < </prompt>intros H P H0.

<prompt>classic_excluded_middle < 12 |classic_excluded_middle| 0 < </prompt>specialize (H P).

<prompt>classic_excluded_middle < 13 |classic_excluded_middle| 0 < </prompt>destruct H.

<prompt>classic_excluded_middle < 14 |classic_excluded_middle| 0 < </prompt>trivial.

<prompt>classic_excluded_middle < 15 |classic_excluded_middle| 0 < </prompt>contradiction.

<prompt>classic_excluded_middle < 16 |classic_excluded_middle| 0 < </prompt>Unset Silent. 

<prompt>classic_excluded_middle < 17 |classic_excluded_middle| 0 < </prompt>Qed.

<prompt>classic_excluded_middle < 19 |classic_excluded_middle| 0 < </prompt>

Here the additional prompt is only processed 12 commands later! For this new test this happens in about 1 of 10 runs. In the other runs the additional prompt is processed directly after the blacklist command.
This effect is a very good candidate for causing #537.
@Matafou
Copy link
Contributor

Matafou commented Mar 19, 2021

Well spotted!
I can fix that.

@hendriktews
Copy link
Collaborator Author

hendriktews commented Mar 19, 2021 via email

@Matafou
Copy link
Contributor

Matafou commented Mar 19, 2021

It is not worth it. There is already a command coq-search-blacklist-stringset also callable from menu: Coq/Settings/Search Blacklist, which deals with search blacklist. I will just change this to not use proof-assistant-settings at alls. I will still allow the customization of coq-search-blacklist-string via the defcustom but it will be only for the default blacklist at pg start.

Matafou added a commit to Matafou/PG that referenced this issue Mar 19, 2021
@Matafou
Fix ProofGeneral#563.
04025d7 
Splitting the coq into two commands made me remove
coq-search-blacklist-string from defpgcustom. The visible effect is
that the menu entry has moved, and the command name changed. This is
explained in the CHANGES.
@hendriktews
Copy link
Collaborator Author

ok, fine with me, I don't even know what that feature is for

@Matafou
Copy link
Contributor

Matafou commented Mar 19, 2021

Search is for listing currently imported lemmas by queries, by there names, type etc. The Blacklist thing is to systematically exclude things from the queries. I find it quite useful to set it to "Private_" "_subproof" "_ind" "_rec" "_rect", and during development I tend to make it grow while detecting things polluting my queries.
Another feature I would like is to have PG allow to set a similar mechanism for excluding entire modules from the query. Currently you have to put outside UglyModule at the end of each query.

Matafou added a commit to Matafou/PG that referenced this issue Mar 19, 2021
@Matafou
Fix ProofGeneral#563.
d880ac6 
Splitting the coq into two commands made me remove
coq-search-blacklist-string from defpgcustom. The visible effect is
that the menu entry has moved, and the command name changed. This is
explained in the CHANGES.
This was referenced Mar 19, 2021
Merged
Merged
Matafou added a commit to Matafou/PG that referenced this issue Mar 21, 2021
@Matafou
Fix ProofGeneral#563 avoid dual-send bug in search blacklist customiz…
1182531 
…ation.

Splitting the coq into two commands made me remove
coq-search-blacklist-string from defpgcustom. The visible effect is
that the menu entry has moved, and the command name changed. This is
explained in the CHANGES.

To squash.
Matafou added a commit that referenced this issue Mar 21, 2021
@Matafou
Fix #563 avoid dual-send bug in search blacklist customization.
0a0a343 
Splitting the coq into two commands made me remove
coq-search-blacklist-string from defpgcustom. The visible effect is
that the menu entry has moved, and the command name changed. This is
explained in the CHANGES.

To squash.
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Assignees
No one assigned
Labels
None yet
Projects
None yet
Milestone
No milestone
Development

Successfully merging a pull request may close this issue.

Fix #563. Refactor search blacklist custom to avoid dual-send bug. Matafou/PG
2 participants
@Matafou @hendriktews