should `pin-depends` imply `depends` ?

[zapashcanon]

Hi,

I realized that if I have the following owi.opam file:

depends: []
pin-depends: [
  [ "encoding.dev" "git+https://github.com/formalsec/encoding"]
]

Then, running opam install -y ./*.opam --deps-only --with-test would not install encoding.

But if I add it to the depends fields:

depends: [ "encoding" ]
pin-depends: [
  [ "encoding.dev" "git+https://github.com/formalsec/encoding"]
]

Then it would be properly installed with the same command.

I'm wondering if there is a reason why a package being present in pin-depends does not imply it is part of depends ?

Thanks!

[kit-ty-kate]

I'm wondering if there is a reason why a package being present in pin-depends does not imply it is part of depends ?

one reason i can think of out of my head at the moment is: it could be a depopt (optional dependency) instead

[kit-ty-kate]

TODO for us: we could add a lint check to warn users when a pin-depends is not listed in either depends or depopts

[zapashcanon]

Oh indeed, that's a nice idea. In our case, it would have been enough to detect our mistake earlier. :)