Amin Timany (Jul 09 2021 at 10:37): Amin Timany (Jul 09 2021 at 10:37):I have a problem where the make file does not call Coq dep. Interestingly it does work when in the git repository but when I make a separate tar file of source it stops working. I have event tried explicitly running make -f Makefile.coq .Makefile.coq.d but I get the following error:
make: *** No rule to make target .Makefile.coq.d'. Stop.`
Yannick Forster (Jul 09 2021 at 10:43):Is Makefile.coq generated from _CoqProject? And is _CoqProject fixed or generated?
Amin Timany (Jul 09 2021 at 10:51):_CoqProject is handwritten.
Yannick Forster (Jul 09 2021 at 11:02):I have had similar errors in the past when the _CoqProject file contains a file which does not exist. It does not sound related to your problem, but maybe worth to check
Amin Timany (Jul 09 2021 at 11:12):Yes, thanks. this was exactly the problem. The script making the package was not including some files that were in the _CoqProject file.
Yannick Forster (Jul 09 2021 at 17:57):Actually, one might consider this a bug of coq_makefile. coq_makefile should procude Makefiles which output a meaningful error message in such a case.
Yannick Forster (Jul 09 2021 at 17:58):I don't know who to tag, so I'm tagging @Théo Zimmermann in the hope that he can point us to somebody in the coq-makefile-maintainers team
Théo Zimmermann (Jul 10 2021 at 08:01):That would be @Enrico Tassi
Enrico Tassi (Jul 10 2021 at 08:10):This rings a bell
Enrico Tassi (Jul 10 2021 at 08:12):https://github.com/coq/coq/pull/14024
Enrico Tassi (Jul 10 2021 at 08:14):In particular: https://github.com/coq/coq/pull/14024/files#diff-488701d3b7305ecad7279fe1b0646b432283bc7acb4c14068cc9a53da942d9e8 which is in 8.14
Enrico Tassi (Jul 10 2021 at 08:17):Which version are you using Amin? 8.13.x?
Paolo Giarrusso (Jul 10 2021 at 17:07):For Mac users (like me and IIRC @Amin Timany ), another workaround is switching to make 4.X, which gives better error messages compared to Apple's provided make 3.x from ~2 decades ago (2006):
Paolo Giarrusso (Jul 10 2021 at 17:08):$ /usr/bin/make --version
GNU Make 3.81
Copyright (C) 2006 Free Software Foundation, Inc.
This is free software; see the source for copying conditions.
There is NO warranty; not even for MERCHANTABILITY or FITNESS FOR A
PARTICULAR PURPOSE.
This program built for i386-apple-darwin11.3.0
$ make --version
GNU Make 4.3
Built for x86_64-apple-darwin17.7.0
Copyright (C) 1988-2020 Free Software Foundation, Inc.
License GPLv3+: GNU GPL version 3 or later <http://gnu.org/licenses/gpl.html>
This is free software: you are free to change and redistribute it.
There is NO WARRANTY, to the extent permitted by law.
$ which make
/usr/local/opt/make/libexec/gnubin/make
(I got the new make via Homebrew)
Amin Timany (Jul 10 2021 at 17:16):@Enrico Tassi I am using 8.13.1. @Paolo Giarrusso thanks for the tip; the error make gives is indeed not helpful at all.
Amin Timany (Jul 10 2021 at 17:20):Maybe one way to improve the situation is to make the .vo files depend on the result of coqdep. That way, it would not proceed to compile .v files in case it fails to produce the dependencies file.
Last updated: Sep 15 2024 at 13:02 UTC