Stream: math-comp analysis

Topic: opam & dev packages


view this post on Zulip Pierre-Yves Strub (Feb 08 2021 at 16:42):

Hi. I don't understand why when I install version 0.3.5, opam pulls dev versions of Coq & mathcomp & etc, etc...

view this post on Zulip Pierre-Yves Strub (Feb 08 2021 at 16:43):

I would expect opam to pull dev packages only if asked explicitly.

view this post on Zulip Cyril Cohen (Feb 08 2021 at 19:51):

This is anoying, the main reason is for CI purposes (where relevant stuff is pinned) we always include dev deps.
My personal way out is not to add the extra-dev remote to my opam.
I wonder how @Pierre Roux and @Erik Martin-Dorel deal with this...

view this post on Zulip Erik Martin-Dorel (Feb 09 2021 at 01:25):

Hi, I guess I do exactly as @Cyril Cohen suggests: I only add the coq-released opam repo in my main opam switches; otherwise it's true that the packages that have a "dev" version would automatically be promoted (as the implied order on the opam version numbers indeed enforces that forall x, "8.x" <= "dev"…), but a workaround in this case (if extra-dev is really necessary), can just be version-pinning the offending packages.
otherwise FWIW, there is another solution to have a development version of a package in one's switch without importing the whole extra-dev: opam's git-pinning (I had written a quick summary of this in that stackoverflow thread)


Last updated: Aug 11 2022 at 01:03 UTC