[darcs-users] darcs patch: Haddockize literate comments in Darcs.Pa... (and 3 more)

Eric Kow kowey at darcs.net
Mon Apr 6 09:50:45 UTC 2009


Hi Trent,

Haddockize literate comments in Darcs.Patch.Properties.
-------------------------------------------------------
> Trent W. Buck <trentbuck at gmail.com>**20090406090153
>  Ignore-this: 49cb9c7e1e8627da17eada5d5a42281e
>  I converted some LaTeX math to the corresponding Unicode characters,
>  but it seems that Haddock 2.4 is back in the 70s: it converts high-bit
>  bytes to control characters and similar gibberish.  Hopefully cases
>  like this will encourage the Haddock codebase to get up to speed on
>  the whole internationalization scene.

So, I shall defer to you on all matters documentation.

But before I apply this patch, are you sure this is a good idea?

One concern I have is: how are people expected to edit this
documentation easily?

Another thought is: wait, you mean this will break our documentation on
patch properties?  That doesn't sound very good.  Maybe we could bug the
haddock folks to fix this for the hackathon?  Is there another way to go
about this?  Should we resign ourselves to ASCII art?  It seems like
patch theory discussions have to go over email anyway, so darcs patch
theory folks might as well devise a good ASCII notation and stick with
it...

I see from below that this is not (?) part of the darcs manual, but
on the patch-theory.pdf document, so maybe this isn't so scary.

Finally, if you really want me to go ahead with this (and I will),
please submit the changepref in a separate patch (just intuitions
talking as usual).

> changepref test
> set -x && ghc --make Setup; ./Setup configure --user -ftype-witnesses; ./Setup build; ./Setup test tests network
> set -ex && ghc --make Setup; ./Setup configure --user -ftype-witnesses; ./Setup build; ./Setup haddock; ./Setup test tests network

