Stream: math-comp analysis

Topic: ✔ finmap not found


view this post on Zulip Quentin VERMANDE (Feb 09 2024 at 15:22):

When I try to compile the master branch with MC 2.1.0, I get the error Cannot find a physical path bound to logical path finmap with prefix mathcomp from classical/mathcomp_extra.v. Looking at MC on the remote repo, I can find finmap.v neither in master nor in mathcomp-1. Does anyone have an idea what happens?

view this post on Zulip Pierre Roux (Feb 09 2024 at 15:32):

Stupid question but have you installed finmap? (it's a dependency of classical according to opam show coq-mathcomp-classical).

view this post on Zulip Quentin VERMANDE (Feb 09 2024 at 15:39):

No, that is probably the issue, many thanks. I close as soon as it compiles.

view this post on Zulip Notification Bot (Feb 09 2024 at 15:52):

Quentin VERMANDE has marked this topic as resolved.


Last updated: Jun 22 2024 at 15:01 UTC