Commit 48db1c08 authored by Duncan Coutts's avatar Duncan Coutts
Browse files

Extend the InstallPlan processing invariant

Add two additional properties that we believe are true:

 - All immediate reverse deps of packges that are currently processing
   are not currently being processed (ie not in the processing set).
 - The failed set is upwards closed, i.e. equal to its rev dep closure
parent 48a21cbf
......@@ -600,7 +600,14 @@ processingInvariant plan (Processing processingSet completedSet failedSet) =
&& noIntersection processingSet failedSet
-- intersection processingClosure failedSet is quite possible however
&& noIntersection failedSet completedSet
&& noIntersection processingClosure completedSet
&& noIntersection (reverseClosure processingSet) completedSet
&& failedSet == reverseClosure failedSet
&& and [ rdeppkgid `Set.notMember` processingSet
| pkgid <- Set.toList processingSet
, rdeppkgid <- maybe (internalError "processingInvariant")
(map nodeKey)
(Graph.revNeighbors (planIndex plan) pkgid)
]
&& and [ case Graph.lookup pkgid (planIndex plan) of
Just (Configured _) -> True
Just (PreExisting _) -> False
......@@ -608,12 +615,11 @@ processingInvariant plan (Processing processingSet completedSet failedSet) =
Nothing -> False
| pkgid <- Set.toList processingSet ++ Set.toList failedSet ]
where
processingClosure = Set.fromList
reverseClosure = Set.fromList
. map nodeKey
. fromMaybe (internalError "processingClosure")
. fromMaybe (internalError "processingInvariant")
. Graph.revClosure (planIndex plan)
. Set.toList
$ processingSet
noIntersection a b = Set.null (Set.intersection a b)
......
Markdown is supported
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment