[darcs-users] darcs patch: partial type witnesses in Unrevert (and 44 more)
David Roundy
droundy at darcs.net
Wed Aug 27 20:22:47 UTC 2008
On Wed, Aug 27, 2008 at 01:14:56PM -0700, Jason Dagit wrote:
> On Wed, Aug 27, 2008 at 12:06 PM, David Roundy <droundy at darcs.net> 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 <dagit at codersbase.com>
> > * updates to Repository.Internal to fix conflicts and support type witness refactor in commands
> >
> > Wed Aug 27 00:40:25 EDT 2008 Jason Dagit <dagit at codersbase.com>
> > * fix error in Properties due to new commuteFL
> >
> > Wed Aug 27 00:13:44 EDT 2008 Jason Dagit <dagit at codersbase.com>
> > * fix minor type witness compile error with new commuteFL
> >
> > Wed Aug 27 00:13:21 EDT 2008 Jason Dagit <dagit at codersbase.com>
> > * fix conflicts with get_extra changes
> >
> > Sun Aug 24 21:18:10 EDT 2008 Jason Dagit <dagit at codersbase.com>
> > * improve reporting for bug in get_extra
> >
> > Mon Aug 25 14:59:07 EDT 2008 Jason Dagit <dagit at codersbase.com>
> > * Finish refactor of Unrevert as well as making it pass double-unrevert.sh
> >
> > Mon Aug 25 14:32:35 EDT 2008 Jason Dagit <dagit at codersbase.com>
> > * add double-unrevert.sh test
> >
> > Wed Aug 13 01:38:37 EDT 2008 Jason Dagit <dagit at codersbase.com>
> > * 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 <dagit at codersbase.com>**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.
What's tr and tu?
> 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.
I understand that, but your changes are wrong with respect to the
code, and that's worse. We may as well make Repository.Internal
right, since we can't make the commands right.
And the truth is that the tentative state *does* exist, and we
*should* document it, and we should document it correctly. Certain
functions (e.g. those I changed back) can be run after a previous
function has changed the tentative state, and this needs to be
documented. Alas, we have no tracking of changes of the tentative
state, but that just means that we gain nothing by converting all the
commands to use type witnesses. It doesn't mean that we can't gain
anything in converting Repository--when we convert Repository, we gain
documentation, and I want it to be correct.
David
More information about the darcs-users
mailing list