Stream: Coq devs & plugin devs

Topic: findlib needs the package to not be installed

view this post on Zulip Karl Palmskog (Nov 15 2022 at 09:39):

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?

view this post on Zulip Enrico Tassi (Nov 15 2022 at 09:46):

No, it can be removed. It is an oversight on my side to have the comment there (and not toplevel)

view this post on Zulip Karl Palmskog (Nov 15 2022 at 09:50):

@Enrico Tassi OK, so I can just submit a PR that removes this text in CoqMakefile.in? We can move it to toplevel maybe?

view this post on Zulip Enrico Tassi (Nov 15 2022 at 09:50):

Yes please, keep the comment but move it outside the rule body

view this post on Zulip Enrico Tassi (Nov 15 2022 at 09:51):

Maybe add "(see the fiddling with the META file)"

view this post on Zulip Enrico Tassi (Nov 15 2022 at 09:51):

since it will be a bit far from the actual code performing the action the comment is about

view this post on Zulip Karl Palmskog (Nov 15 2022 at 09:58):

if anyone else is following this: https://github.com/coq/coq/pull/16806

Last updated: Apr 19 2024 at 18:01 UTC