Created on 20230618.16:26:27 by bfrk, last changed 20230729.15:48:24 by bfrk.
See mailing list archives
for discussion on individual patches.
msg23331 (view) 
Author: bfrk 
Date: 20230618.16:26:26 

Not selfaccepting even though these are only comments; it would be cool if
someone doublechecks that the proofs are correct.
1 patch for repository http://darcs.net/screened:
patch cd1d4ea4c5589c6f47d83b96e411ec51c1924d1f
Author: Ben Franksen <ben.franksen@online.de>
Date: Fri Jun 9 00:07:35 CEST 2023
* add proofs of impossibility for all error cases in V3.Core
Attachments

msg23606 (view) 
Author: ganesh 
Date: 20230716.22:04:07 

Reviewing these proofs slowly...
> (2) If v depends on u and p conflicts with u then it also conflicts
> with v.
I actually have trouble understanding what this means: my intuitive
definition of "p conflicts with u" is that `merge (p :\/: u) == Nothing`.
But in this scenario we can't even construct `p :\/: v`.
> merge (lhs@(Conflictor com_r x cp) :\/: rhs@(Conflictor com_s y cq)) =
> case findCommonFL com_r com_s of
> Fork _ r s >
> case cleanMerge (r :\/: s) of
> Nothing >
>  Proof that this is impossible:
I believe this one.
>  similar to above case: a prim and a conflictor that conflicts with the prim
>  but also conflicts with other patches
>  [p] :> [p^ s, {s^:p} U Y, cq] <> [s, Y, cq] :> [, {cq}, s^:p]
> commuteConflicting (Prim p :> Conflictor s y cq)
>  ident p `S.member` S.map ctxId y =
> case fastRemoveFL (invert p) s of
> Nothing >
>  Proof that this is impossible:
> 
>  The case assumption (that p is in conflict with q) together
>  with the fact that the rhs is obviously the first patch that
>  conflicts with the lhs, imply that p^ is contained in s. It
>  remains to be shown that p^ does not depend on any prim contained
>  in s. Suppose there were such a prim, then p would be in conflict
>  with it, which means p would have to be a conflictor. QED
FWIW I found this slightly harder to read because of a notational inconsistency between
the code and the comment just above the code: in the comment p^ is not part of s,
but in the code p^ is part of s (as we have to remove it).
Coming back to the proof and expanding out the final bits of the argument a bit:
"It remains to be shown that p^ does not depend on any prim r^ contained in s.
Suppose there were such a prim, then p and r^ would be in conflict, as r^p^
wouldn't commute."
However r^ is the inverse of a prim r somewhere in the history of the repo, whereas
p is a prim directly in the history of the repo, so I can't quite get from the
statement that they are in conflict to "p would have to be a conflictor".
I can convince myself with the following slightly stronger statement about
invariants:
If we take the effect of a conflictor, then let rs = the inverse of that effect, i.e. the
patches the conflictor reverts. If we let cs = the the unconflicted prims in the context
of that conflictor, then we can commute cs so that rs is a suffix of it.
Given that statement, the appearance of r^p^ in s with p^ depending on r^ implies
that the unconflicted prims in the context contain pr where r depends on p. But then
the commute we are trying to do is impossible because r would be stuck inbetween p and
the conflictor.

msg23607 (view) 
Author: ganesh 
Date: 20230716.22:41:51 

