Opened 12 years ago
Last modified 11 years ago
#454 assigned enhancement
coq mode: compile before import fails when no .v file
| Reported by: | courtieu | Owned by: | hendrik |
|---|---|---|---|
| Priority: | major | Milestone: | PG-Emacs-4.3 |
| Component: | 2:pg-emacs | Keywords: | coq compile |
| Cc: |
Description
Some users use .vo files without having the corresponding .v files. the compile before require feature should consider a .vo up-to-date if there is no corresponding .v file.
Change History (4)
comment:1 Changed 12 years ago by
| Owner: | changed from David Aspinall to coquser |
|---|---|
| Status: | new → accepted |
comment:2 Changed 12 years ago by
| Milestone: | PG-Emacs-4.2 → PG-Emacs-4.3 |
|---|
comment:3 Changed 11 years ago by
| Type: | defect → enhancement |
|---|
I suggest to keep this ticket open until coqdep changes the warning, which seems not to be very likely. Set to enhancement, because using .vo's without .v's is very obscure.
Hendrik
comment:4 Changed 11 years ago by
| Owner: | changed from coquser to hendrik |
|---|---|
| Status: | accepted → assigned |
Note: See
TracTickets for help on using
tickets.
Hi,
this is actually a coqdep bug, which warns that the library is missing, if only the .vo file is present, see coq bug #2910 (https://coq.inria.fr/bugs/show_bug.cgi?id=2910). Therefore, I cannot do anything about this problem.
There is a workaround using coq-compile-ignored-directories. If you have a.vo without a.v, create b.v with the line "Require Import b.", compile b.v manually and then add b.v to coq-compile-ignored-directories. Note that each member of coq-compile-ignored-directories is matched against the .vo file name, so you can actually ignore single files, and not only complete directories.
Bye,
Hendrik