CODEWITHSUNDEEP
coq
gust
gust

Reputation: 945

`coqc -Q`returns "coqc: -Q: no such file or directory"

When I try to compile files with coqc -Q . LF, I get the error:

coqc: -Q: no such file or directory

coqc information:

The Coq Proof Assistant, version 8.4pl6 (December 2020)
compiled on Dec 02 2020 23:06:36 with OCaml 4.02.0

What's strange is that it worked previously for me. I formatted my disk to the same exact OS, installed the same exact opam, yet I'm getting an error where I didn't before. Also using 8.4.6 for legacy reasons.

Upvotes: 0

Views: 87

Answers (1)

Yves
Yves

Reputation: 4236

Version 8.4.6 of Coq does not support a -Q option, this can be confirmed by looking in the manual, where no such option is documented. I also checked in the source files: they can be downloaded from https://github.com/coq/coq/releases/tag/V8.4pl6. a systematic search of string -R shows that it does appear in file scripts/coqc.ml but no string -Q appears anywhere in the sources.

You did not tell us the whole story. You are not reproducing exactly the same attempt... You must have been using a more recent version until now.

Upvotes: 2

Related Questions