Merge pull request haskell#5012 from grayjay/issue-4823

 Rerun dependency solver to generate a better error message (issue haskell#4823).

cabal-install/Distribution/Client/Dependency.hs

@@ -64,7 +64,7 @@ module Distribution.Client.Dependency (
   ) where
 
 import Distribution.Solver.Modular
-         ( modularResolver, SolverConfig(..) )
+         ( modularResolver, SolverConfig(..), PruneAfterFirstSuccess(..) )
 import Distribution.Simple.PackageIndex (InstalledPackageIndex)
 import qualified Distribution.Simple.PackageIndex as InstalledPackageIndex
 import Distribution.Client.SolverInstallPlan (SolverInstallPlan)
@@ -719,7 +719,7 @@ resolveDependencies platform comp pkgConfigDB solver params =
   $ runSolver solver (SolverConfig reordGoals cntConflicts
                       indGoals noReinstalls
                       shadowing strFlags allowBootLibs maxBkjumps enableBj
-                      solveExes order verbosity)
+                      solveExes order verbosity (PruneAfterFirstSuccess False))
                      platform comp installedPkgIndex sourcePkgIndex
                      pkgConfigDB preferences constraints targets
   where

cabal-install/Distribution/Solver/Modular.hs

@@ -1,5 +1,5 @@
 module Distribution.Solver.Modular
-         ( modularResolver, SolverConfig(..)) where
+         ( modularResolver, SolverConfig(..), PruneAfterFirstSuccess(..)) where
 
 -- Here, we try to map between the external cabal-install solver
 -- interface and the internal interface that the solver actually
@@ -9,25 +9,39 @@ module Distribution.Solver.Modular
 -- and finally, we have to convert back the resulting install
 -- plan.
 
-import Data.Map as M
-         ( fromListWith )
+import Data.Map (Map)
+import qualified Data.Map as M
+import Data.Set (Set)
+import Data.Ord
 import Distribution.Compat.Graph
          ( IsNode(..) )
+import Distribution.Compiler
+         ( CompilerInfo )
 import Distribution.Solver.Modular.Assignment
-         ( toCPs )
+         ( Assignment, toCPs )
 import Distribution.Solver.Modular.ConfiguredConversion
          ( convCP )
+import qualified Distribution.Solver.Modular.ConflictSet as CS
+import Distribution.Solver.Modular.Dependency
+import Distribution.Solver.Modular.Flag
+import Distribution.Solver.Modular.Index
 import Distribution.Solver.Modular.IndexConversion
          ( convPIs )
 import Distribution.Solver.Modular.Log
-         ( logToProgress )
+         ( SolverFailure(..), logToProgress )
 import Distribution.Solver.Modular.Package
          ( PN )
 import Distribution.Solver.Modular.Solver
-         ( SolverConfig(..), solve )
+         ( SolverConfig(..), PruneAfterFirstSuccess(..), solve )
+import Distribution.Solver.Types.DependencyResolver
 import Distribution.Solver.Types.LabeledPackageConstraint
 import Distribution.Solver.Types.PackageConstraint
-import Distribution.Solver.Types.DependencyResolver
+import Distribution.Solver.Types.PackagePath
+import Distribution.Solver.Types.PackagePreferences
+import Distribution.Solver.Types.PkgConfigDb
+         ( PkgConfigDb )
+import Distribution.Solver.Types.Progress
+import Distribution.Solver.Types.Variable
 import Distribution.System
          ( Platform(..) )
 import Distribution.Simple.Utils
@@ -38,9 +52,8 @@ import Distribution.Simple.Utils
 -- solver. Performs the necessary translations before and after.
 modularResolver :: SolverConfig -> DependencyResolver loc
 modularResolver sc (Platform arch os) cinfo iidx sidx pkgConfigDB pprefs pcs pns =
-  fmap (uncurry postprocess)                           $ -- convert install plan
-  logToProgress (solverVerbosity sc) (maxBackjumps sc) $ -- convert log format into progress format
-  solve sc cinfo idx pkgConfigDB pprefs gcs pns
+  fmap (uncurry postprocess) $ -- convert install plan
+  solve' sc cinfo idx pkgConfigDB pprefs gcs pns
     where
       -- Indices have to be converted into solver-specific uniform index.
       idx    = convPIs os arch cinfo (shadowPkgs sc) (strongFlags sc) (solveExecutables sc) iidx sidx
@@ -58,3 +71,95 @@ modularResolver sc (Platform arch os) cinfo iidx sidx pkgConfigDB pprefs pcs pns
       -- Helper function to extract the PN from a constraint.
       pcName :: PackageConstraint -> PN
       pcName (PackageConstraint scope _) = scopeToPackageName scope
