I'm opening this issue to track the result of a recent discussion on Gitter.
Coq 8.11.1 release broke coq-mathcomp-finmap on opam and some other packages that depend on it: coq-mathcomp-multinomials, coq-coqeal, and coq-ceramist.
Adding finmap to Coq's CI will help prevent this. Although it requires that the maintainers are ready to communicate with the Coq dev team in a timely manner and accept occasional patches. See https://github.com/coq/coq/blob/master/dev/ci/README-users.md for more detail.
I'm opening this issue to track the result of a recent discussion on Gitter.
Coq 8.11.1 release broke
coq-mathcomp-finmapon opam and some other packages that depend on it:coq-mathcomp-multinomials,coq-coqeal, andcoq-ceramist.Adding
finmapto Coq's CI will help prevent this. Although it requires that the maintainers are ready to communicate with the Coq dev team in a timely manner and accept occasional patches. See https://github.com/coq/coq/blob/master/dev/ci/README-users.md for more detail.