[darcs-users] Getting ready to sprint, camp team

[Florent Becker]

Ian Lynagh <igloo at earth.li> writes:

> On Wed, Apr 15, 2009 at 03:30:02PM +0200, Florent Becker wrote:
>> 
>> A/ camp mailing-list versus darcs-users mailing list.
>> 
>> I discovered yesterday the existence of camp's own mailing list, which
>>  sees very few usage. darcs-user's traffic is also not that big, and given
>>  that it would be nice for everyone here to know in what shape the future
>> darcs-3 is. I propose to use darcs-user for both camp and darcs for 
>> normal discussion, and respectively the camp and darcs-devel lists for
>> automated traffic. Is it ok with everybody?
>
> Some people have been saying that d-u is too busy for them, and I think
> that many people on d-u won't be interested in the camp talk, so I'd say
> it's best on the camp list. I'll happily reply here if that's what other
> people want, though.
>
Ok, i'll continue the discussion here. If it gets too noisy for somebody, just
tell so. If somebody is intrested in knowing what happens to camp, please
let us know too.

>> C/ camp-paper and camp-coq.
>> 
>> This situation, with 4 different sources of "truth" about camp must be resolved,
>
> We should certainly try to merge the coq's. Actually formally linking
> the Haskell to the coq seems infeasible in the short term.
>
Yes, but we should be careful to keep the coq and paper theory faithful to the code.

>> 3/ sensible sequences versus states
>> 
>> camp-coq does not seem to care about that issue (ie, at the moment, it
>> does not encode this constraint).
>
> Yes; I think this is the most "obviously correct" bit, so I'm leaving it
> until last.
>
>> My view on this point is:
>> -camp-paper's axiom are incomplete. We need at least one more axioms
>> that says that if sp and sq are sensible sequences, then so is spp^q.
>> Without this axiom, nothing says that p^ undoes p, we only know its
>> behaviour with respect to commutation. 
>
> Yes. (Things like overlooking this axiom is the reason I want a coq
> proof: It's too easy to miss a detail when making human proofs. More
> eyes will spot more of the details, as you have done here, but nothing
> beats a machine proof).
>
This i actually got from thinking about the machine proof.

>> -camp-code's (and dic's) stateful patches (where states are an
>> _abstract_ type) are much easier to work with in coq (and in code) 
>> than a bunch of axioms, as the states prevent most mistakes.
>> Note that using states makes proving that every sequence you produce is
>> good automatic, whereas you need a proof with each operation when
>> using sensibility.
>
> Yes, I don't object to using states. The only reason I haven't is to
> keep it simpler for now.
>
Ok, my experience is that when doing the actual (coq or manual )proofs,
states are more a help than anhindrance. So we should go for them.

>> 4/ Unnamed marked sequences
>> 
>> before introducing names (they don't exist yet in dic), dic relies on a
>> concept which is not present in camp-paper, nor in camp-coq.
>> 
>> That concept is that of marked sequences (shuffle_mark_[1,2] in
>> dic). The idea is that if s (with p marked) can be shuffled into t (with q marked),
>> then when shuffling s into t, p "lands" on q. (There is also a version with
>> two marks). Additionally, one will need a lossy version, with
>> s (with p marked) can be turned into t (with q marked) if by shuffling
>> patches in s, adding and removing patches, p "lands" on q.
>
> This feels like an ugly kludge to me. The "obvious" human proofs for
> some of the lemmas required a similar kludge, but I managed to find a
> way to do the proofs that didn't need it in the end. I hope we can avoid
> it with machine proofs too.
>
What lemmas and what proofs are concerned by this? How did you get out of
that situation? I want to know, because i don't find it is a kludge, and i don't see
any other way to _completely_ do some proofs.

>> 5/ Zigzag sequences (and their absence)
>> 
>> This is a point that's absent in all sources alike, but which we will need
>> to take into account somehow. We can sum it up by saying that the
>> subsequence pp^p is evil, and should probably not appear in a repository 
>
> Unfortunately, you can trace patch sequences like this within a catch
> repo. If you have
>
>     A + B + AC
>
> then you get
>
> A             [A^, :B]                        [, A:C]
> (the patch A) (The patch B, conflicts with A) (The patch C, with context A)
>
> So to get the context of C you start at the left, and have A A^ A.
>
I don't think it's a problem: the context of a patch can have a zigzag, but not
the sequence of names of a repo. So not all sequences are straight, but there
are some places where sequences that arise are guaranteed to be straight. Is
that right?
>
>> 6/ names as a function or a component of patches
>> 
>> Second, Ian's proofs that 'c' holds are difficult
>
> We've talked about this OOB, and I think we're agreed that we need to be
> able to do these proofs, because they're simpler versions of the catch
> proofs that we're going to have to do.
>
> I still think that my way, i.e. constructing named patches from unnamed
> patches and names, is the best way. But even if I didn't, I think that
> doing these simple proofs will help me understand how best to write the
> big proofs, so I plan to continue with this.

Ok, i agree with the training bit, even though i'm not sure those proofs are
actually much simpler than the catch proofs, since they require setoid
manipulations for the namesets. I think the difference between your approach
and mine is not a deep difference. It's only a matter of pragmatism and of
cutting code into module. My idea is to separate the proofs that named patches
behave like unnamed patches when you forget the names from the actual
use of named patches. If, as I think you'll have the unpleasant surprise to
discover, these "simple" proofs turn out to be non-trivial or problematic, then
my approach allows to leave them for later. I'm inclined to thinking that catches
will be not that much more to build, since they are only _sequences_ of names
there, no fsets. So the coq difficulties for catches will correspond to real
difficulties, unlike for named patches. I'm only advocating your "obviously
correct bits" approach.
>
>> 7/ Where to introduce names?
>> 
>
> I think you may have missed the idea behind patch universes.
>
I probably did: i don't even know what a patch universe is (i mean
what it bourbakily is).

