coq-club AT inria.fr
Subject: The Coq mailing list
List archive
- 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
A.v B.v _CoqProject
[abhishek@optiplex temp]$ cat B.v
Require Import Test.A.
Definition y :=4.
Require Import Test.A.
Definition y :=4.
[abhishek@optiplex temp]$ cat _CoqProject
-Q . Test
A.v
B.v
C.v
-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.
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
-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]$
COQDEP VFILES
COQC A.v
COQC B.v
[abhishek@optiplex temp]$
- [Coq-Club] COQDEP not called if _CoqProject has nonexistent .v files, Abhishek Anand, 01/31/2019
- Re: [Coq-Club] COQDEP not called if _CoqProject has nonexistent .v files, Enrico Tassi, 01/31/2019
- Re: [Coq-Club] COQDEP not called if _CoqProject has nonexistent .v files, Abhishek Anand, 01/31/2019
- Re: [Coq-Club] COQDEP not called if _CoqProject has nonexistent .v files, Enrico Tassi, 01/31/2019
Archive powered by MHonArc 2.6.18.