> On 26 Aug 2019, at 18:46, Jasmin Blanchette <[email protected]> wrote: > > Gerwin wrote: > >> There is another option for the AFP: we could host on github and use the >> mercurial git plugin [https://hg-git.github.io] to work with it as if it was >> a mercurial repo. I don’t have much experience with how stable that option >> is, but it would be free and it would be easy on account management. > > I've been using hg-git since 2015, notably for my main private repository. A > quick check on my disk reveals that's how I'm accessing 32 git repositories.
That sounds encouraging! > I find that the plugin works well for branch-free repositories. I don't know > what it would do with git branches, and for such repositories I use git > directly. > > The main things I noticed about hg-git: > > 1. The first time you use it it refuses to push. One has to enter > > hg bookmark -f master > > 2. When merging, "hg merge" is never enough; you need e.g. "hg merge tip”. These two would be acceptable to me, esp now that we know about them. > 3. Once in a while, I get low level Python errors. That gets sorted out by > updating hg-git. hg-git seems to depend on quite a bit of Python libraries, > so it's easy for them to get out of sync if I update my system. That is a bit more worrying. I personally don’t mind, but I could imagine others getting confused about which parts need updating. Is this usually triggered by you updating python specifically, or does it also occur with standard OS updates? (Mac or Linux?) > 4. You can't refer to revision numbers directly in your change logs, because > these are different in git and hg. That would be expected, yes, the git revision id would be the real identifier in this case. Does hg-git expose the git id in some usable way? Cheers, Gerwin _______________________________________________ isabelle-dev mailing list [email protected] https://mailman46.in.tum.de/mailman/listinfo/isabelle-dev
