6 ms·

FWIW, this has gotten a certain amount of attention on HN over the years since it was begun but it's instantly noticeable that patches tailed off and stopped la

by xoa 7y ago

FWIW, this has gotten a certain amount of attention on HN over the years since it was begun but it's instantly noticeable that patches tailed off and stopped last June. Naturally that raises the question of "is this even still alive", and last month the starter of the project, Pierre Meunier, posted a response to a query about that indicating a major rewrite is in progress: ---- https://discourse.pijul.org/t/is-this-project-still-active-yes-it-is/451 https://discourse.pijul.org/t/is-this-project-still-active-y... >Is Pijul still under active development? >That’s right, the last patches are pretty old. A few things have happened since then, but they’re not public yet. This has included (1) thinking about new algorithms to solve our remaining problems and (2) thinking about the future and sustainability of the project, including its funding. >Another thing going on is a major rewrite of libpijul. This project was our first Rust project, was started in a pretty early version of Rust, on an incomplete theory that was only finalised in 2019. Until then it wasn’t clear what functions and types we wanted to expose, and how to document them. >I’m currently reorganising everything, in particular using a lot more proc-macros, and making it more general so that it can run on various backends (well, actually different variants of Sanakirja). >We will hopefully have news pretty soon. I’d love to fix all the bugs in the Nest discussions, my hope is that many of them will simply disappear with the rewrite. ---- Of course, everyone here probably knows about the risks of major rewrites, though granted that's lessoned for something that began in the research phase and never got close to a 1.0 and major uptake. It is a pretty interesting project and I'd love to see it go well, so hopefully it can make the series of transitions to something more mature and self-sustaining! For now though it looks like things will be in a bit of stasis, and everyone will have to wait and see what emerges on the other side.

eikenberry 7y ago
> risks of major rewrites The risks are mostly in relation to your existing users. As this was more of a prototype, with no real user base, in my mind it fits more with the "throw the first away" line of thinking.
potiuper 7y ago
Rust or any procedural language seems not to be the most apt lang to do a first implementation / rewrite of a patch theory. Patches themselves have already been generalized to paths using HOTT ref: https://www.cs.cmu.edu/~rwh/papers/htpt/paper.pdf https://www.cs.cmu.edu/~rwh/papers/htpt/paper.pdf. The takeaway from https://arxiv.org/abs/1311.3903 https://arxiv.org/abs/1311.3903 is the use of commutation to allow for push out while the HOT ref discusses pseudocommutation regarding merges. See the footnote about commutation being inaccurate term regarding darts model. With the addition of ojo "ghost" deletes and pseudo edges, a formal implementation should provide a non-exponential model/algorithm amenable for optimization.
- dan-robertson 7y ago
  What does HOT stand for? It’s surely not higher order types but I can’t think of anything beginning with homotopy.
  - potiuper 7y ago
    Abbreviation for Homotopy Type: https://homotopytypetheory.org/book/ https://homotopytypetheory.org/book/
- dan-robertson 7y ago
  I tried to read that HOTT paper. I should preface this by saying that my homotopy type theory knowledge is basically 0 and my topology/homotopy/algebra knowledge is limited and rusty. Here are some notes I took as I read it: 1. I guess I’m starting off not understanding the relevance of this paper to distributed version control. If you have a type R for states of your repository and patches are then paths of type a =_R b, with certain properties of patches being certain path homotopies, surely many functions giving you a path are somewhat boring (because a path should exist between any two repositories). But maybe the point will be proofs about the equality and construction of those paths. Or maybe it is to get functoriality for free. 2. In this formalisation patches are paths so they have to form a groupoid but if you want a distributed version control system, I think you don’t want inverses of patches. You don’t want p . p^-1 = 1 because you want properties like repo state = (in some sense) the composition of all patches in a set, and if patches form a groupoid then the sets {p, p^-1} and {p, p^-1, p} are equal (ie there isn’t a way to distinguish “apply p” from “unrevert p” and you need some way to distinguish them if you want to be distributed. But maybe there is some way to work around this. 3. How to think about apd? If I think of B like a fibration of A then I guess it makes sense but it seems weaker than that. I don’t really understand why PathOver should depend on p (and not f too) 4. Perhaps the paper aims to construct a patch theory where any two patches are equal (which I guess means homotopic) under their laws. My intuition of a patch would be that the answer to this is yes but I’m not confident. Maybe that isn’t what the paper is about. 5. Well I’ve heard a bunch about the univalence axiom so I’m glad to finally get a definition of it. 6. In 2.4.1 the definition of reversing seems wrong to me. It seems like it only gets the right types because loop has the same type as refl. It feels like it’s actually splitting up a path into its individual loops, reversing them, then putting them together in the same order. On the other hand I think I candefine a type like a : I ; b : I ; i : a = b, and then write rev a = b; rev b = a; ap rev i = ! i. And I suppose one could define a circle type with two points and two paths and it would look ok. So maybe the loop example doesn’t matter because it’s all equivalent no matter how it feels. 7. Describing patch equivalence as equivalent affect on the repo isn’t clear to me: is the repository just the (visible) contents of the files or does it also include hidden state related to deletions/merges/applied patches. I’m guessing this paper needs it to be the former. 8. It would have been nice if the paper stuck to one composition order but whatever 9. My concerns about reverting are slightly allayed by the paragraph about being careful with contexts but only slightly because of the following paragraph about coincidence. I guess invert ability is fine so long as no one cannot actually commit a patch and its inverse 10. Perhaps HTT gives a better framework for defining and proving things about pseudocommutation. Maybe that is the point of this paper. I would guess (without having read the paper) that that isn’t particularly well formalised in category theory (but formalising a merge as a push out does seem foot to me). 11. Ah so inverses + pseudocommutation laws gives you merges. That seems pretty nice. Does this let one define pseudocommutation in the categorical approach? I guess if you have inverses and want the pseudocommutation of A -f-> B -g-> C, you compute the push out of the span A <-!f- B -g-> C as A -h-> D <-k- C and then say the pseudocommutation is (h,!k). But my (vague) understanding of that theory is that it wouldn’t have nontrivial inverses 12. At the end of sec 3, I feel like I’m left wanting pseudocommutation better defined. They say how their definition falls short but they don’t say they will improve it. Currently it feels like they could go on to prove a bunch of nice properties about version control systems which are allowed to resolve merges by reverting the conflicting packages. Fingers crossed everything will make sense soon. 13. The “topological meaning” paragraph seems weirdly written. If the reader knows what a universal cover is then it should say “this is the universal cover of the circle” and then provide some actual topological colour to the description. And if the reader doesn’t know what a universal cover is then this information won’t add anything. Might as well have said “this is called the fubar of the circle” and had the same effect. 14. I would have rather had a paragraph about universality than a weird one-liner about fundamental groups 15. In sec 4.2 their patch types are all the same. Are we skipping some difficulties because of this? 16. In sec 5, why do the patches not first require that the document contains the strings they care about? I guess that isn’t necessary. 17. Why no homotopy that ! s<>t@i = s<>t@i or that <> is symmetric? Maybe it’s not used. But it feels like the authors are admitting a more complex universal cover than they intend from the semantics they give by doing that. 18. I’m left somewhat wondering what the point is. I would say that the motto of the category theory paper which I haven’t read but which pijul is somewhat related to would be “patches form a category and merges are push outs. You can use category theory to extend the category of patches into one where all push outs exist.” For this paper I guess it’s something like “homotopy type theory gives you some tools for working with groupoids. Here it is applied to patches.” But otherwise I’m not really sure what the relevance is to the implementation or correctness of a dvcs is. They don’t really provide a tool to show that your pseudocommutation function does what it’s supposed to do and so you don’t know that your merges work either. I guess if you could prove that your merges are push outs, does that imply the pseudocommutation is correct? With the category theory paper it at least gives you “correct” merges and a good idea for how to think about patches.
otabdeveloper4 7y ago
"v2 major rewrite, to make the code clean and stuff" is where dumb projects go to die. (There's even a scientific name for this phenomenon.)
rstarast 7y ago
The combination of > (2) thinking about the future and sustainability of the project, including its funding. and the rewrite apparently not happening in the open casts some doubt as to whether the project will remain fully open source.
- Freak_NL 7y ago
  > […] the rewrite apparently not happening in the open […] That's a major red flag for a FOSS DVCS that aims to exist as a valid alternative for existing tools like git. Fine for a hobby project, portfolio project, or experiment of course.
- pmeunier 7y ago
  > the rewrite apparently not happening in the open I'm the author of the rewrite. It will almost certainly be open source when it's done, but it is not open right now, because: - the license of the current version has not been properly observed by other projects in the past. - this project keeps getting bashed for "corrupting repositories" and "changing formats constantly", even though it is announced as experimental everywhere (also, some corruption claims have been wrong in the past, and we have released converters every time the formats have changed). Therefore, allowing people to test the new version as it is being debugged would probably not improve this situation.
  - rstarast 7y ago
    Thank you, that's good to hear! Your arguments are valid.

by xoa 7y ago

eikenberry 7y ago

> risks of major rewrites The risks are mostly in relation to your existing users. As this was more of a prototype, with no real user base, in my mind it fits more with the "throw the first away" line of thinking.

potiuper 7y ago

Rust or any procedural language seems not to be the most apt lang to do a first implementation / rewrite of a patch theory. Patches themselves have already been generalized to paths using HOTT ref: https://www.cs.cmu.edu/~rwh/papers/htpt/paper.pdf https://www.cs.cmu.edu/~rwh/papers/htpt/paper.pdf. The takeaway from https://arxiv.org/abs/1311.3903 https://arxiv.org/abs/1311.3903 is the use of commutation to allow for push out while the HOT ref discusses pseudocommutation regarding merges. See the footnote about commutation being inaccurate term regarding darts model. With the addition of ojo "ghost" deletes and pseudo edges, a formal implementation should provide a non-exponential model/algorithm amenable for optimization.

dan-robertson 7y ago
What does HOT stand for? It’s surely not higher order types but I can’t think of anything beginning with homotopy.
- potiuper 7y ago
  Abbreviation for Homotopy Type: https://homotopytypetheory.org/book/ https://homotopytypetheory.org/book/
dan-robertson 7y ago
I tried to read that HOTT paper. I should preface this by saying that my homotopy type theory knowledge is basically 0 and my topology/homotopy/algebra knowledge is limited and rusty. Here are some notes I took as I read it: 1. I guess I’m starting off not understanding the relevance of this paper to distributed version control. If you have a type R for states of your repository and patches are then paths of type a =_R b, with certain properties of patches being certain path homotopies, surely many functions giving you a path are somewhat boring (because a path should exist between any two repositories). But maybe the point will be proofs about the equality and construction of those paths. Or maybe it is to get functoriality for free. 2. In this formalisation patches are paths so they have to form a groupoid but if you want a distributed version control system, I think you don’t want inverses of patches. You don’t want p . p^-1 = 1 because you want properties like repo state = (in some sense) the composition of all patches in a set, and if patches form a groupoid then the sets {p, p^-1} and {p, p^-1, p} are equal (ie there isn’t a way to distinguish “apply p” from “unrevert p” and you need some way to distinguish them if you want to be distributed. But maybe there is some way to work around this. 3. How to think about apd? If I think of B like a fibration of A then I guess it makes sense but it seems weaker than that. I don’t really understand why PathOver should depend on p (and not f too) 4. Perhaps the paper aims to construct a patch theory where any two patches are equal (which I guess means homotopic) under their laws. My intuition of a patch would be that the answer to this is yes but I’m not confident. Maybe that isn’t what the paper is about. 5. Well I’ve heard a bunch about the univalence axiom so I’m glad to finally get a definition of it. 6. In 2.4.1 the definition of reversing seems wrong to me. It seems like it only gets the right types because loop has the same type as refl. It feels like it’s actually splitting up a path into its individual loops, reversing them, then putting them together in the same order. On the other hand I think I candefine a type like a : I ; b : I ; i : a = b, and then write rev a = b; rev b = a; ap rev i = ! i. And I suppose one could define a circle type with two points and two paths and it would look ok. So maybe the loop example doesn’t matter because it’s all equivalent no matter how it feels. 7. Describing patch equivalence as equivalent affect on the repo isn’t clear to me: is the repository just the (visible) contents of the files or does it also include hidden state related to deletions/merges/applied patches. I’m guessing this paper needs it to be the former. 8. It would have been nice if the paper stuck to one composition order but whatever 9. My concerns about reverting are slightly allayed by the paragraph about being careful with contexts but only slightly because of the following paragraph about coincidence. I guess invert ability is fine so long as no one cannot actually commit a patch and its inverse 10. Perhaps HTT gives a better framework for defining and proving things about pseudocommutation. Maybe that is the point of this paper. I would guess (without having read the paper) that that isn’t particularly well formalised in category theory (but formalising a merge as a push out does seem foot to me). 11. Ah so inverses + pseudocommutation laws gives you merges. That seems pretty nice. Does this let one define pseudocommutation in the categorical approach? I guess if you have inverses and want the pseudocommutation of A -f-> B -g-> C, you compute the push out of the span A <-!f- B -g-> C as A -h-> D <-k- C and then say the pseudocommutation is (h,!k). But my (vague) understanding of that theory is that it wouldn’t have nontrivial inverses 12. At the end of sec 3, I feel like I’m left wanting pseudocommutation better defined. They say how their definition falls short but they don’t say they will improve it. Currently it feels like they could go on to prove a bunch of nice properties about version control systems which are allowed to resolve merges by reverting the conflicting packages. Fingers crossed everything will make sense soon. 13. The “topological meaning” paragraph seems weirdly written. If the reader knows what a universal cover is then it should say “this is the universal cover of the circle” and then provide some actual topological colour to the description. And if the reader doesn’t know what a universal cover is then this information won’t add anything. Might as well have said “this is called the fubar of the circle” and had the same effect. 14. I would have rather had a paragraph about universality than a weird one-liner about fundamental groups 15. In sec 4.2 their patch types are all the same. Are we skipping some difficulties because of this? 16. In sec 5, why do the patches not first require that the document contains the strings they care about? I guess that isn’t necessary. 17. Why no homotopy that ! s<>t@i = s<>t@i or that <> is symmetric? Maybe it’s not used. But it feels like the authors are admitting a more complex universal cover than they intend from the semantics they give by doing that. 18. I’m left somewhat wondering what the point is. I would say that the motto of the category theory paper which I haven’t read but which pijul is somewhat related to would be “patches form a category and merges are push outs. You can use category theory to extend the category of patches into one where all push outs exist.” For this paper I guess it’s something like “homotopy type theory gives you some tools for working with groupoids. Here it is applied to patches.” But otherwise I’m not really sure what the relevance is to the implementation or correctness of a dvcs is. They don’t really provide a tool to show that your pseudocommutation function does what it’s supposed to do and so you don’t know that your merges work either. I guess if you could prove that your merges are push outs, does that imply the pseudocommutation is correct? With the category theory paper it at least gives you “correct” merges and a good idea for how to think about patches.

otabdeveloper4 7y ago

"v2 major rewrite, to make the code clean and stuff" is where dumb projects go to die. (There's even a scientific name for this phenomenon.)

rstarast 7y ago

The combination of > (2) thinking about the future and sustainability of the project, including its funding. and the rewrite apparently not happening in the open casts some doubt as to whether the project will remain fully open source.

Freak_NL 7y ago
> […] the rewrite apparently not happening in the open […] That's a major red flag for a FOSS DVCS that aims to exist as a valid alternative for existing tools like git. Fine for a hobby project, portfolio project, or experiment of course.
pmeunier 7y ago
> the rewrite apparently not happening in the open I'm the author of the rewrite. It will almost certainly be open source when it's done, but it is not open right now, because: - the license of the current version has not been properly observed by other projects in the past. - this project keeps getting bashed for "corrupting repositories" and "changing formats constantly", even though it is announced as experimental everywhere (also, some corruption claims have been wrong in the past, and we have released converters every time the formats have changed). Therefore, allowing people to test the new version as it is being debugged would probably not improve this situation.
- rstarast 7y ago
  Thank you, that's good to hear! Your arguments are valid.