Stream: Coq devs & plugin devs

Topic: ✔ findlib errors


view this post on Zulip Jason Gross (Feb 11 2022 at 05:03):

Where do I go looking for the source of this error?

# INSTALL BigZ/BigZ.glob D:\a\fiat-crypto\fiat-crypto\_opam\lib/coq//user-contrib/Bignums\\BigZ
# # findlib needs the package to not be installed, so we remove it before
# # installing it
# /bin/sh: D:afiat-cryptofiat-crypto_opambin/ocamlfind.exe: No such file or directory

view this post on Zulip Guillaume Melquiond (Feb 11 2022 at 05:28):

That is the content of the Makefile generated by coq_makefile. More precisely, this is the findlib_remove directive. No idea whether adding some double quotes there would fix the issue.

view this post on Zulip Jason Gross (Feb 11 2022 at 06:22):

Reported as https://github.com/coq/coq/issues/15664 and fixed in https://github.com/coq/coq/issues/15665

view this post on Zulip Notification Bot (Feb 11 2022 at 06:22):

Jason Gross has marked this topic as resolved.


Last updated: Feb 06 2023 at 00:03 UTC