The Coq mailing list

[Pierre Courtieu <pierre.courtieu AT gmail.com>]

Hi Flavio,

In an empty configuration the command launched by pg is "coqtop
-emacs". AFAIK any other option comes from user configuration.

Once you have started coq, can you look at buffer *Messages* please?
It should contain a line describing the coqtop command (and the
options)  launched. Given the error message you get you should see a
-Q option that must come from somewhere in your configuration.

The configuration can be in a _CoqProject file inside you project, or
(unlikely) in a .dir-locals.el file, or from file variables at the end
of your file.

Hope this helps,
Pierre




2017-01-13 11:27 GMT+01:00 Flávio L. C. de Moura 
<flavio.de.moura AT gmail.com>:
> Hi Pierre,
>
> Before answering your questions, let me give some information:
>
> I installed Proof General from github as follows:
>
>  git clone https://github.com/ProofGeneral/PG ~/.emacs.d/lisp/PG
>      cd ~/.emacs.d/lisp/PG
>      make clean; make EMACS=/usr/local/bin/emacs
>
>
>
>> Hi,
>
>> Your coqtop is launched with -Q option py proofgeneral, which is not
>> compatible with coq-8.4. Please give more information on your
>> configuration so that we can help you:
>
>> - Does the directory where you start proofgeneral contain a _CoqProject 
>> file?
>
> No.
>
>> - Does the file where you start proofgeneral contain some file variable
>
> I don't think so... at least I couldn't find any. If there is some file
> variable, it is created automatically during the installation process.
>
>> - Do you have some pg related configuration in your .emacs?
>
> Yes.
>
> (load "~/.emacs.d/lisp/PG/generic/proof-site")
>
> (eval-after-load "proof-script" '(progn
>                                    (define-key proof-mode-map [(C-down)]
>                                      'proof-assert-next-command-interactive)
>                                    (define-key proof-mode-map [(C-up)]
>                                      'proof-undo-last-successful-command)
>                                    ))
>
> (add-hook 'proof-goals-mode-hook
>    (lambda () (setq proof-eagerly-raise nil)))
> (add-hook 'proof-response-mode-hook
>    (lambda () (setq proof-eagerly-raise nil)))
>
>> - Do you have a .coqrc?
>
> No
>
>> Best regards,
>> Pierre Courtieu
>
> Thank you in advance for your help.
>
> Best regards,
> Flávio.
>
>
>> 2017-01-13 1:19 GMT+01:00 Flávio L. C. de Moura
>> <flavio.de.moura AT gmail.com>:
>> > Hello Coq users,
>> >
>> > I am facing a strange problem with Proof General, and I didn't realize
>> > how to solve it. When I try to process a .v file (with Coq 8.4pl4), I
>> > get the following screen:
>> >
>> > Don't know what to do with -Q
>> > Usage: coqtop <options>
>> >
>> > Coq options are:
>> > -I dir -as coqdir map physical dir to logical coqdir
>> > -I dir map directory dir to the empty logical path
>> > -include dir (idem)
>> > -R dir -as coqdir recursively map physical dir to logical coqdir
>> > -R dir coqdir (idem)
>> > -top coqdir set the toplevel name to be coqdir instead of Top
>> > -notop set the toplevel name to be the empty logical path
>> > -exclude-dir f exclude subdirectories named f for option -R
>> >
>> > -inputstate f read state from file f.coq
>> > -is f (idem)
>> > -nois start with an empty state
>> > -outputstate f write state in file f.coq
>> > -compat X.Y provides compatibility support for Coq version X.Y
>> > -verbose-compat-notations be warned when using compatibility notations
>> > -no-compat-notations get an error when using compatibility notations
>> >
>> > -load-ml-object f load ML object file f
>> > -load-ml-source f load ML file f
>> > -load-vernac-source f load Coq file f.v (Load f.)
>> > -l f (idem)
>> > -load-vernac-source-verbose f load Coq file f.v (Load Verbose f.)
>> > -lv f (idem)
>> > -load-vernac-object f load Coq object file f.vo
>> > -require f load Coq object file f.vo and import it (Require
>> > f.)
>> > -compile f compile Coq file f.v (implies -batch)
>> > -compile-verbose f verbosely compile Coq file f.v (implies -batch)
>> >
>> > -opt run the native-code version of Coq
>> > -byte run the bytecode version of Coq
>> >
>> > -where print Coq's standard library location and exit
>> > -config print Coq's configuration information and exit
>> > -v print Coq version and exit
>> >
>> > -q skip loading of rcfile
>> > -init-file f set the rcfile to f
>> > -batch batch mode (exits just after arguments parsing)
>> > -boot boot mode (implies -q and -batch)
>> > -emacs tells Coq it is executed under Emacs
>> > -noglob do not dump globalizations
>> > -dump-glob f dump globalizations in file f (to be used by
>> > coqdoc)
>> > -with-geoproof (yes|no) to (de)activate special functions for Geoproof
>> > within Coqide (default is yes)
>> > -impredicative-set set sort Set impredicative
>> > -force-load-proofs load opaque proofs in memory initially
>> >
>> > -lazy-load-proofs load opaque proofs in memory by necessity (default)
>> > -dont-load-proofs see opaque proofs as axioms instead of loading them
>> > -xml export XML files either to the hierarchy rooted in
>> > the directory $COQ_XML_LIBRARY_ROOT (if set) or to
>> > stdout (if unset)
>> > -quality improve the legibility of the proof terms produced
>> > by
>> > some tactics
>> > -h, --help print this list of options
>> >
>> >
>> > I have opam installed, and if I switch to Coq 8.5 or 8.6, everything
>> > works fine. The first line of the above screen says "Don't know what to
>> > do with -Q" but I don't know how to fix this. Any help is very welcome.
>> >
>> > Best regards,
>> > Flávio.