> With unnamed patches we have some axioms, say A1 and A2.
> With named patches we prove equivalent lemmas N1, N2.
> With catches we prove equivalent lemmas C1, C2.
>
> Then the patch universe says: Given a patch type P, and lemmas L1 and L2
> on P, there is a patch universe in which L3, L4, L5 are true.
ok
>
> Roughly speaking, L1 and L2 are how triples of patches are related by
> commutation, and L3+ are things like "patches in a sequence (or, indeed,
> theentire universe) have a minimal context".
So why not make L3 be "patches have a minimal context?" That's what I'm
advocating (actually something a bit weaker: that they have a common
straight context).
>
> So the point of patch universes is that we don't have to prove that
> named patches /and/ catches have minimal context, we only have to prove
> that patch-like things have minimal context.
>
Note that by N1 and N2, and C1 and C2, this is the case whichever
formalisation for L3+ you take. So this argument is moot, since
named patches and catches are /just a particular case of unnamed
patches/.
>
> As for "operations", you can represent them as relations, in the same
> way that we already represent the commute operation as a relation.
>
Won't make things easier either way.

>> My proposal is to end the madness. I propose to add an axiom that says
>> that we can decide whether two patches are related, and draw the consequences.
>
> I don't want to add axioms about named patches. Apart from anything
> else, if you need to make it an axiom for named patches then I can't see
> how you're going to do it for catches. Or to phrase it differently: If
> you can prove it for catches, I'm sure you could prove it for named
> patches, so it has no business being an axiom.

There's a fundamental misunderstanding here: i'm not adding as an axiom
something you can prove. I'm advocating transforming one of your axioms.

You had an axiom that says that record produces fresh names. It wasn't
really a satisfying formalisation. (and it is certainly not something I want
to do in coq. If you can find me an example of a theory in coq with a use
of name freshness, i'll reconsider that idea).

Then you turned it into the patch universes construction. I'm not much more
convinced by this construction, since i haven't even seen a paper definition
of patch universes.

So what I propose is to look at why we need names and name freshness in
the first place, and see if we can get rid of freshness. Again, it's just
separation of concerns and modularity for the proofs.

So, what do we use name for? The only thing we do with them is to compare
them for equality. (We don't order them, or concatenate them, for instance).
So in fact what we're manipulating is the equivalence name(p) = name(q).

What is this equivalence? It's the reflexive symmetric transitive closure of
the relation (p,p') -> exists (q,q') <<p,q>> <~> <<q',p'>>. So in fact, all
we are using name for is to have a decision procedure for this equivalence.
(That's not quite exact: it also gives an explicit type for the classes of that
equivalence, but in paper terms, that's not important). So what i propose
is to make that decision procedure the axiom¹, and prove that using stored
names works for that procedure somewhere else. Modularity again.

So what I propose is to have a function name as a parameter, plus an axiom
that says that name(p) = name(q) <-> p ~ q for that equivalence (i use a name
function in order to be able to manipulate equivalence classes explicitly. There
might be a better way). Then in another module, we prove that names given at
patch creation and preserves through commutation fit the bill. This is another
"obvious bit" where the coq proof is going to be unnecessarily hard, because
we are going to have to model record, the only effectful operation. There we
might have to use patch universes, but i want to keep their use to one module,
and do that module last (I'd even advocate doing without it, since we _can't_ and
_won't_ have correct name generation in a fully distributed setting).

I hope to have convinced you that i'm not adding an axiom to named patches, but
rather advocating the use of "identified" or "trackable" patches for all the theoretical
construction, with the final obvious note that giving a name to each patch at record
and having it kept at each commutation gives us patch trackability. It's just a matter
of separationg high-level concerns from low-level concerns.

Hope this helps,

Florent

¹: if you doubt it really removes one axiom, the one it removes is the infinity
of the set of names.