Resolve issue1413: remove duplicate documentation.
--------------------------------------------------
> Trent W. Buck <trentbuck at gmail.com>**20090406092918
>  Ignore-this: caff76e7441d5af26f9400814c9282d2
> ] hunk ./src/Darcs/Patch/Core.lhs 45
>  import Darcs.Patch.Info ( PatchInfo, patchinfo, make_filename )
>  import Darcs.Patch.Patchy ( Patchy )
>  import Darcs.Ordered
> -import Darcs.Patch.Prim ( Prim(..), FromPrim(..), Effect(effect, effectRL) )
> +import Darcs.Patch.Prim ( Prim(..), FromPrim(..), Effect(effect, effectRL), n_fn )
>  #include "impossible.h"
>  
>  data Patch C(x y) where
> hunk ./src/Darcs/Patch/Core.lhs 130
>  
>  patchcontents :: Named p C(x y) -> p C(x y)
>  patchcontents (NamedP _ _ p) = p
> -
> -n_fn :: FilePath -> FilePath
> -n_fn f = "./"++(fn2fp $ norm_path $ fp2fn f)
>  \end{code}
>  
>  The simplest relationship between two patches is that of ``sequential''
> hunk ./src/Darcs/Patch/Prim.lhs 18
>  %  the Free Software Foundation, Inc., 51 Franklin Street, Fifth Floor,
>  %  Boston, MA 02110-1301, USA.
>  
> -
> -\section{Patch relationships}
> -
>  \begin{code}
>  {-# OPTIONS_GHC -cpp -fglasgow-exts #-}
>  {-# LANGUAGE CPP #-}
> hunk ./src/Darcs/Patch/Prim.lhs 173
>  
>  n_fn :: FilePath -> FilePath
>  n_fn f = "./"++(fn2fp $ norm_path $ fp2fn f)
> -\end{code}
> -
> -The simplest relationship between two patches is that of ``sequential''
> -patches, which means that the context of the second patch (the one on the
> -left) consists of the first patch (on the right) plus the context of the
> -first patch.  The composition of two patches (which is also a patch) refers
> -to the patch which is formed by first applying one and then the other.  The
> -composition of two patches, $P_1$ and $P_2$ is represented as $P_2P_1$,
> -where $P_1$ is to be applied first, then $P_2$\footnote{This notation is
> -inspired by the notation of matrix multiplication or the application of
> -operators upon a Hilbert space.  In the algebra of patches, there is
> -multiplication (i.e.\ composition), which is associative but not
> -commutative, but no addition or subtraction.}
>  
> hunk ./src/Darcs/Patch/Prim.lhs 174
> -There is one other very useful relationship that two patches can have,
> -which is to be parallel patches, which means that the two patches have an
> -identical context (i.e.\ their representation applies to identical trees).
> -This is represented by $P_1\parallel P_2$.  Of course, two patches may also
> -have no simple relationship to one another.  In that case, if you want to
> -do something with them, you'll have to manipulate them with respect to
> -other patches until they are either in sequence or in parallel.
> -
> -The most fundamental and simple property of patches is that they must be
> -invertible.  The inverse of a patch is described by: $P^{ -1}$.  In the
> -darcs implementation, the inverse is required to be computable from
> -knowledge of the patch only, without knowledge of its context, but that
> -(although convenient) is not required by the theory of patches.
> -\begin{dfn}
> -The inverse of patch $P$ is $P^{ -1}$, which is the ``simplest'' patch for
> -which the composition \( P^{ -1} P \) makes no changes to the tree.
> -\end{dfn}
> -Using this definition, it is trivial to prove the following theorem
> -relating to the inverse of a composition of two patches.
> -\begin{thm} The inverse of the composition of two patches is
> -\[ (P_2 P_1)^{ -1} = P_1^{ -1} P_2^{ -1}. \]
> -\end{thm}
> -Moreover, it is possible to show that the right inverse of a patch is equal
> -to its left inverse.  In this respect, patches continue to be analogous to
> -square matrices, and indeed the proofs relating to these properties of the
> -inverse are entirely analogous to the proofs in the case of matrix
> -multiplication.  The compositions proofs can also readily be extended to
> -the composition of more than two patches.
> -\begin{code}
>  instance Invert Prim where
>      invert Identity = Identity
>      invert (FP f RmFile)  = FP f AddFile
> hunk ./src/Darcs/Patch/Prim.lhs 403
>  showSplit x ps = blueText "("
>              $$ vcat (mapFL (showPrim x) ps)
>              $$ blueText ")"
> -\end{code}
>  
> hunk ./src/Darcs/Patch/Prim.lhs 404
> -
> -\section{Commuting patches}
> -
> -\subsection{Composite patches}
> -
> -Composite patches are made up of a series of patches intended to be applied
> -sequentially.  They are represented by a list of patches, with the first
> -patch in the list being applied first.
> -\begin{code}
>  commute_split :: CommuteFunction
>  commute_split (Split patches :< patch) =
>      toPerhaps $ cs (patches :< patch) >>= sc
> hunk ./src/Darcs/Patch/Prim.lhs 545
>                                                  push_coalesce_patch p' r
>                                       Left r -> Left (p' :>: r)
>                                   Nothing -> Left (new:>:ps)
> -\end{code}
> -
> -\newcommand{\commutex}{\longleftrightarrow}
> -\newcommand{\commutes}{\longleftrightarrow}
>  
> hunk ./src/Darcs/Patch/Prim.lhs 546
> -The first way (of only two) to change the context of a patch is by
> -commutation, which is the process of changing the order of two sequential
> -patches.
> -\begin{dfn}
> -The commutation of patches $P_1$ and $P_2$ is represented by
> -\[ P_2 P_1 \commutes {P_1}' {P_2}'. \]
> -Here $P_1'$ is intended to describe the same change as $P_1$, with the
> -only difference being that $P_1'$ is applied after $P_2'$ rather than
> -before $P_2$.
> -\end{dfn}
> -The above definition is obviously rather vague, the reason being that what
> -is the ``same change'' has not been defined, and we simply assume (and
> -hope) that the code's view of what is the ``same change'' will match those
> -of its human users.  The `$\commutes$' operator should be read as something
> -like the $==$ operator in C, indicating that the right hand side performs
> -identical changes to the left hand side, but the two patches are in
> -reversed order.  When read in this manner, it is clear that commutation
> -must be a reversible process, and indeed this means that commutation
> -\emph{can} fail, and must fail in certain cases.  For example, the creation
> -and deletion of the same file cannot be commuted.  When two patches fail to
> -commutex, it is said that the second patch depends on the first, meaning
> -that it must have the first patch in its context (remembering that the
> -context of a patch is a set of patches, which is how we represent a tree).
> -\footnote{The fact that commutation can fail makes a huge difference in the
> -whole patch formalism.  It may be possible to create a formalism in which
> -commutation always succeeds, with the result of what would otherwise be a
> -commutation that fails being something like a virtual particle (which can
> -violate conservation of energy), and it may be that such a formalism would
> -allow strict mathematical proofs (whereas those used in the current
> -formalism are mostly only hand waving ``physicist'' proofs).  However, I'm
> -not sure how you'd deal with a request to delete a file that has not yet
> -been created, for example.  Obviously you'd need to create some kind of
> -antifile, which would annihilate with the file when that file finally got
> -created, but I'm not entirely sure how I'd go about doing this.
> -$\ddot\frown$ So I'm sticking with my hand waving formalism.}
> -
> -%I should add that one using the inversion relationship of sequential
> -%patches, one can avoid having to provide redundant definitions of
> -%commutation.
> -
> -% There is another interesting property which is that a commutex's results
> -% can't be affected by commuting another thingamabopper.
> -
> -\begin{code}
>  is_in_directory :: FileName -> FileName -> Bool
>  is_in_directory d f = iid (fn2fp d) (fn2fp f)
>      where iid (cd:cds) (cf:cfs)
> hunk ./src/Darcs/Patch/Prim.lhs 695
>       ("commute_filepatches", clever_commute commute_filepatches),
>       ("commutex", toPerhaps . commutex)
>      ]
> -\end{code}
> -
> -\paragraph{Merge}
> -\newcommand{\merge}{\Longrightarrow}
> -The second way one can change the context of a patch is by a {\bf merge}
> -operation.  A merge is an operation that takes two parallel patches and
> -gives a pair of sequential patches.  The merge operation is represented by
> -the arrow ``\( \merge \)''.
> -\begin{dfn}\label{merge_dfn}
> -The result of a merge of two patches, $P_1$ and $P_2$ is one of two patches,
> -$P_1'$ and $P_2'$, which satisfy the relationship:
> -\[  P_2 \parallel P_1 \merge {P_2}' P_1 \commutex {P_1}' P_2. \]
> -\end{dfn}
> -Note that the sequential patches resulting from a merge are \emph{required}
> -to commutex.  This is an important consideration, as without it most of the
> -manipulations we would like to perform would not be possible.  The other
> -important fact is that a merge \emph{cannot fail}.  Naively, those two
> -requirements seem contradictory.  In reality, what it means is that the
> -result of a merge may be a patch which is much more complex than any we
> -have yet considered\footnote{Alas, I don't know how to prove that the two
> -constraints even \emph{can} be satisfied.  The best I have been able to do
> -is to believe that they can be satisfied, and to be unable to find an case
> -in which my implementation fails to satisfy them.  These two requirements
> -are the foundation of the entire theory of patches (have you been counting
> -how many foundations it has?).}.
> -
> -\subsection{How merges are actually performed}
> -
> -The constraint that any two compatible patches (patches which can
> -successfully be applied to the same tree) can be merged is actually quite
> -difficult to apply.  The above merge constraints also imply that the result
> -of a series of merges must be independent of the order of the merges.  So
> -I'm putting a whole section here for the interested to see what algorithms
> -I use to actually perform the merges (as this is pretty close to being the
> -most difficult part of the code).
> -
> -The first case is that in which the two merges don't actually conflict, but
> -don't trivially merge either (e.g.\ hunk patches on the same file, where the
> -line number has to be shifted as they are merged).  This kind of merge can
> -actually be very elegantly dealt with using only commutation and inversion.
> -
> -There is a handy little theorem which is immensely useful when trying to
> -merge two patches.
> -\begin{thm}\label{merge_thm}
> -$ P_2' P_1 \commutex P_1' P_2 $ if and only if $ P_1'^{ -1}
> -P_2' \commutex P_2 P_1^{ -1} $, provided both commutations succeed.  If
> -either commutex fails, this theorem does not apply.
> -\end{thm}
> -This can easily be proven by multiplying both sides of the first
> -commutation by $P_1'^{ -1}$ on the left, and by $P_1^{ -1}$ on the right.
> -
> -\begin{code}
>  
>  elegant_merge :: (Prim :\/: Prim) C(x y)
>                -> Maybe ((Prim :/\: Prim) C(x y))

Include literate docs from Darcs.Patch.Prim in the user manual.
---------------------------------------------------------------
> Trent W. Buck <trentbuck at gmail.com>**20090406092939
>  Ignore-this: cf2f452e3519839ada2276697f0f08d8
> ] hunk ./src/Darcs/Patch.lhs 148
>  
>  \input{Darcs/Patch/Apply.lhs}
>  \input{Darcs/Patch/Core.lhs}
> +\input{Darcs/Patch/Prim.lhs}
>  \input{Darcs/Patch/Commute.lhs}
>  \input{Darcs/Patch/Show.lhs}

I'll apply this one now, thanks!  

Remove autoconf references to patch_theory.pdf, which is subsumed by haddock.
-----------------------------------------------------------------------------
Waiting on your comments to the above concerns.

-- 
Eric Kow <http://www.nltg.brighton.ac.uk/home/Eric.Kow>
PGP Key ID: 08AC04F9
-------------- next part --------------
A non-text attachment was scrubbed...
Name: not available
Type: application/pgp-signature
Size: 194 bytes
Desc: not available
URL: <http://lists.osuosl.org/pipermail/darcs-users/attachments/20090406/8ff2b054/attachment.pgp>


More information about the darcs-users mailing list