<div dir="ltr">I am wondering how difficult it would be to have the "git pin in opam file" feature without the fixpoint resolver. I think in many cases, the dependencies of package foo will be subsumed by the other dependencies listed in the opam file. <br><div>If they are not, I would be happy to have the solver fail, telling me that this situation is too complicated for now. In that case, I would be happy either to come back to my shadow repository solution, or to inline the dependencies in my opam file. </div><div><br></div></div><div class="gmail_extra"><br><div class="gmail_quote">On Wed, May 6, 2015 at 5:51 PM, Ashish Agarwal <span dir="ltr"><<a href="mailto:agarwal1975@gmail.com" target="_blank">agarwal1975@gmail.com</a>></span> wrote:<br><blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex"><div dir="ltr"><div class="gmail_extra"><div class="gmail_quote"><span class="">On Wed, May 6, 2015 at 4:51 AM, Thomas Braibant <span dir="ltr"><<a href="mailto:thomas.braibant@gmail.com" target="_blank">thomas.braibant@gmail.com</a>></span> wrote:<br><div><br></div></span><span class=""><blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex"><div dir="ltr"><div><div class="gmail_extra"><div class="gmail_quote"><div><div>depends: [</div><div>  "asn1-combinators" { = "0.1.1" }<br></div></div><div><div>  ...</div><div>  "foo" { git: "path-to-git/foo#bar"}</div></div><div>]</div></div></div></div></div></blockquote><div><br></div></span><div>This could be very useful. It would also help to allow {path: $HOME/mycode}. With only git pins, developing multiple repos is still difficult. You have to push the changes in one repo before testing them with another repo. Sharing path pins would let multiple developers all work on multiple repos, but each developer can still have fine control over exactly what state each of the individual repos is at. The only slight inconvenience is everyone has to standardize on the paths of their local working directories, but that's not too bad as along as a $HOME variable was allowed.</div><div><br></div><div><br></div></div></div></div>
</blockquote></div><br></div>