Enh/missing constraints

scripts/solve.py

@@ -1,9 +1,9 @@
 from __future__ import print_function
 
 import argparse
+import logging
 import sys
 
-
 from simplesat.dependency_solver import DependencySolver
 from simplesat.pool import Pool
 from simplesat.sat.policy import InstalledFirstPolicy
@@ -13,15 +13,15 @@
 
 def solve_and_print(request, remote_repositories, installed_repository,
                     print_ids, prune=True, prefer_installed=True, debug=0,
-                    simple=False):
+                    simple=False, strict=False):
     pool = Pool(remote_repositories)
     pool.add_repository(installed_repository)
 
     policy = InstalledFirstPolicy(pool, installed_repository,
                                   prefer_installed=prefer_installed)
     solver = DependencySolver(
         pool, remote_repositories, installed_repository,
-        policy=policy, use_pruning=prune)
+        policy=policy, use_pruning=prune, strict=strict)
 
     fmt = "ELAPSED : {description:20} : {elapsed:e}"
     try:
@@ -51,17 +51,25 @@ def main(argv=None):
     p.add_argument("--no-prune", dest="prune", action="store_false")
     p.add_argument("--no-prefer-installed", dest="prefer_installed",
                    action="store_false")
-    p.add_argument("-d", "--debug", action="count")
+    p.add_argument("-d", "--debug", default=0, action="count")
     p.add_argument("--simple", action="store_true",
                    help="Show a simpler description of the transaction.")
+    p.add_argument("--strict", action="store_true",
+                   help="Use stricter error checking for package metadata.")
 
     ns = p.parse_args(argv)
 
+    logging.basicConfig(
+        format=('%(asctime)s %(levelname)-8.8s [%(name)s:%(lineno)s]'
+                ' %(message)s'),
+        datefmt='%Y-%m-%d %H:%M:%S',
+        level=('INFO', 'WARNING', 'DEBUG')[ns.debug])
+
     scenario = Scenario.from_yaml(ns.scenario)
     solve_and_print(scenario.request, scenario.remote_repositories,
                     scenario.installed_repository, ns.print_ids,
                     prune=ns.prune, prefer_installed=ns.prefer_installed,
-                    debug=ns.debug, simple=ns.simple)
+                    debug=ns.debug, simple=ns.simple, strict=ns.strict)
 
 
 if __name__ == '__main__':

simplesat/dependency_solver.py

@@ -13,14 +13,16 @@
 
 class DependencySolver(object):
     def __init__(self, pool, remote_repositories, installed_repository,
-                 policy=None, use_pruning=True):
+                 policy=None, use_pruning=True, strict=False):
         self._pool = pool
         self._installed_repository = installed_repository
         self._remote_repositories = remote_repositories
+        self._last_rules_time = timed_context("Generate Rules")
+        self._last_solver_init_time = timed_context("Solver Init")
+        self._last_solve_time = timed_context("SAT Solve")
+
+        self.strict = strict
         self.use_pruning = use_pruning