>  if we have two conflictors where the rhs conflicts /only/ with the lhs,
>  the latter becomes a prim patch
>  [r, X, cp] [, {cp}, r^:q] <> [q] [q^r, {r^:q} U X, cp]
> commuteConflicting (lhs@(Conflictor r x cp) :> rhs@(Conflictor NilFL y cq))
>  y == S.singleton cp =
> case ctxView (ctxAddFL r cq) of
> Sealed (NilFL :> q') > [...]
> Sealed (c' :> _) >
>  Proof that this is impossible:
> 
>  First, it must be true that commutePastFL r cq = Just cq'. For if
>  not, then there would be a conflict between the rhs and one of the
>  prims that the lhs reverts, in contradiction to our case
>  assumption that the rhs conflicts only with the lhs.
> 
>  Second, suppose that cq' has residual nonempty context. That means
>  there is a patch x in the history that the rhs depends on, and
>  which is in conflict with at least one other patch y in our
>  history (the history being the patches that precede the lhs);
>  because otherwise cq' appended to the history would be a sequence
>  that contains x twice without an intermediate revert. But then the
>  rhs would also have to conflict with the patch x, again in
>  contradiction to our case assumption. QED
I roughly get the argument here, but I'm having trouble following it precisely.
I think it'd help if you used the same functions in the proof as in the logic:
how does commutePastFL relate to ctxAddFL? And is that definitely what you meant,
don't we actually expect the inversecancellation logic of ctxAdd to kick in?
Also is it meaningful to talk both about the rhs depending on x and being in
conflict with it? (this partly goes back to my earlier comment about
what being in conflict really means)

msg23616 (view) 
Author: bfrk 
Date: 20230718.20:34:03 

>> (2) If v depends on u and p conflicts with u then it also conflicts
>> with v.
>
> I actually have trouble understanding what this means: my intuitive
> definition of "p conflicts with u" is that `merge (p :\/: u) == Nothing`.
More precisely it means that `cleanMerge (p :\/: u) == Nothing`.
> But in this scenario we can't even construct `p :\/: v`.
True. In this formulation I (sloppily) identify nominally equal patches. Formally, we can
merge (p :\/: u) = u' :/\: p'
and then
cleanMerge (p' :\/: v)
should fail if
cleanMerge (p :\/: u)
fails. The sloppy formulation can be excused on the ground that commutation (or merge)
never changes whether patches commute, which is the identity law we discussed lately.
> FWIW I found this slightly harder to read because of a notational inconsistency between
> the code and the comment just above the code: in the comment p^ is not part of s,
> but in the code p^ is part of s (as we have to remove it).
Ah, yes. In the proofs I used the notation from the code, not the older comments above,
which I had more or less copied from the paper (modulo some renamings) back when I wrote
this code. Perhaps I should delete these older "pseudoformal" comments, the more so since
their notation is also borrowed from the paper and that notation is nowhere explained in
the module.
> Coming back to the proof and expanding out the final bits of the argument a bit:
>
> "It remains to be shown that p^ does not depend on any prim r^ contained in s.
> Suppose there were such a prim, then p and r^ would be in conflict, as r^p^
> wouldn't commute."
I like your formulation that gives an explicit name to the supposedly existing prim in s.
My formulation is unclear because it doesn't clearly distinguish between r and r^.
> However r^ is the inverse of a prim r somewhere in the history of the repo, whereas
> p is a prim directly in the history of the repo, so I can't quite get from the
> statement that they are in conflict to "p would have to be a conflictor".
The fact that the lhs is a Prim (capital case i.e. not a Conflictor) means that p cannot be
in conflict with any patch preceding it. I think that's plainly obvious, or isn't it?

msg23617 (view) 
Author: bfrk 
Date: 20230718.21:34:46 

>> commuteConflicting (lhs@(Conflictor r x cp) :> rhs@(Conflictor NilFL y cq))
>>  y == S.singleton cp =
>> case ctxView (ctxAddFL r cq) of
>> Sealed (NilFL :> q') > [...]
>> Sealed (c' :> _) >
>>  Proof that this is impossible:
>> 
>>  First, it must be true that commutePastFL r cq = Just cq'. For if
>>  not, then there would be a conflict between the rhs and one of the
>>  prims that the lhs reverts, in contradiction to our case
>>  assumption that the rhs conflicts only with the lhs.
>> 
>>  Second, suppose that cq' has residual nonempty context. That means
>>  there is a patch x in the history that the rhs depends on, and
>>  which is in conflict with at least one other patch y in our
>>  history (the history being the patches that precede the lhs);
>>  because otherwise cq' appended to the history would be a sequence
>>  that contains x twice without an intermediate revert. But then the
>>  rhs would also have to conflict with the patch x, again in
>>  contradiction to our case assumption. QED
>
> I roughly get the argument here, but I'm having trouble following it precisely.
This is the most difficult proof and it's not easy to follow.
> I think it'd help if you used the same functions in the proof as in the logic:
> how does commutePastFL relate to ctxAddFL?
I used a fact about Contexted that is not explicitly stated anywhere, but obvious from the
definition of ctxAdd, namely
(*) commutePast r cq = Just cq' => ctxAdd r cq = cq'
We want to prove that the context in (ctxAddFL r cq) is empty. What I show is that
(commutePast r cq) succeeds and its result has empty context. Together with (*) this implies
that the context in (ctxAddFL r cq) is empty.
> And is that definitely what you meant,
> don't we actually expect the inversecancellation logic of ctxAdd to kick in?
No; if my argument in the first paragraph of the proof convinces you, then inverses of prims
in r cannot be in the context of cq.
> Also is it meaningful to talk both about the rhs depending on x and being in
> conflict with it? (this partly goes back to my earlier comment about
> what being in conflict really means)
Thanks for pointing that out. Indeed I made two mistakes here. First I reused the variables x
and y for new things, which is bad. Let us use u and v instead. The second mistake was that in
the last sentence I should have said "y" instead of "x".
The point is that something (say, u) can be in the context of cq only if it previously got
reverted by a conflictor. That is, we must have a situation like this:
u ... (conflictor (...u^...) _ (... : v)) ... lhs rhs@(Conflictor _ _ cq@(...u... : q))
Now, u being in the context of q means that q depends on u. So, by our invariant (2), v (which
conflicts with u) must also conflict with q, in contradiction to the case assumption that q
only conflicts with p.

msg23618 (view) 
Author: ganesh 
Date: 20230719.00:24:54 

The problem I have with your definition of "conflict" is that it
is based on some notion of repo patches rather than prim patches.
Granted, all valid implementations should behave in the way you
describe, but it's still quite circular. Plus the distinction
between merge and cleanMerge adds extra complexity.
In addition, the constituent parts of a RepoPatchV3 are all prim
patches, so it's weird to be talking about properties that only
make sense when they are lifted into repo patches.
[mismatch between notation and code]
> Ah, yes. In the proofs I used the notation from the code, not
> the older comments above, which I had more or less copied from
> the paper (modulo some renamings) back when I wrote this code.
> Perhaps I should delete these older "pseudoformal" comments,
> the more so since their notation is also borrowed from the paper
> and that notation is nowhere explained in the module.
I found that reading the comments helped quite a bit even with the
mismatches, so I'd like to keep them.
> > Suppose there were such a prim, then p and r^ would be in
> > conflict, [...]
> > However r^ is the inverse of a prim r somewhere in the
> > history of the repo, whereas p is a prim directly in the
> > history of the repo, so I can't quite get from the
> > statement that they are in conflict to "p would have to
> > be a conflictor".
> The fact that the lhs is a Prim (capital case i.e. not a
> Conflictor) means that p cannot be in conflict with any patch
> preceding it. I think that's plainly obvious, or isn't it?
But r^ isn't even in the repo so can't precede p in the repo.
My alternative argument doesn't talk about conflicts, it actually
talks about dependencies.

msg23620 (view) 
Author: bfrk 
Date: 20230719.11:18:24 

The problem I have with your formulation of the invariant (2) is that it is
a "global" property of all patches in the context of a conflictor i.e. that
they can be reordered in a certain way. That means it is hard to see that we
actually maintain it when constructing new Conflictors, which makes it
useless in practice.
Instead, let me rephrase my invariant (2) to avoid any circularity:
First, generalize the definition(!) of "conflicts with" for (named) prims:
if p conflicts with u, and v depends on u, then we say that p also conflicts
with v. It follows from permutivity that this generalized definition is
commutation invariant and is therefore a property that depends only on the identity of the prims involved.
The invariant now says: if both (Prim u) and (Prim v) are present in the
history of (i.e. the context preceding) the conflictor representing p, then the latter must have a contexted prim (...u... : v') as a member of its "set
of conflicts", where ident v' == indent v.
In other words, the "set of conflicts" in a Conflictor representing p
/indeed/ contains all prims (in Contexted form) that are in its context and
that p conflicts with. Formally: for every RepoPatch Q representing q in the
context of a (Conflictor _ x _) representing p we have
ident q `S.member` S.map ctxId x == "p conflicts with q"
in the generalized sense of "conflicts with" defined above.
It is now easy to systematically check that whenever we construct a new
Conflictor we maintain this invariant.

msg23621 (view) 
Author: ganesh 
Date: 20230719.20:08:15 

I'll keep working through your comments, but if possible when you have a chance
could you turn your changes to the proofs into new draft patch? It'll make
it easier for me to reread the updated argument in its entirety.
> The problem I have with your formulation of the invariant (2) is that it is
> a "global" property of all patches in the context of a conflictor i.e. that
> they can be reordered in a certain way. That means it is hard to see that we
> actually maintain it when constructing new Conflictors, which makes it
> useless in practice.
Here's a rough sketch of what I intuitively had in mind. Requoting the invariant:
> If we take the effect of a conflictor, then let rs = the inverse of that effect,
> i.e. the patches the conflictor reverts. If we let cs = the unconflicted
> prims in the context of that conflictor, then we can commute cs so that rs
> is a suffix of it.
Let's assume that the invariant already holds for all Conflictors in a repo.
Essentially the idea is that whenever we do an operation that might touch cs
or rs for a particular Conflictor, the nature of the changes we make also
guarantee that the "can commute cs so that rs is a suffix" property is maintained.
When we first introduce a Conflictor from nothing, I think it always just
reverts a single prim? That prim is always going to be right before it in the
context so the property is obvious.
Let's suppose we permute the patches in the context of a Conflictor X, i.e.
we might be changing cs. If we just touch Prim patches, the property is maintained
for X because we can always undo do the commutes to get back to the previous cs.
If we touch Conflictors too, I think the logic guarantees that we
don't invert any new prims, just move around where it happens, so cs
should be unchanged.
When we commute conflictor X itself then rs is what might change. I think again
all we are doing is shuffling the prims we already inverted around, and any
shuffling will involve commute on the prims. So we can also undo those
commutes to get back to the previous rs, which is equivalent to commuting cs so
that the new rs is a suffix of it.

msg23623 (view) 
Author: bfrk 
Date: 20230719.22:38:05 

Following up as requested. I haven't screened them yet, so I can still amend
if I made a mistake or something is still unclear.
On a general note, this is not unlike writing a paper: one the one hand you
want to be as precise and clear as possible, on the other hand you have
limits on the length of the text. I think it is important to keep these
proofs inline with the code, so they should be concise and not too much
frought with formal detail. This is clearly a difficult balancing act!
I am using the reformulated invariant (2) in the proofs by tacitly assuming
that the "set of conflicts" really coincides with the set of prims from the
context that (in the generalized sense) conflict with the prim represented
by the Conflictor in question.
Regarding your counterproposal for invariant (2): you have made it clear
that it is not "useless", sorry for claiming that. I still prefer my version
because it more closely corresponds to (and explains) the concept underlying
the "set of conflicts" component of a Conflictor, and (I think) allows for
shorter proofs.
2 patches for repository http://darcs.net/screened:
patch a0fbff5012d0e8cc5402552fa3e384f5b3c8e81d
Author: Ben Franksen <ben.franksen@online.de>
Date: Wed Jul 19 22:48:56 CEST 2023
* RepoPatchV3: improve definition of invariant (2)
patch 47a8e3d7dea1de5da6cb4e75e4b15b7158fa73ff
Author: Ben Franksen <ben.franksen@online.de>
Date: Wed Jul 19 23:41:06 CEST 2023
* RepoPatchV3: reword one of the proofs
Attachments

msg23624 (view) 
Author: bfrk 
Date: 20230721.08:37:50 

One more followup, not yet screened.
1 patch for repository http://darcs.net/screened:
patch 9b5ed0d55de16416f0c86143b8c914481b0dc59f
Author: Ben Franksen <ben.franksen@online.de>
Date: Fri Jul 21 10:29:24 CEST 2023
* RepoPatchV3: fix yet another proof
I talked about "conflicts with" here which is completely wrong, it is purely
about dependency.
Attachments

msg23625 (view) 
Author: bfrk 
Date: 20230721.09:24:15 

One remark about the proof for
commuteConflicting (lhs@(Conflictor r x cp) :> rhs@(Conflictor NilFL y cq))
 y == S.singleton cp =
case ctxView (ctxAddFL r cq) of
Sealed (NilFL :> q') >
Just $ Prim q' :> Conflictor (invert q' :>: r) (cq + x) cp
Sealed (c' :> _) >
 Proof that this is impossible:
It relies on a property about sequences of patches in class Ident:
In any sequence of patches identities must be unique.
Formally:
forall u,v :: p, (u;ps;v) :: Fl p. ident u /= ident v
(Notation: (;) is concatenating, identifying single patches with singleton
sequences)
This is, BTW, also needed in order for the instance Ident (FL p) to make
sense.
Can we prove that from the class laws? Or do we have to add another axiom
here? So far my attempts to prove it failed...

msg23626 (view) 
Author: bfrk 
Date: 20230721.09:35:38 

Ah, forget it: this is only true for "positive patches". If patches
can be inverted (like for named prims), then this is clearly false.
The property we want is actually
forall u,u' :: p, (u;ps;u') :: Fl p. ident u == ident u'
=> ps contains some p with ident p = ident u^
If all patches are not invertible then this implies that patch
identities are unique, but not the other way around.

msg23627 (view) 
Author: bfrk 
Date: 20230721.16:13:39 

Coming back to invariant (2).
When I (again: sloppily) wrote that "v depends on u", I was implicitly including
situations where u and v are not adjacent, i.e. we may have u;p_1;...;p_n;v.
Formally, for u;v define "v directly depends on u" iff commute(u,v) fails, then
"depends on" is the transitive closure of "directly depends on".
But that doesn't make sense. Suppose our universe of patches has x;u and x;v, which
can be merged cleanly to x;u;v', that is, commute(u^;v)=Just(v',_). So v does not
depend on u^. But we can also form the sequence u^;x^;x;v and now it would appear
that v does depend (indirectly) on u^ since none of the adjacent pairs in that
sequence commute!
(How is that possible? I guess the answer is that indeed the transitive closure here
is trivial i.e. relates any two patches. And this is probably true for any non
trivial universe of patches.)
So we need a better definition. One possibility is to define "depends on" only for
the subuniverses of either positive or negative patches. The transitive closure is
thus taken only over patches with the same polarity (given by the 'positiveId' method
of class SignedId).
That means the extended definition of "conflicts with" is also valid only if
restricted to positive patches. I think all the proofs will go through with that
restriction. We may need an additional invariant (3) stating that all elements of a
Contexted prim inside a Conflictor are positive. In fact, this is a stated property
that we test with QC.
I think this also clarifies why we are allowed (and indeed required) to "cancel
inverses" in Contexted prims, but not anywhere else. And the answer is that what we
actually do here is removing (positive) prims from the context by "adding inverses".
The definition of ctxAdd makes this quite clear: the first thing it tries is to
fastRemoveFL (invert p). So to prove that we maintain invariant (3) we need to show
that whenever we add a negative prim to a Contexted, it's inverse is already
contained in it.

msg23628 (view) 
Author: bfrk 
Date: 20230721.21:28:59 

I deleted the unscreened followup patches in favour of a single patch
(upcoming) that fixes a few errors, simplifies some of the proofs, and
(most importantly) takes my latest considerations into account.

msg23630 (view) 
Author: bfrk 
Date: 20230723.17:42:52 

The two dependencies (which I would like to screen to get them out of the
way) make minor refactors to the code itself. The changes to the proofs and
definitions are all in the last patch (which is not for screened yet).
I find the theory of the newly introduced relations "positively depends on"
and "positively conflicts with", quite interesting insofar as they clarify
why we need contexted prims. Indeed, the contexts contained in them are
exactly what we need to constructively /calculate/ these relations, provided
they are positive throughout as stated by invariant (3). Perhaps we should
move the definitions to D.P.V3.Contexted?
Another point that became clear to me is that ctxNoConflicts really is a
misnomer. The relation it expresses (again, assuming contexteds contain only
positive prims) is exactly what I called "(positively) unrelated", i.e. they
don't conflict and neither patch depends on the other. A better name would
thus be ctxUnrelated.
One last remark: I am aware that my definition of "positively depends on /
conflicts with" has the disadvantage of not being constructive, because of
the existential quantifiers. Your variant may thus be better suited for full
formalisation. However, I find them quite elegant to use for the sort of
informal reasoning we are doing here.
3 patches for repository http://darcs.net/screened:
patch 6258469bb43380d5f73532d5a7d88a7867f6444e
Author: Ben Franksen <ben.franksen@online.de>
Date: Sun Jul 23 09:19:35 CEST 2023
* RepoPatchV3: rename a local variable in commuteConflicting
patch 5a1177c436d5cafe50337833e614c0e81201b0c2
Author: Ben Franksen <ben.franksen@online.de>
Date: Mon Jul 3 23:02:52 CEST 2023
* RepoPatchV3 refactor commuteNoConflicts case for two conflictors
The code now mirrors the corresponding case in cleanMerge exactly.
patch 439bfa608121eb75932c4eb85c430367043a63d1
Author: Ben Franksen <ben.franksen@online.de>
Date: Fri Jul 21 21:31:58 CEST 2023
* WIP RepoPatchV3: refine and fix proofs
Attachments

msg23631 (view) 
Author: ganesh 
Date: 20230723.17:47:56 

No problem to screen things as convenient.

msg23632 (view) 
Author: ganesh 
Date: 20230723.22:23:02 

Couple of initial questions from a first glance:
> It follows from permutivity that "(positively/negatively) depends on" and
> "positively conflicts with" are commutation invariant and therefore depend
> only on the identity of the prims involved.
I don't think this is true by your definitions: for example if p and q
conflict "directly", i.e. cleanMerge (p :\/: q) fails, and p commutes
to p' which lives in a different context, then none of the clauses
for "conflicts with" apply.
I think it's a simple fix though, just start by talking about being able
to commute them to an common context.
> Also, both relations are irreflexive, so any patch is unrelated to itself.
Given we work on NamedPrims, this is sort of true, except that
cleanMerge (p :\/: p) is an error case which confuses the formal definitions
a bit.
> The two dependencies (which I would like to screen to get them out of
> the way) make minor refactors to the code itself.
>  commuteNoConflicts _ = Nothing
Did you drop this by mistake? I'm now getting incomplete patternmatch
warnings for several cases in commuteNoConflicts.

msg23633 (view) 
Author: bfrk 
Date: 20230725.23:55:06 

>>  commuteNoConflicts _ = Nothing
>
> Did you drop this by mistake? I'm now getting incomplete patternmatch
> warnings for several cases in commuteNoConflicts.
Ah, yes, removing this line actually belongs to another patch. I'm glad I
did in fact not yet screen those. Will fix and then send the amended
refactors separately.
Your observations about my new definitions are both good points, thanks
for noticing them! More details later.

msg23635 (view) 
Author: bfrk 
Date: 20230726.10:08:58 

Reworked definitions, following up on your latest comments.
1 patch for repository http://darcs.net/screened:
patch 1c9efc791a220f6992895ddd7dea49d1852564d3
Author: Ben Franksen <ben.franksen@online.de>
Date: Fri Jul 21 21:31:58 CEST 2023
* WIP RepoPatchV3: proofs and definitions
Attachments

msg23636 (view) 
Author: bfrk 
Date: 20230726.10:19:08 

Forgot to record a minor change that clarifies invariant (3).
1 patch for repository http://darcs.net/screened:
patch 5d1f8104581b352f09a002bcb4b0c3f1d67f2cc8
Author: Ben Franksen <ben.franksen@online.de>
Date: Fri Jul 21 21:31:58 CEST 2023
* WIP RepoPatchV3: proofs and definitions
Attachments

msg23644 (view) 
Author: ganesh 
Date: 20230729.14:42:43 

>  (ctxAddInvFL s) adds positive prims
I had to stop and think about this for a bit. I wonder if the code
in general would be easier to read if we made the first parameter to
Conflictor positive, so that all the contained patches are positive?

msg23645 (view) 
Author: bfrk 
Date: 20230729.15:48:23 

>>  (ctxAddInvFL s) adds positive prims
>
> I had to stop and think about this for a bit. I wonder if the code
> in general would be easier to read if we made the first parameter to
> Conflictor positive, so that all the contained patches are positive?
I have thought about this, too. This is how it was done for RepoPatchV2. In the
end I decided against that for several reasons. First, I always found the
witnesses somewhat confusing there. With the way Ian designed it, the prims in
a conflictor always point rightwards. To me this is the picture that makes the
most sense when thinking about e.g. how to define commute. Also, in many places
we do need the effect (as negative prims) for commutation with prims in plain
or in contexted form. So I think any clarity you may win for ctxAdd* would be
offset by a loss of clarity when commuting them.


Date 
User 
Action 
Args 
20230618 16:26:27  bfrk  create  
20230618 16:28:44  bfrk  set  status: needsscreening > needsreview 
20230716 22:04:10  ganesh  set  status: needsreview > reviewinprogress messages:
+ msg23606 
20230716 22:41:52  ganesh  set  messages:
+ msg23607 
20230718 20:34:07  bfrk  set  messages:
+ msg23616 
20230718 21:34:49  bfrk  set  messages:
+ msg23617 
20230719 00:24:55  ganesh  set  messages:
+ msg23618 
20230719 11:18:24  bfrk  set  messages:
+ msg23620 
20230719 20:08:16  ganesh  set  messages:
+ msg23621 
20230719 22:38:07  bfrk  set  files:
+ patchpreview.txt, repopatchv3_improvedefinitionofinvariant_2_.dpatch messages:
+ msg23623 
20230721 08:37:51  bfrk  set  files:
+ patchpreview.txt, repopatchv3_fixyetanotherproof.dpatch messages:
+ msg23624 
20230721 09:24:18  bfrk  set  messages:
+ msg23625 
20230721 09:35:42  bfrk  set  messages:
+ msg23626 
20230721 16:13:42  bfrk  set  messages:
+ msg23627 
20230721 21:25:21  bfrk  set  files:
 repopatchv3_improvedefinitionofinvariant_2_.dpatch 
20230721 21:25:27  bfrk  set  files:
 repopatchv3_fixyetanotherproof.dpatch 
20230721 21:25:32  bfrk  set  files:
 patchpreview.txt 
20230721 21:25:35  bfrk  set  files:
 patchpreview.txt 
20230721 21:29:00  bfrk  set  messages:
+ msg23628 
20230723 17:43:02  bfrk  set  files:
+ patchpreview.txt, repopatchv3_renamealocalvariableincommuteconflicting.dpatch messages:
+ msg23630 
20230723 17:48:02  ganesh  set  messages:
+ msg23631 
20230723 22:23:06  ganesh  set  messages:
+ msg23632 
20230725 23:55:07  bfrk  set  messages:
+ msg23633 
20230726 10:08:59  bfrk  set  files:
+ patchpreview.txt, wiprepopatchv3_proofsanddefinitions.dpatch messages:
+ msg23635 
20230726 10:13:28  bfrk  set  files:
 patchpreview.txt 
20230726 10:13:42  bfrk  set  files:
 repopatchv3_renamealocalvariableincommuteconflicting.dpatch 
20230726 10:19:09  bfrk  set  files:
+ patchpreview.txt, wiprepopatchv3_proofsanddefinitions.dpatch messages:
+ msg23636 
20230726 10:19:37  bfrk  set  files:
 patchpreview.txt 
20230726 10:19:43  bfrk  set  files:
 wiprepopatchv3_proofsanddefinitions.dpatch 
20230729 14:42:44  ganesh  set  messages:
+ msg23644 
20230729 15:48:24  bfrk  set  messages:
+ msg23645 
