The Coq mailing list

[flavio.de.moura AT gmail.com (Flávio L. C. de Moura)]

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.