search

coq / coq

Coq is a formal proof management system. It provides a formal language to write mathematical definitions, executable algorithms and theorems together with an environment for semi-interactive development of machine-checked proofs.
https://coq.inria.fr/
GNU Lesser General Public License v2.1
4.79k stars 640 forks source link

coqdep treats inclusion paths differently from coqc #3720

Closed coqbot closed 9 years ago

coqbot commented 9 years ago

Note: the issue was created automatically with bugzilla2github tool

Original bug ID: BZ#3720 From: @jwiegley Reported version: 8.4 CC: @aspiwack

coqbot commented 9 years ago

Comment author: @jwiegley

I have ssreflect installed on my system, and when I run coqc pointed at it, everything works as expected:

coqc -I . -R ~/.nix-profile/lib/coq/8.4/user-contrib/Ssreflect Ssreflect Lib.v

However, the exact same arguments with coqdep fails:

coqdep -I . -R ~/.nix-profile/lib/coq/8.4/user-contrib/Ssreflect Ssreflect Lib.v

The output is:

*** Warning: in file Lib.v, library Ssreflect.choice.v is required and has not been found in loadpath!

This is very unfortunate, because Proof General in Emacs uses coqdep, so legitimate code is unable to be checked.

coqbot commented 9 years ago

Comment author: @jwiegley

I should further mention that the ssreflect installation only installs the .vo files, not the .v files, so perhaps that's part of the problem here. Still, this shouldn't stop Proof General from type-checking a file, should it?

coqbot commented 9 years ago

Comment author: @jwiegley

This is a Proof General bug. When coq-compile-before-require is non-nil, it will try to compile dependencies when they are required. It should be ignoring dependencies with no source.

coqbot commented 9 years ago

Comment author: @aspiwack

Well, it is actually a coqdep thing. When coqdep requires a file and does not find a source for a required it issues a warning or an error (I forget which), which thwarts the emacs recompilation (which could work around the issue, but you will find it is not necessarily what you want. Imagine you've just renamed a file and the .vo with the old name still lingers around).

The "solution" is to install stuff in places recognised by Coq as library installation places. Which you seem to have done. In this case you do not need to pass the -R option to coqc/coqdep.

Try removing the -R option from your _CoqProject file, and you should be good.

coqbot commented 9 years ago

Comment author: @jwiegley

Ah, right you are. I'm using Nix and had simply forgotten to set this in my environment:

export COQPATH=$HOME/.nix-profile/lib/coq/8.4/user-contrib
coqbot commented 9 years ago

Comment author: @jwiegley

This is not a real issue in coqdep, but with Proof General's heuristics and the fact that I was not using Ssreflect from a standard location.