+
+-- | Run 'D.S.Modular.Solver.solve' and then produce a summarized log to display
+-- in the error case.
+--
+-- When there is no solution, we produce the error message by rerunning the
+-- solver but making it prefer the goals from the final conflict set from the
+-- first run. We also set the backjump limit to 0, so that the log stops at the
+-- first backjump and is relatively short. Preferring goals from the final
+-- conflict set increases the probability that the log to the first backjump
+-- contains package, flag, and stanza choices that are relevant to the final
+-- failure. The solver shouldn't need to choose any packages that aren't in the
+-- final conflict set. (For every variable in the final conflict set, the final
+-- conflict set should also contain the variable that introduced that variable.
+-- The solver can then follow that chain of variables in reverse order from the
+-- user target to the conflict.) However, it is possible that the conflict set
+-- contains unnecessary variables.
+--
+-- Producing an error message when the solver reaches the backjump limit is more
+-- complicated. There is no final conflict set, so we create one for the minimal
+-- subtree containing the path that the solver took to the first backjump. This
+-- conflict set helps explain why the solver reached the backjump limit, because
+-- the first backjump contributes to reaching the backjump limit. Additionally,
+-- the solver is much more likely to be able to finish traversing this subtree
+-- before the backjump limit, since its size is linear (not exponential) in the
+-- number of goal choices. We create it by pruning all children after the first
+-- successful child under each node in the original tree, so that there is at
+-- most one valid choice at each level. Then we use the final conflict set from
+-- that run to generate an error message, as in the case where the solver found
+-- that there was no solution.
+--
+-- Using the full log from a rerun of the solver ensures that the log is
+-- complete, i.e., it shows the whole chain of dependencies from the user
+-- targets to the conflicting packages.
+solve' :: SolverConfig
+       -> CompilerInfo
+       -> Index
+       -> PkgConfigDb
+       -> (PN -> PackagePreferences)
+       -> Map PN [LabeledPackageConstraint]
+       -> Set PN
+       -> Progress String String (Assignment, RevDepMap)
+solve' sc cinfo idx pkgConfigDB pprefs gcs pns =
+    foldProgress Step createErrorMsg Done (runSolver sc)
+  where
+    runSolver :: SolverConfig
+              -> Progress String SolverFailure (Assignment, RevDepMap)
+    runSolver sc' =
+        logToProgress (solverVerbosity sc') (maxBackjumps sc') $ -- convert log format into progress format
+        solve sc' cinfo idx pkgConfigDB pprefs gcs pns
+
+    createErrorMsg :: SolverFailure
+                   -> Progress String String (Assignment, RevDepMap)
+    createErrorMsg (NoSolution cs        msg) =
+        Fail $ rerunSolverForErrorMsg cs msg
+    createErrorMsg (BackjumpLimitReached msg) =
+        Step ("Backjump limit reached. Rerunning dependency solver to generate "
+              ++ "a final conflict set for the search tree containing the "
+              ++ "first backjump.") $
+        foldProgress Step f Done $
+        runSolver sc { pruneAfterFirstSuccess = PruneAfterFirstSuccess True }
+      where
+        f :: SolverFailure -> Progress String String (Assignment, RevDepMap)
+        f (NoSolution cs        _) = Fail $ rerunSolverForErrorMsg cs msg
+        f (BackjumpLimitReached _) =
+            -- This case is possible when the number of goals involved in
+            -- conflicts is greater than the backjump limit.
+            Fail $ msg ++ "Failed to generate a summarized dependency solver "
+                       ++ "log due to low backjump limit."
+
+    rerunSolverForErrorMsg :: ConflictSet -> String -> String
+    rerunSolverForErrorMsg cs finalMsg =
+      let sc' = sc {
+                    goalOrder = Just (preferGoalsFromConflictSet cs)
+                  , maxBackjumps = Just 0
+                  }
+      in unlines ("Could not resolve dependencies:" : messages (runSolver sc'))
+          ++ finalMsg
+
+    messages :: Progress step fail done -> [step]
+    messages = foldProgress (:) (const []) (const [])
+
+-- | Goal ordering that chooses goals contained in the conflict set before
+-- other goals.
+preferGoalsFromConflictSet :: ConflictSet
+                           -> Variable QPN -> Variable QPN -> Ordering
+preferGoalsFromConflictSet cs =
+    comparing $ \v -> not $ CS.member (toVar v) cs
+  where
+    toVar :: Variable QPN -> Var QPN
+    toVar (PackageVar qpn)    = P qpn
+    toVar (FlagVar    qpn fn) = F (FN qpn fn)
+    toVar (StanzaVar  qpn sn) = S (SN qpn sn)

cabal-install/Distribution/Solver/Modular/Log.hs

@@ -1,13 +1,12 @@
 module Distribution.Solver.Modular.Log
     ( Log
     , logToProgress
+    , SolverFailure(..)
     ) where
 
 import Prelude ()
 import Distribution.Solver.Compat.Prelude
 
-import Data.List as L
-
 import Distribution.Solver.Types.Progress
 
 import Distribution.Solver.Modular.Dependency
@@ -23,20 +22,22 @@ import Distribution.Verbosity
 -- Parameterized over the type of actual messages and the final result.
 type Log m a = Progress m (ConflictSet, ConflictMap) a
 
-messages :: Progress step fail done -> [step]
-messages = foldProgress (:) (const []) (const [])
+data Exhaustiveness = Exhaustive | BackjumpLimit
 
-data Exhaustiveness = Exhaustive | BackjumpLimitReached
+-- | Information about a dependency solver failure. It includes an error message
+-- and a final conflict set, if available.
+data SolverFailure =
+    NoSolution ConflictSet String
+  | BackjumpLimitReached String
 
 -- | Postprocesses a log file. Takes as an argument a limit on allowed backjumps.
 -- If the limit is 'Nothing', then infinitely many backjumps are allowed. If the
 -- limit is 'Just 0', backtracking is completely disabled.
-logToProgress :: Verbosity -> Maybe Int -> Log Message a -> Progress String String a
+logToProgress :: Verbosity -> Maybe Int -> Log Message a -> Progress String SolverFailure a
 logToProgress verbosity mbj l =
-    let es = proc (Just 0) l -- catch first error (always)
-        ms = proc mbj l
-    in go es es -- trace for first error
-          (showMessages (const True) True ms) -- run with backjump limit applied
+    let ms = proc mbj l
+        mapFailure f = foldProgress Step (Fail . f) Done
+    in mapFailure finalError (showMessages ms) -- run with backjump limit applied
   where
     -- Proc takes the allowed number of backjumps and a 'Progress' and explores the
     -- messages until the maximum number of backjumps has been reached. It filters out
@@ -48,45 +49,25 @@ logToProgress verbosity mbj l =
     proc _        (Fail (cs, cm))                   = Fail (Exhaustive, cs, cm)
     proc mbj'     (Step x@(Failure cs Backjump) xs@(Step Leave (Step (Failure cs' Backjump) _)))
       | cs == cs'                                   = Step x (proc mbj'           xs) -- repeated backjumps count as one
