Do you have to run this command manually, and does it mutate the shell state? That's one thing that frustrated me with opam in the past as well. I couldn't just jump into a directory and build a thing, then switch to another project directory - there was a lot of manual switching and unswitching of packages if I recall correct?
Is it possible to install multiple tools globally using opam that use disjoint library versions? Like, I might want to install Abella and Coq side-by-side, but they might have conflicting version requirements. I think I was super excited about opam 2, then tried installing one thing, only to have it break again when I installed something else.
Is it possible to have multiple versions of the same libray in the same project, or does the constraint solver need to find a single solution for each library? [1]