In 8.16.0 and on Coq
master I get this worrying message about findlib anytime I install something using
coq_makefile (even pure Coq projects):
$ make install .... INSTALL theories/MyFile.glob /home/user/.opam/my-opam-switch/lib/coq//user-contrib/MyProject/ # findlib needs the package to not be installed, so we remove it before # installing it
Should this message really be echoed?
No, it can be removed. It is an oversight on my side to have the comment there (and not toplevel)
@Enrico Tassi OK, so I can just submit a PR that removes this text in
CoqMakefile.in? We can move it to toplevel maybe?
Yes please, keep the comment but move it outside the rule body
Maybe add "(see the fiddling with the META file)"
since it will be a bit far from the actual code performing the action the comment is about
if anyone else is following this: https://github.com/coq/coq/pull/16806
Last updated: Dec 01 2023 at 06:01 UTC