Stream: Coq users

Topic: makefile does not call coqdep


view this post on Zulip 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.`

view this post on Zulip Yannick Forster (Jul 09 2021 at 10:43):

Is Makefile.coq generated from _CoqProject? And is _CoqProject fixed or generated?

view this post on Zulip Amin Timany (Jul 09 2021 at 10:51):

_CoqProject is handwritten.

view this post on Zulip 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

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip 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

view this post on Zulip Théo Zimmermann (Jul 10 2021 at 08:01):

That would be @Enrico Tassi

view this post on Zulip Enrico Tassi (Jul 10 2021 at 08:10):

This rings a bell

view this post on Zulip Enrico Tassi (Jul 10 2021 at 08:12):

https://github.com/coq/coq/pull/14024

view this post on Zulip 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

view this post on Zulip Enrico Tassi (Jul 10 2021 at 08:17):

Which version are you using Amin? 8.13.x?

view this post on Zulip 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):

view this post on Zulip 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

view this post on Zulip Paolo Giarrusso (Jul 10 2021 at 17:08):

(I got the new make via Homebrew)

view this post on Zulip 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.

view this post on Zulip 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: Feb 01 2023 at 12:30 UTC