Stream: Coq devs & plugin devs

Topic: Findlib warning


view this post on Zulip Arpan Agrawal (Feb 07 2024 at 19:12):

I'm seeing this warning when running a build script:
CAMLOPT -c -for-pack Ornaments src/ornamental.ml
findlib: [WARNING] Interface search.cmi occurs in several directories: /home/arpan/.opam/copy-coq-8.12/lib/coq/vernac, src/automation/search

How do I make sure it uses the src/automation/search version over the other one?
THanks!

view this post on Zulip Matthieu Sozeau (Feb 08 2024 at 06:22):

The most reliable way is to rename your file to not clash with Coq's modules I think

view this post on Zulip Matthieu Sozeau (Feb 08 2024 at 06:23):

There's an "Extraction Blacklist" option to do that automatically for files generated by extraction, if that's your situation.


Last updated: Oct 13 2024 at 01:02 UTC