-    proc (Just 0) (Step   (Failure cs Backjump)  _) = Fail (BackjumpLimitReached, cs, mempty) -- No final conflict map available
+    proc (Just 0) (Step   (Failure cs Backjump)  _) = Fail (BackjumpLimit, cs, mempty) -- No final conflict map available
     proc (Just n) (Step x@(Failure _  Backjump) xs) = Step x (proc (Just (n - 1)) xs)
     proc mbj'     (Step x                       xs) = Step x (proc mbj'           xs)
 
-    -- The first two arguments are both supposed to be the log up to the first error.
-    -- That's the error that will always be printed in case we do not find a solution.
-    -- We pass this log twice, because we evaluate it in parallel with the full log,
-    -- but we also want to retain the reference to its beginning for when we print it.
-    -- This trick prevents a space leak!
-    --
-    -- The third argument is the full log, ending with either the solution or the
-    -- exhaustiveness and final conflict set.
-    go :: Progress Message (Exhaustiveness, ConflictSet, ConflictMap) b
-       -> Progress Message (Exhaustiveness, ConflictSet, ConflictMap) b
-       -> Progress String  (Exhaustiveness, ConflictSet, ConflictMap) b
-       -> Progress String String b
-    go ms (Step _ ns)        (Step x xs)           = Step x (go ms ns xs)
-    go ms r                  (Step x xs)           = Step x (go ms r  xs)
-    go ms (Step _ ns)        r                     = go ms ns r
-    go ms (Fail (_, cs', _)) (Fail (exh, cs, cm))  = Fail $
-        "Could not resolve dependencies:\n" ++
-        unlines (messages $ showMessages (L.foldr (\ v _ -> v `CS.member` cs') True) False ms) ++
+    finalError :: (Exhaustiveness, ConflictSet, ConflictMap) -> SolverFailure
+    finalError (exh, cs, cm) =
         case exh of
             Exhaustive ->
+                NoSolution cs $
                 "After searching the rest of the dependency tree exhaustively, "
                 ++ "these were the goals I've had most trouble fulfilling: "
                 ++ showCS cm cs
               where
                 showCS = if verbosity > normal
                          then CS.showCSWithFrequency
                          else CS.showCSSortedByFrequency
-            BackjumpLimitReached ->
+            BackjumpLimit ->
+                BackjumpLimitReached $
                 "Backjump limit reached (" ++ currlimit mbj ++
                 "change with --max-backjumps or try to run with --reorder-goals).\n"
               where currlimit (Just n) = "currently " ++ show n ++ ", "
                     currlimit Nothing  = ""
-    go _  _                  (Done s)              = Done s
-    go _  (Done _)           (Fail _)              = Fail $
-        -- Should not happen: Second argument is the log up to first error,
-        -- third one is the entire log. Therefore it should never happen that
-        -- the second log finishes with 'Done' and the third log with 'Fail'.
-        "Could not resolve dependencies; something strange happened."