[darcs-devel] camp paper location

[Ganesh Sittampalam]

On 13/08/2019 06:40, Ben Franksen wrote:

> Am 12.08.19 um 01:54 schrieb Ganesh Sittampalam:

>> 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.

Yeah. I'd put it on hub.darcs.net if we were going to maintain something
long-term, but since we're not I won't.

> 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).

Cool. From what I remember, the group presentation of S_n also nearly
offers a concise way of expressing the proof, except that's it's not
obvious how to extend it to cope with failure.

> 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?

I just spent a little while trying to automatically disable all the
'coqdoccode' sections, including using the 'comment' package, but no
luck - I get LaTeX errors that are incomprehensible to me. It's a
horribly uncompositional language :-(

>> 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.

OK. Shall we just stick with the one Ian published, then?

Ganesh