-        self._last_rules_time = None
-        self._last_solver_init_time = None
-        self._last_solve_time = None
 
         self._policy = policy or InstalledFirstPolicy(
             pool, installed_repository
@@ -31,13 +33,13 @@ def solve(self, request):
         operations to apply to resolve it, or raise SatisfiabilityError
         if no resolution could be found.
         """
-        with timed_context("Generate Rules") as self._last_rules_time:
+        with self._last_rules_time:
             requirement_ids, rules = self._create_rules_and_initialize_policy(
                 request
             )
-        with timed_context("Solver Init") as self._last_solver_init_time:
+        with self._last_solver_init_time:
             sat_solver = MiniSATSolver.from_rules(rules, self._policy)
-        with timed_context("SAT Solve") as self._last_solve_time:
+        with self._last_solve_time:
             solution = sat_solver.search()
         solution_ids = _solution_to_ids(solution)
 
@@ -86,7 +88,7 @@ def key(package):
             installed_map[pool.package_id(package)] = package
 
         rules_generator = RulesGenerator(
-            pool, request, installed_map=installed_map)
+            pool, request, installed_map=installed_map, strict=self.strict)
 
         return all_requirement_ids, list(rules_generator.iter_rules())
 

simplesat/errors.py

@@ -27,6 +27,14 @@ def __init__(self, requirement, *a, **kw):
         self.args = self.args or (str(requirement),)
 
 
+class MissingInstallRequires(NoPackageFound):
+    pass
+
+
+class MissingConflicts(NoPackageFound):
+    pass
+
+
 class SatisfiabilityError(SolverException):
     def __init__(self, unsat):
         self.unsat = unsat

simplesat/rules_generator.py

@@ -1,11 +1,16 @@
 import collections
 import enum
+import logging
 
 from .constraints import Requirement
-from .errors import NoPackageFound, SolverException
+from .errors import (
+    MissingConflicts, MissingInstallRequires, NoPackageFound, SolverException
+)
 from .request import JobType
 
 
+logger = logging.getLogger(__name__)
+
 INDENT = 4
 
 
@@ -19,6 +24,7 @@ class RuleType(enum.Enum):
     package_same_name = 10
     package_implicit_obsoletes = 11
     package_installed = 12
+    package_broken = 100
 
     internal = 256
 
@@ -113,6 +119,12 @@ def to_string(self, pool, unique=False):
             left = pool.id_to_string(abs(left_id))[1:]
             right = pool.id_to_string(abs(right_id))
             rule_desc = "{} conflicts with {}".format(left, right)
+        elif self._reason == RuleType.package_broken:
+            package_id = self.literals[0]
+            # Trim the sign
+            package_str = pool.id_to_string(abs(package_id))
+            msg = "{} was ignored because it depends on missing packages"
+            rule_desc = msg.format(package_str)
         else:
             rule_desc = s
 
@@ -135,13 +147,14 @@ def __hash__(self):
 
 
 class RulesGenerator(object):
-    def __init__(self, pool, request, installed_map=None):
+    def __init__(self, pool, request, installed_map=None, strict=False):
         self._rules_set = collections.OrderedDict()
         self._pool = pool
 
         self.request = request
         self.installed_map = installed_map or collections.OrderedDict()
         self.added_package_ids = set()
+        self.strict = strict
 
     def iter_rules(self):
         """
@@ -284,6 +297,7 @@ def _add_rule(self, rule, rule_type):
             self._rules_set[rule] = None
 
     def _add_install_requires_rules(self, package, work_queue, requirements):
+        all_dependency_candidates = []
         for constraints in package.install_requires:
             pkg_requirement = Requirement.from_constraints(constraints)
             dependency_candidates = self._pool.what_provides(pkg_requirement)
@@ -296,20 +310,44 @@ def _add_install_requires_rules(self, package, work_queue, requirements):
                 else None)
 
             if not dependency_candidates:
