On Wed, Aug 27, 2008 at 12:06 PM, David Roundy <[EMAIL PROTECTED]> wrote:
> On Wed, Aug 27, 2008 at 09:56:32AM -0700, Jason Dagit wrote:
>> David,
>>
>> This is the resend you requested.
>>
>> I can't be sure that the individal patches below will compile by themselves,
>> but
>> I know they result in a working darcs when applied together. Hopefully,
>> sending like this will make it easier for you to review them!
>
> I've applied:
>
> Wed Aug 27 12:53:27 EDT 2008 Jason Dagit <[EMAIL PROTECTED]>
> * updates to Repository.Internal to fix conflicts and support type witness
> refactor in commands
>
> Wed Aug 27 00:40:25 EDT 2008 Jason Dagit <[EMAIL PROTECTED]>
> * fix error in Properties due to new commuteFL
>
> Wed Aug 27 00:13:44 EDT 2008 Jason Dagit <[EMAIL PROTECTED]>
> * fix minor type witness compile error with new commuteFL
>
> Wed Aug 27 00:13:21 EDT 2008 Jason Dagit <[EMAIL PROTECTED]>
> * fix conflicts with get_extra changes
>
> Sun Aug 24 21:18:10 EDT 2008 Jason Dagit <[EMAIL PROTECTED]>
> * improve reporting for bug in get_extra
>
> Mon Aug 25 14:59:07 EDT 2008 Jason Dagit <[EMAIL PROTECTED]>
> * Finish refactor of Unrevert as well as making it pass double-unrevert.sh
>
> Mon Aug 25 14:32:35 EDT 2008 Jason Dagit <[EMAIL PROTECTED]>
> * add double-unrevert.sh test
>
> Wed Aug 13 01:38:37 EDT 2008 Jason Dagit <[EMAIL PROTECTED]>
> * partial type witnesses in Unrevert
>
>
> but I've spent most of my time reviewing the changes in
> Repository.Internal, and ended up reverting many of those changes
> (which were wrong).
>
>> [updates to Repository.Internal to fix conflicts and support type witness
>> refactor in commands
>> Jason Dagit <[EMAIL PROTECTED]>**20080827165327] hunk
>> ./src/Darcs/Repository/Internal.lhs 336
>> get_unrecorded :: RepoPatch p => Repository p C(r u t) -> IO (FL Prim C(r
>> u))
>> get_unrecorded = get_unrecorded_private id
>>
>> +-- | The /unrecorded/ includes the pending and the working directory
>> changes.
>> get_unrecorded_private :: RepoPatch p => ([DarcsFlag]->[DarcsFlag]) ->
>> Repository p C(r u t) -> IO (FL Prim C(r y))
>> get_unrecorded_private _ (Repo _ opts _ _)
>> | NoUpdateWorking `elem` opts = return $ unsafeCoerceP NilFL
>> hunk ./src/Darcs/Repository/Internal.lhs 573
>> decideHashedOrNormal rf $ HvsO {hashed =
>> HashedRepo.apply_to_tentative_pristine c opts p,
>> old =
>> DarcsRepo.add_to_tentative_pristine p}
>
> It looks pretty clear to me that tentativelyAddToPending is still used
> in a buggy manner. It's only used three times, but two of those make
> differents assumptions (the third is in Get, where we know there are
> initially no local changes), so fixing a bug in Unrevert will be
> guaranteed to create a bug in Unrecord (but in the command
> obliterate).
Well, the way I started thinking about tentativelyAddToPending is that
the pending has context C(r w), where w is the working copy context
(and thus the unrecorded changes are (pend +>+ working) :: C(r u). We
don't track the working copy context. That's why I changed it to x in
the type sig of tentatvelyAddToPending. Even if we add tr and tu to
the repository state below we're not tracking the working copy
context. Furthermore, as I understand it, even if we do track the
working copy context we'd still have the burden of proving that
sometimes w = r in some of the commands.
>
>> -tentativelyAddToPending :: forall p C(r u t y). RepoPatch p
>> - => Repository p C(r u t) -> [DarcsFlag] -> FL Prim
>> C(u y) -> IO ()
>> +-- | This fuction is unsafe because it accepts a patch that works on the
>> tentative
>> +-- pending and we don't currently track the state of the tentative pending.
>> +tentativelyAddToPending :: forall p C(r u t x y). RepoPatch p
>> + => Repository p C(r u t) -> [DarcsFlag] -> FL Prim
>> C(x y) -> IO ()
>> tentativelyAddToPending (Repo _ opts _ _) _ _
>> | NoUpdateWorking `elem` opts = return ()
>> | DryRun `elem` opts = bug "tentativelyAddToPending called when
>> --dry-run is specified"
>> hunk ./src/Darcs/Repository/Internal.lhs 585
>> let pn = pendingName rt
>> tpn = pn ++ ".tentative"
>> Sealed pend <- readPrims `liftM` (gzReadFilePS tpn `catchall` (return
>> nilPS))
>> - FlippedSeal newpend_ <- return $ newpend (unsafeCoerceP pend :: FL
>> Prim C(r t)) patch
>> + FlippedSeal newpend_ <- return $ newpend (unsafeCoerceP pend :: FL
>> Prim C(a x)) patch
>> writePatch tpn $ fromPrims_ newpend_
>> where newpend :: FL Prim C(a b) -> FL Prim C(b c) -> FlippedSeal (FL
>> Prim) C(c)
>> newpend NilFL patch_ = flipSeal patch_
>
> ..
>
>> tentativelyRemovePatches :: RepoPatch p => Repository p C(r u t) ->
>> [DarcsFlag]
>> - -> FL (Named p) C(x t) -> IO ()
>> + -> FL (Named p) C(x r) -> IO ()
>> tentativelyRemovePatches = tentativelyRemovePatches_ UpdatePristine
>
> The former definition is correct. A quick look at
> tentativelyRemovePatches_ shows that it is in fact the tentative
> inventory that is being modified, which requires that the patches be
> in the context of the tentative state.
>
> But it's a bit vague since with our current type witnesses 't' is
> always guaranteed to be the same as 'r', and there is no correct
> answer. Certainly with the type you've given this function, if it's
> called twice it will corrupt the repository. (It isn't called twice,
> but the type system can't check this, and there are reasonable reasons
> to call it twice, or to use some other repository-modifying command
> afterwards.)
As you said in a different email, we don't have a way to track state
mutation with the type witnesses. As you said here, we don't separate
tentative recorded (tr) from tentative unrecorded (tu). Which, as I
tried to point out in a different email (off list) which you said you
didn't read in detail, would be required to solve this ambiguity. As
such, I've pretty much stopped using the 't' type and I was tempted to
just remove it for now but have trouble justifying that work when I
could probably replace it with tr and tu for a similar amount of
effort. Then once I'm done adding tr and tu I'd run head first into
the problem of tracking the mutations of state.
We've rolled around ideas about tracking those mutations, but it seems
that doing it in a safe way requires formalizing something like Monad
but with either incompatible kinds or types (I forget which was the
bigger problem). Either way, it seems as though this would require a
new type or class similar to Monad (let's call it Monadish for this
discussion). Once we have that defined I imagine us lifting IO into
that new monadish. Now the inelegance of this solution rears it's
ugly head. We make very heavy use of the do-notation and we'd have to
revert all our monad code to use the monad primitives.
We *might* be able to make heavy use of GHC specific hacks to take
over the do-notation but I'm not sure. And as I understand it you
can't use both means of do-notation in the same module. This has the
implication that we'd need to make new Monadish instances for the
places that we use do-notation currently, such as Maybe and Either.
>> hunk ./src/Darcs/Repository/Internal.lhs 632
>> remove_from_unrevert_context repository ps
>> debugMessage "Removing changes from tentative inventory..."
>> if format_has HashedInventory rf
>> - then do HashedRepo.remove_from_tentative_inventory repository opts
>> ps
>> + -- I believe this call to
>> HashedRepo.remove_from_tentative_inventory is safe
>> + -- Because the above call to remove_from_unrevert_context ensures
>> that
>> + -- none of the patches in pending depend on ps.
>> + then do HashedRepo.remove_from_tentative_inventory repository opts
>> (unsafeCoerceP ps :: FL (Named p) C(x t))
>> when (up == UpdatePristine) $
>> HashedRepo.apply_to_tentative_pristine c opts $
>> progressFL "Applying inverse to pristine" $ invert ps
>
> The comment here is completely wrong. The call to
> remove_from_unrevert_context has no effect on pending, and no effect
> on the repository itself. Fortunately, fixing the bug in the type of
> this function removes the need for the unsafeCoerceP.
Ah right, I forgot to revise that comment after realizing that Pending
!= Tentative.
Changing the type to t would still be the wrong thing though. As t is
not a well-defined context. The reason I made it r is because we
don't have tr. Also, tr would be equal to r until we do our first
tentative operation, which is probably quite problematic to explain to
the type checker also.
>
>> hunk ./src/Darcs/Repository/Internal.lhs 642
>> -tentativelyReplacePatches :: forall p C(r u t). RepoPatch p => Repository p
>> C(r u t) -> [DarcsFlag]
>> - -> FL (Named p) C(r t) -> IO ()
>> -tentativelyReplacePatches repository opts ps =
>> +tentativelyReplacePatches :: forall p C(r u t x). RepoPatch p => Repository
>> p C(r u t) -> [DarcsFlag]
>> + -> FL (Named p) C(x r) -> IO ()
>> +tentativelyReplacePatches repository@(Repo x y z w) opts ps =
>> + -- tentativelyRemovePatches_ leaves the repository in state C(x u t)
>> do tentativelyRemovePatches_ DontUpdatePristine repository opts ps
>
> Again, this is vague, given that t and r are identical, but the
> correct answer is clearly t (because this calls
> tentativelyRemovePatches_).
If we were tracking tr an tu, the first step would result:
C(r u tr tu) -> C(r u x tu)
So, I disagree. Again, I took the liberty of ignoring t and using r
(for the reasons above).
>
>> hunk ./src/Darcs/Repository/Internal.lhs 647
>> - sequence_ $ mapAdd repository ps
>> + -- Now we add the patches back so that the repo again has state C(r
>> u t)
>> + sequence_ $ mapAdd ((Repo x y z w) :: Repository p C(x u t)) ps
>> where mapAdd :: Repository p C(i l m) -> FL (Named p) C(i j) -> [IO ()]
>> mapAdd _ NilFL = []
>> mapAdd r@(Repo dir df rf dr) (a:>:as) =
>
> Again, same issue here, that we can't write safe code that changes the
> repository, and thus must use unsafe hacks.
Yup :)
>> hunk ./src/Darcs/Repository/Internal.lhs 718
>> -patchSetToPatches :: RepoPatch p => PatchSet p C(x) -> FL (Named p) C(() x)
>> +patchSetToPatches :: RepoPatch p => RL (RL (PatchInfoAnd p)) C(x y) -> FL
>> (Named p) C(x y)
>> patchSetToPatches patchSet = mapFL_FL hopefully $ reverseRL $ concatRL
>> patchSet
>
> Fine.
>
>> hunk ./src/Darcs/Repository/Internal.lhs 783
>> remove_from_unrevert_context :: forall p C(r u t x). RepoPatch p
>> - => Repository p C(r u t) -> FL (Named p) C(x
>> t) -> IO ()
>> + => Repository p C(r u t) -> FL (Named p) C(x
>> r) -> IO ()
>
> Same issue. This function is only called once, and that single call
> was wrong.
Again, pick your poison.
>> remove_from_unrevert_context repository ps = do
>> Sealed bundle <- unrevert_patch_bundle `catchall` (return $ seal
>> (NilRL:<:NilRL))
>> remove_from_unrevert_context_ bundle
>> hunk ./src/Darcs/Repository/Internal.lhs 806
>> debugMessage "Adjusting the context of the unrevert changes..."
>> ref <- readTentativeRepo repository
>> case get_common_and_uncommon (bundle, ref) of
>> + -- This case means that the pending state has no changes
>> which are
>> + -- unique to the tentative state.
>> + -- This means that as far as the unrevert state is
>> concerned, r = t.
>> + -- This is why we have the unsafeCoerceP below.
>> (common,(h_us:<:NilRL):<:NilRL :\/: NilRL:<:NilRL) ->
>> hunk ./src/Darcs/Repository/Internal.lhs 811
>> - case commuteRL (reverseFL ps :> hopefully h_us) of
>> + case commuteRL (reverseFL ps :> hopefully
>> (unsafeCoerceP h_us :: (PatchInfoAnd p) C(r x))) of
>> Nothing -> unrevert_impossible unrevert_loc
>> Just (us' :> _) -> do
>> s <- slurp_recorded repository
>
> This comment is wrong, and the code is buggy as written--if you count
> the type witness as part of the code. A simple fix would be to
> replace readTentativeRepo with read_repo and to remove the
> unsafeCoerceP, but that would be a regression--reducing the code
> functionality to match what the type witnesses are capable of.
It's true the comment is wrong. I forgot to update that as my
understanding changed.
> A more interesting and correct fix would be to switch argument back to
> type 't' instead of 'r' and fix the calling code to also respect that
> type. But the 't' type really is useless in the current code, since
> the type witnesses don't support any scenario in which the two types
> are different.
Yeah, t is wrong.
> I'm pushing a change fixing these type witnesses... I guess it's
> basically just a revert of most of this patch, but it involved a
> careful review.
Okay, but I wish you hadn't :( If we're going to stop ignoring t and
really fix it we need to add tr and tu. Of course, that change
doesn't solve the problem that you want to solve. Adding those types
without the mutation tracking means the burden of proof is still on
the programmer.
I hope you can appreciate that from my point of view your reverts are
equally wrong to my changes. But, at least with my changes I was able
to add documentation at the call sites which tried to explain or give
a proof as to why the type witnesses didn't match the usage. In my
opinion, without the state tracking, the context of Repository is just
machine checkable documentation. meaning, it's not a proof, but a
guide and way to understand the code.
Jason
_______________________________________________
darcs-users mailing list
[email protected]
http://lists.osuosl.org/mailman/listinfo/darcs-users
