The Coq mailing list

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

Hi,

I found a way to fix this problem, but I am not sure about it. I changed
the file coq-system.el that comes with Proof General as follows: The two
occurrences of -Q below were changed to -q and I recompiled Proof
General. Therefore, it seems to be a problem of Proof General. Do you
agree?


(defun coq-option-of-load-path-entry (entry &optional pre-v85)
  "Translate a single ENTRY from `coq-load-path' into options.
See `coq-load-path' for the possible forms of ENTRY and to which
options they are translated.  Use a non-nil PRE-V85 flag to
request compatibility handling of flags."
  (if pre-v85
      ;; FIXME Which base directory do we expand against? Should the entries 
of
      ;; load-path just always be absolute?
      ;; NOTE we don't handle 'recnoimport in 8.4, and we don't handle 'nonrec
      ;; in 8.5.
      (pcase entry
        ((or (and (pred stringp) dir) `(ocamlimport ,dir))
         (list "-I" (expand-file-name dir)))
        (`(nonrec ,dir ,alias)
         (list "-I" (expand-file-name dir) "-as" alias))
        ((or `(rec ,dir ,alias) `(,dir ,alias))
         (list "-R" (expand-file-name dir) alias)))
    (pcase entry
      ((and (pred stringp) dir)
       (list "-Q" (expand-file-name dir) ""))
      (`(ocamlimport ,dir)
       (list "-I" (expand-file-name dir)))
      (`(recnoimport ,dir ,alias)
       (list "-Q" (expand-file-name dir) alias))
      ((or `(rec ,dir ,alias) `(,dir ,alias))
       (list "-R" (expand-file-name dir) alias)))))

Best regards,
Flávio.

flavio.de.moura AT gmail.com
 (Flávio L. C. de Moura) writes:

> Hi Pierre,
>
> The *Messages* buffer is not very informative, except from the
> fact that coq is launched by the command 'coqtop -emacs -Q' and that
> there is no Coq project file. I couldn't find a tip about where the -Q
> comes from. Here is the output:
>
> Loading coq...
> Welcome to Coq Proof General!
> Coq abbrevs already exists, default not loaded
> Loading coq...done
> Coq project file not detected.
> Welcome to company-coq! Use M-x company-coq-tutorial to get started. [2 
> times]
> Right click (or C-click) to show the refactoring menu.
> Coq project file not detected.
> The Coq Proof Assistant, version 8.4pl4 (May 2016)
> compiled on May 06 2016 08:27:03 with OCaml 4.01.0
> Starting: coqtop -emacs -Q /Users/flaviomoura/workspace-git/tlc/src 
> Process coq exited abnormally with code 1
> , shutting down scripting...
> *coq*, cleaning up and exiting...
> *coq* exited.
> Process coq exited abnormally with code 1
> , shutting down scripting...done.
> proof-activate-scripting: coq process exited!
>
> I hope you can find something useful from this output.
>
> Thank you again!
> Flávio.
>
>
> Pierre Courtieu 
> <pierre.courtieu AT gmail.com>
>  writes:
>
>> 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.