coq
Not pinning package versions results in non-expert users accidentally changing their version of Coq.
I have two distinct researchers that have told me that they used Coq Platform to install Coq but ended up with an unexpected version of Coq in their Platform switch. This usually happens when users want to install some other package with opam install but this package is (directly or indirectly) incompatible with their version of Coq. Users will gladly answer yes to opam's plan without properly reading it and without noticing that it includes downgrading Coq (for instance).
Given the primary goals of the Platform (reliability and reproducibility), I think that the choice to not pin the packages should be reconsidered. I am fine with leaving the option to not pin in a Coq Platform expert mode, but by default, IMHO all the packages installed by the Coq Platform should be pinned. It is always possible for a user who knows what they are doing to unpin some specific package later.
Related to this, many users seem unaware that the recommended upgrade path for the Coq Platform is to reinstall it and create a new switch. They think that they should do opam update && opam upgrade, and this is reinforced by the fact that these commands may actually work (but lead to an unknown state). Pinning would solve half the problem. I think solving the other half requires writing an upgrade documentation and linking from the release notes and release announcements.
I am open to this, but I am not sure if it wouldn't be sufficient / better to just pin Coq itself.
Regarding docs: there is "Maintaining an installation" section on the Coq Platform main readme. I just fear that it is made in such a way that it is difficult to link this section.
Mid term we should have a Coq Platform opam package, which would solve this, but this currently conflicts with the MinGW opam repo (they didn't take some required fixes).
I now also pin packages in parallel mode (the sequential mode already had a few packages pinned because otherwise some packages get recompiled cause of downgrades later in some picks). I pinned the version of coq in all picks. I think this is the best solution - it makes coq stable, but it leaves enough flexibility to use opam.