-                msg = ("No candidates found for requirement {0!r}, needed for "
-                       "dependency {1!r}")
-                raise NoPackageFound(
-                    pkg_requirement,
-                    msg.format(pkg_requirement.name, package),
+                pkg_msg = "'{0.name} {0.version}'"
+                if hasattr(package, 'repository_info'):
+                    pkg_msg += " from '{0.repository_info.name}'"
+                pkg_str = pkg_msg.format(package)
+                req_str = str(pkg_requirement)
+                msg = ("Blocking package {0!s}: no candidates found for"
+                       " dependency {1!r}").format(pkg_str, req_str)
+                if self.strict:
+                    # We only raise an exception if this comes directly from a
+                    # job requirement. Unfortunately, we don't track that
+                    # explicitly because we push all of the work through a
+                    # queue. As a proxy, we can examine the associated
+                    # requirements directly. Everything is rooted in a job, so
+                    # if there's only one requirement, that must be it.
+                    if len(requirements) == 1:
+                        raise MissingInstallRequires(pkg_requirement, msg)
+                    else:
+                        logger.warning(msg)
+                else:
+                    logger.info(msg)
+
+                rule = self._create_remove_rule(
+                    package, RuleType.package_broken,
+                    requirements=combined_requirements,
                 )
+                self._add_rule(rule, "package")
+                return
 
             rule = self._create_dependency_rule(
                 package, dependency_candidates, RuleType.package_requires,
                 combined_requirements)
             self._add_rule(rule, "package")
-
-            for candidate in dependency_candidates:
-                work_queue.append((candidate, combined_requirements))
+            # We're "buffering" this so that we don't queue up any dependencies
+            # unless they are all successfully processed
+            all_dependency_candidates.extend(
+                (candidate, combined_requirements)
+                for candidate in dependency_candidates)
+        work_queue.extend(all_dependency_candidates)
 
     def _add_conflicts_rules(self, package, requirements):
         """
@@ -345,12 +383,27 @@ def _add_conflicts_rules(self, package, requirements):
                 else None)
 
             if not conflict_providers:
-                msg = ("No candidates found for requirement {0!r}, needed for "
-                       "conflict {1!r}")
-                raise NoPackageFound(
-                    pkg_requirement,
-                    msg.format(pkg_requirement.name, package),
-                )
+                pkg_msg = "'{0.name} {0.version}'"
+                if hasattr(package, 'repository_info'):
+                    pkg_msg += " from '{0.repository_info.name}'"
+                pkg_str = pkg_msg.format(package)
+                req_str = str(pkg_requirement)
+                msg = ("No candidates found for requirement {0!r}, needed"
+                       " for conflict with {1!s}").format(req_str, pkg_str)
+                if self.strict:
+                    # We only raise an exception if this comes directly from a
+                    # job requirement. Unfortunately, we don't track that
+                    # explicitly because we push all of the work through a
+                    # queue. As a proxy, we can examine the associated
+                    # requirements directly.
+                    if len(requirements) == 1:
+                        raise MissingConflicts(pkg_requirement, msg)
+                    else:
+                        logger.warning(msg)
+                else:
+                    # We just ignore missing constraints. They don't break
+                    # anything.
+                    logger.info(msg)
 
             for provider in conflict_providers:
                 rule = self._create_conflicts_rule(

simplesat/sat/minisat.py

@@ -99,7 +99,7 @@ def _find_conflict_paths(self, end_clauses, relevant_clauses):
 
             See https://github.com/enthought/sat-solver/wiki/Unsatisfiability-Error-Messages
             for discussion about how best to implement this.
-        """
+        """  # noqa
         # It's expensive to figure out which clauses are neighbors. This dict
         # maps ids to clauses containing that id. We can do this lookup for
         # each literal in a clause to get all of its neighbors.
@@ -345,7 +345,13 @@ def add_clause(self, clause, rule=None):
             self.status = False
         elif len(clause) == 1:
             # Unit facts are enqueued.
-            self.enqueue(clause[0], cause=clause)
+            if not self.enqueue(clause[0], cause=clause):
+                # Bail out if we've found a conflict
+                conflict = UNSAT(
+                    clause, clause,
+                    self.clause_trails,
+                    self.assigning_clauses)
+                raise SatisfiabilityError(conflict)
         else:
             p, q = clause[:2]
             self.watches[-p].append(clause)
@@ -391,7 +397,8 @@ def propagate(self):
                         self.enqueue(unit, clause)
 
     def enqueue(self, lit, cause=None):
-        """ Enqueue a new true literal.
+        """ Enqueue a new true literal. Return True if this assignment does not
+        conflict with a previous assignment, otherwise False.
 
         Parameters
         ----------
@@ -403,8 +410,6 @@ def enqueue(self, lit, cause=None):
         """
         status = self.assignments.value(lit)
         if status is not None:
-            # Known fact. Don't enqueue, but return whether this fact
-            # contradicts the earlier assignment.
             return status
         else:
             # New fact, store it.

simplesat/tests/missing_direct_conflict.yaml

@@ -0,0 +1,9 @@
+packages:
+    - MKL 10.3-1
+    - libgfortran 3.0.0-2
+    - numpy 1.9.2-1; conflicts (libgfortran ^= 3.0.0, MKL == 10.3-1)
+    - numpy 1.9.3-1; conflicts (libfortran ^= 3.0.0, MKL == 10.3-1)
+
+request:
+    - operation: "install"
+      requirement: "numpy >= 1.9"

simplesat/tests/missing_direct_dependency.yaml

@@ -0,0 +1,9 @@
+packages:
+    - MKL 10.3-1
+    - libgfortran 3.0.0-2
+    - numpy 1.9.2-1; depends (libgfortran ^= 3.0.0, MKL == 10.3-1)
+    - numpy 1.9.3-1; depends (libfortran ^= 3.0.0, MKL == 10.3-1)
+
+request:
+    - operation: "install"
+      requirement: "numpy >= 1.9"