Join GitHub today
GitHub is home to over 28 million developers working together to host and review code, manage projects, and build software together.Sign up
Share a set of dev repositories #1734
See this discussion for the underlying issue.
Some times ago, we put up a repository containing all these packages, but the current situation is that
In practice we could solve this by some automation, but I think it's possible to do better at opam level. One solution could be to have only the url of the git repository and let opam fetch the
I think the mirage project used to have the same issue. @avsm ?
Yeah, we have a https://github.com/mirage/mirage-dev for the same purpose
The main source of duplication is the opam file itself, but it is useful to have the opam remote to bump version numbers as well. Some automation around this would be useful, but it might be better to let the dust settle on the OPAM 1.2 workflow before diving into it in detail (since OPAM 1.2 does improve the state of affairs by probing for a remote opam file in the pinned repo).
On 17 Sep 2014, at 14:12, Gabriel Radanne email@example.com wrote:
Note that fetching
For me having an opam-admin option that extracts opam files sounds like a good alternative: done only once, and it already downloads and extracts the archives when changed. That won't work with a bare git repo though and requires some heavier infrastructure.
As loosely suggested in this comment one option would be to forget about using dev repos in these cases and provide a simple way to bulk add and remove a set of pins. The former can already be solved by using
In contrast to the opam repo approach, one thing that this wouldn't handle though is the addition/removal of pacakges (you'd have to redowload the published file). This could be aleviated by having pin sources: