David Roundy wrote: > On Fri, Mar 09, 2007 at 07:27:09PM +0100, Juliusz Chroboczek wrote: >>> 1. The conflict bug. >> This is the big one. Nobody knows how to fix it (or they're not saying). > > I believe we do know how to solve it, it's just that it'll be a lot of > work. Jason is planning on starting work on that in the spring--but of > course he'll start out by working on a simulated version. We talked about > this after the Haskell workshop in the fall, and I'm quite confident that > we know what the solution looks like, it's just a question of coding it up > and figuring how to design a repository format that'll work with it. > > [...] There will be lots of book keeping, but the math > needed to determine the state of a repository is actually very simple, so > the main issues should be technical ones (doing so efficiently, how to > store it on disk, how to determine dependencies interactively when > prompting for changes, etc).
Disclaimer: I'm an uninformed bystander. But I'm in awe of the miracle that darcs exists without a really rigorous Theory Of Patches. Alas, the miracle dissolves rather quickly when noting that The Conflict Bug haunts darcs for some year(s) now. This gives rise to the following prophecy: darcs will be haunted until it is crystal clear what the semantics of patches are. Crystal clear. Why must the prophecy be true? Well, here's the _proof_: once the issue is solved, the darcs source code is a fully worked out Theory Of Patches. QED :) Please, do not underestimate this, developing a crystal clear Theory Of Patches is hard. It is far form being a "technical issue" that only needs "coding it up". For instance, efficiency is an integral part: it's quite imaginable that the Theory is too general and turns out to be NP-hard. What if it's interactivity that makes it NP-hard? I guess E.W. Dijsktra and R. Bird would give the same advice: understand the problem, find the proofs. Equational reasoning will generate your implementation for free. Regards, apfelmus PS: Personally, I always wondered whether one could use a bit category theory for a Theory Of Patches. Patches f : A -> B are arrows between repositories A and B. Actually, to be able to move them around, they should be a family of arrows (= a functor) like F : forall a . A a -> B a, I don't know. The product AxB of two repositories is the last common repo they developed from. The coproduct A+B is a canonical merge of A and B. Maybe it's not a merge but it's the disjoint sum with all conflicts yet unresolved. Then, a conflict resolving patch would have a family member f : A+B -> C. Can such single arrows be extended to functors by some universal property? I mean, that's the key point: given a change f : A -> B between very concrete repos, find a more general one. _______________________________________________ darcs-users mailing list [email protected] http://lists.osuosl.org/mailman/listinfo/darcs-users
