Skip to Content.
Sympa Menu

coq-club - [Coq-Club] COQDEP not called if _CoqProject has nonexistent .v files

coq-club AT inria.fr

Subject: The Coq mailing list

List archive

[Coq-Club] COQDEP not called if _CoqProject has nonexistent .v files


Chronological Thread 
  • From: Abhishek Anand <abhishek.anand.iitg AT gmail.com>
  • To: coq-club <coq-club AT inria.fr>
  • Subject: [Coq-Club] COQDEP not called if _CoqProject has nonexistent .v files
  • Date: Wed, 30 Jan 2019 16:44:16 -0800
  • Authentication-results: mail2-smtp-roc.national.inria.fr; spf=None smtp.pra=abhishek.anand.iitg AT gmail.com; spf=Pass smtp.mailfrom=abhishek.anand.iitg AT gmail.com; spf=None smtp.helo=postmaster AT mail-yw1-f45.google.com
  • Ironport-phdr: 9a23:SQGqSxadDY5fD7czYfy+Vt7/LSx+4OfEezUN459isYplN5qZoMW7bnLW6fgltlLVR4KTs6sC17KG9fi4EUU7or+5+EgYd5JNUxJXwe43pCcHRPC/NEvgMfTxZDY7FskRHHVs/nW8LFQHUJ2mPw6arXK99yMdFQviPgRpOOv1BpTSj8Oq3Oyu5pHfeQpFiCa+bL9oMBm6sRjau9ULj4dlNqs/0AbCrGFSe+RRy2NoJFaTkAj568yt4pNt8Dletuw4+cJYXqr0Y6o3TbpDDDQ7KG81/9HktQPCTQSU+HQRVHgdnwdSDAjE6BH6WYrxsjf/u+Fg1iSWIdH6QLYpUjmk8qxlSgLniD0fOjE28G/ZhM9+gr9Frh29vBFw2ZLYbZuPOfZiYq/Qf9UXTndBUMZLUCxBB5uxYpcUAOoBPOZYtIn9qEUNrRCjGQSsAvngyjlViXTr2qA1yf8uEQHH3Aw7H9IBrnfUoM/vO6cUS++1yrTHwS/Cb/NXxTf955PFch8kof6WXLJwddDdxlUoFwPAl1idr5HuMT2S1uQIqWeb7uxgWPqzhG4gsQFxpCagxsMoioXTmI0a103E+CNky4g2Pd21UFB3bcKgHZdKtCyXN5F6Tt4jTm11oio3xb0LtJimdyYQ0psn3QTQa/mffoiI/B3jUOGRLC99hH1/ebK/gw++8Eiuy+HhT8W03llHoypfntnDsXAN0BPT6syZRfdn4kih3jOP2xjS6uFCP080ibLWJ4A9zrM0jJYeskTOEjXrlEj3kaOabEop9+iw5+TieLrmp5ucN4FuigH5N6QjgtawDv84MggPRGib+fqz1L758ULjRrVFlPs2nbTDvJDbJMQbuqG5DhRa0oYm8Rm/DjOm3M4EknkAKVJJYAiHgJTxO1HSPPD4Cu+yjEirkDdy3vzJIrnhAojWIXXYi7fgfbN961ZGxwYpzNBf4YhUCrAbL/7pVE/xro+QMhhsOAuthu3jFd81gogZQCeEBrKTGKLUq16BoOw1dbqifogQ7R/3K/k+5/PtxVY/kFkRNf2g15sWc3C1HbJvJUyfbTztg8sOOWgPtws6CuftjQvRAnZoe3+uUvdktXkAA4W8ANKbH9H/sPm6xC6+W6ZuSCVDA1GIH23vctzdCfgJYSOWZMRml25dDOTze8oazRir8TTC5f9/NOONo38XsJvi0J5+4OiBzUhvpwwxNNyU1iS2d08xnm4MQGVrjqV2oEg420jalKYk3rpXEttc4/4PWQA/Z8bR

I deleted a .v file and forgot to remove it from `_CoqProject`. Suddenly, I was getting too many errors that indicated that `make` is trying to compile files in an order that disrespects the dependencies.
Here is a minimal example to illustrate the problem:

[abhishek@optiplex temp]$ ls
A.v  B.v  _CoqProject

[abhishek@optiplex temp]$ cat B.v  
Require Import Test.A.

Definition y :=4.

[abhishek@optiplex temp]$ cat _CoqProject  
-Q . Test

A.v
B.v
C.v

[abhishek@optiplex temp]$ coq_makefile -f _CoqProject -o Makefile

[abhishek@optiplex temp]$ make -j3
make[1]: *** No rule to make target 'C.v', needed by 'C.vo'.  Stop.
make[1]: *** Waiting for unfinished jobs....
COQC A.v
COQC B.v
File "./B.v", line 1, characters 15-21:
Error: Unable to locate library Test.A.


Clearly, the coq_makefile generated Makefile invoked coqc on B.v before A.v was compiled. Is it desirable to totally ignore the dependencies if _CoqProject has nonexistent .v files?

When I removed the nonexistent C.v from _CoqProject, everything works as expected. Also unlike before, I see a COQDEP invocation on `make`

[abhishek@optiplex temp]$ cat _CoqProject  
-Q . Test

A.v
B.v

[abhishek@optiplex temp]$ coq_makefile -f _CoqProject -o Makefile

[abhishek@optiplex temp]$ make -j3 -k
COQDEP VFILES
COQC A.v
COQC B.v
[abhishek@optiplex temp]$




--
-- Abhishek
http://www.cs.cornell.edu/~aa755/



Archive powered by MHonArc 2.6.18.

Top of Page