This thread is a continuation of the following threads: - Verifying that @<file> will work http://groups.google.com/group/leo-editor/browse_thread/thread/400f28ff3a02958d
- Will just one kind of @file node suffice http://groups.google.com/group/leo-editor/browse_thread/thread/33a3576c904d2a60 In this thread, I will attempt to state and prove one or more @shadow theorems, which generally state that any group of people can use @shadow files in cooperative (bzr) environments. The goal is to state the theorems precisely, and prove them rigorously. I haven't done either yet. This thread will document my efforts, so that everyone can see the thought process involved. This is important, because the goal is to achieve consensus that using @shadow instead of @thin will work in bzr repositories. In my mind, stating and proving this theorem is the most important unfinished task for Leo. If this can indeed be done, the way will be clear to use @shadow for *all* kinds of files. Instead of @asis, @thin, @auto, @shadow, etc, everyone will be able to used a single kind of tree. It might be called @shadow; it might be called something else, but whatever it is called it will be one of the biggest collapses of complexity in Leo's long history. Preliminaries I said earlier, we want to show that any group of people can use @shadow files in bzr repositories. We must first clarify what this means. As a matter of terminology, suppose Alice is a programmer who changes a public file A. Alice may or may not be a Leo user. If she is, Leo will update the private file A' when Alice changes A. If Alice is not a Leo user, Alice will not cause the file A' to change. After changing A (and possibly A'), Alice will push A (and possibly A') to the bzr repository. If Alice uses Leo, she is allowed to push A and A' in either order. In particular, we are assuming that Alice is *not* required to push A and A' at the same time. There may be an arbitrary delay between when Alice pushes A and A'. If Alice does not Leo, then she will only ever push A. Let Bob be a programmer who will pull what Alice pushes. As stated above, Alice need not push A and A' at the same time, and indeed Alice may never push A'. The question is, does it matter in which order Bob pulls A and A' ? There are four cases to consider: Case 1: Alice doesn't use Leo, and pushes only A. Bob pulls A. Case 2: Alice pushes A. Bob pulls A. Alice pushes A'. Bob pulls A'. Case 3: Alice pushes A'. Bob pulls A'. Alice pushes A. Bob pulls A. Case 4: Alice pushes both A and A' before Bob pulls either. Bob then pulls A and A'. So the question is, does Bob get "essentially" the same result in each case. I am leaving the word "essentially" a bit vague on purpose. I'll have to fix this later, but I don't want to try yet because it depends on some tricky details. So this is the task at hand. I'll work on this theorem in replies to this thread. Edward P.S. The above is not a complete analysis. There is a potentially troubling complication. Suppose Carol is another programmer who is pushing changes to A, and possibly to A'. I stated above that there can be arbitrarily long between the time that Alice commits A and the time Alice commits A'. This means that Carol could commit other versions of A and A' after Alice commits the first half of the pair (A,A') and before Alice commits the second half of the pair (A,A'). Similar remarks apply to Doug, Eric, Fred, etc. I am going to ignore this complexity at first. I hope the the proof of the simpler theorem will provide insights or tools that will shed light on the more complex general case. **Important**: this issue can not be a show stopper. If necessary, we could force bzr to commit A and A' simultaneously, thereby reducing all commit/pull combinations to either Case 1 or Case 4. P.P.S. Instead of a rigorous proof, we could just run some experiments to see if there are problems in practice. This might be a valid approach, but I would like to see how far analysis can take us. Conversely, it may turn out that the work of doing the proof might suggest code-level constraints or improvements that would clarify the proof or improve how Leo actually works. EKR --~--~---------~--~----~------------~-------~--~----~ You received this message because you are subscribed to the Google Groups "leo-editor" group. To post to this group, send email to [email protected] To unsubscribe from this group, send email to [email protected] For more options, visit this group at http://groups.google.com/group/leo-editor?hl=en -~----------~----~----~----~------~----~------~--~---
