The Coq mailing list

[Clément Pit--Claudel <clement.pit AT gmail.com>]

Hey Flávio,

This could also be a problem with the version detection (maybe PG is 
improperly detecting your copy of Coq as 8.5).
Can you open a PG bug report?

Thanks!
Clément.

On 2017-01-13 11:45, Flávio L. C. de Moura wrote:
> 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.
>

Attachment: signature.asc
Description: OpenPGP digital signature