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

-vos/-vok not compatible with workers #15140

Open
SkySkimmer opened this issue Nov 8, 2021 · 1 comment
Open

-vos/-vok not compatible with workers #15140

SkySkimmer opened this issue Nov 8, 2021 · 1 comment
Labels
part: STM State Transition Machine, asynchronous proofs, etc.

Comments

@SkySkimmer
Copy link
Contributor

On

Lemma foo : True /\ True.
Proof.
  split.
  par:exact I.
Defined.

coqc -vos (resp -vok) will say

Don't know what to do with -vos tacticworker:0
See -help for the list of supported options
Handshake with tacticworker:0 failed: End_of_file

On

Lemma bar : True.
Proof. exact I. Qed.

coqc -vok -async-proofs on will say

Don't know what to do with -vok
See -help for the list of supported options
Handshake with proofworker:0 failed: End_of_file

On

Lemma bar : True.
Proof. exact I. Qed.

Lemma foo : True /\ True.
Proof.
  split.
  par:exact I.
Defined.

coqc -vos will hang (0% CPU, ps aux shows only the master process) (with -d vernacinterp, it will print interpreting: par : exact I before hanging)
@SkySkimmer SkySkimmer added the part: STM State Transition Machine, asynchronous proofs, etc. label Nov 8, 2021
@SkySkimmer SkySkimmer mentioned this issue Nov 8, 2021
Merged
@charguer
Copy link
Contributor

I am not sure by which exact mechanism the list of accepted arguments depends on the presence of a par: inside a file.
Anyway, I see two possible routes:

  • specify that -vos is not compatible with par:
  • specify and implement the fact that par: commands are ignored when -vos or -vok is used.

@SkySkimmer SkySkimmer mentioned this issue Mar 5, 2022
Merged
SkySkimmer added a commit to artagnon/coq that referenced this issue Mar 14, 2022
@SkySkimmer
Fix (partial) coq#15140 vos/vok vs workers
0b34b80 
~~~coq
Lemma bar : True.
Proof. exact I. Qed.

Lemma foo : True /\ True.
Proof.
  split.
  par:exact I.
Defined.
~~~
still hangs with vos.
SkySkimmer added a commit to SkySkimmer/coq that referenced this issue Mar 18, 2022
@SkySkimmer
Fix (partial) coq#15140 vos/vok vs workers
3593d31 
~~~coq
Lemma bar : True.
Proof. exact I. Qed.

Lemma foo : True /\ True.
Proof.
  split.
  par:exact I.
Defined.
~~~
still hangs with vos.

(cherry picked from commit 0b34b80)
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Assignees
No one assigned
Labels
part: STM State Transition Machine, asynchronous proofs, etc.
Projects
None yet
Milestone
No milestone
Development

No branches or pull requests
2 participants
@charguer @SkySkimmer