[darcs-devel] camp paper location

[Ben Franksen]

Am 12.08.19 um 01:54 schrieb Ganesh Sittampalam:
> I've recently started looking (again) at the "Camp Patch Theory" paper
> in detail so I can properly review the V3 commute/merge implementations.
> 
> The first question is what exactly to look at :-)
> 
> There's a version of the paper dated 27/1/2012 here:
> 
> https://archives.haskell.org/projects.haskell.org/camp/files/theory.pdf

I think this is the version which I have printed some time ago and that
I still ocassionally refer to. Like you I had trouble building the paper
from the repo.

> However the darcs repository for the paper, here, has some more recent
> patches:
> 
> https://archives.haskell.org/code.haskell.org/camp/devel/paper/
> 
> I had some trouble getting that to build. I eventually succeeded, with
> some tweaks (some of which date from my last look at the paper 5 years
> ago!).

Can we make a clone of the repo e.g. on hub.darcs.net and apply your
patches there? Oh, I see below you have already made a clone.

> Unfortunately some of the more recent changes cause a "! Dimension too
> large." error from LaTeX, so start from the 'builds' tag:
> 
> http://urchin.earth.li/darcs/ganesh/camp-paper/
> 
> I also only got the paper building, not the proofs. 

I have never succeeded in understanding Coq well enough to be able to
read the formal proofs. I find them extremely verbose and inelegant and
wouldn't mind if we loose them.

The informal proofs in the text are a different matter. The most
interesting one shows how "consistency of failure" for commutation can
be generalised from a triple of patches to arbitrary sequences. Quite
elegant and a nice complement to your proof of permutivity from
3-permutivity (of which I have a very concise version now, based on
closed paths in the Caley graph of S_n).

Since you built the paper, do you know if there is a way to build it
without the formal proofs embedded to save paper when printing?

> Use "make doc".
> 
> There's a generated PDF here:
> 
> http://urchin.earth.li/~ganesh/temp/theory.pdf
> 
> All this is to say that we should get the "where to get it" on a more
> solid footing for us. That might be simply by saying "let's use this
> frozen PDF", or by being clear what repository to use. I don't know if
> we want to put effort into trying to develop the paper further.

I wouldn't want to do that. Just copy a current pdf somewhere, ideally
on our wiki.

The reason I am not interested in working on the paper is that the way
the theory is presented there is on the one hand too low-level (probably
motivated by the desire for and end-to-end proof of all properties), and
on the other hand missing practical foundation (states and patch
application aren't mentioned at all).

A category theoretic formulation is more elegant and corresponds more
closely to the implementation with witness types. In particular, I think
that any presentation of patch theory should start with a precise
account of patch application as a functor from the groupoid of patch
sequences to that of partial bijections on states.

I do like the pictures in the paper. They are invaluable to understand
the more complicated things like how catches are commuted or merged.

> Also, for the references in the source code, it might be better to refer
> to definitions etc by their names as well as their numbers, as the
> latter can change. E.g. refer to "definition 10.1 (contexted-patch)"
> rather than just "definition 10.1". We should also make it clear in the
> source what paper these definitions actually refer to.

Right on all accounts.

Cheers
Ben