clean up post rebase

lib/spack/spack/solver/asp.py

@@ -614,6 +614,23 @@ class ErrorHandler:
     def no_value_error(self, attribute, pkg):
         return f'Cannot select a single "{attribute}" for package "{pkg}"'
 
+    def _get_cause_tree(self, cause, conditions, condition_causes, literals, indent="        "):
+        parents = [c for e, c in condition_causes if e == cause]
+        local = "required because %s " % conditions[cause]
+
+        return [indent + local] + [
+            c
+            for parent in parents
+            for c in self._get_cause_tree(
+                parent, conditions, condition_causes, literals, indent=indent + "  "
+            )
+        ]
+
+    def get_cause_tree(self, cause):
+        conditions = dict(extract_args(self.model, "condition"))
+        condition_causes = list(extract_args(self.model, "condition_cause"))
+        return self._get_cause_tree(cause, conditions, condition_causes, [])
+
     def handle_error(self, msg, *args):
         """Handle an error state derived by the solver."""
         if msg == "multiple_values_error":
@@ -622,14 +639,28 @@ class ErrorHandler:
         if msg == "no_value_error":
             return self.no_value_error(*args)
 
+        try:
+            idx = args.index("startcauses")
+        except ValueError:
+            msg_args = args
+            cause_args = []
+        else:
+            msg_args = args[:idx]
+            cause_args = args[idx + 1 :]
+
+        msg = msg.format(*msg_args)
+
         # For variant formatting, we sometimes have to construct specs
         # to format values properly. Find/replace all occurances of
         # Spec(...) with the string representation of the spec mentioned
-        msg = msg.format(*args)
         specs_to_construct = re.findall(r"Spec\(([^)]*)\)", msg)
         for spec_str in specs_to_construct:
             msg = msg.replace("Spec(%s)" % spec_str, str(spack.spec.Spec(spec_str)))
 
+        for cause in set(cause_args):
+            for c in self.get_cause_tree(cause):
+                msg += f"\n{c}"
+
         return msg
 
     def message(self, errors) -> str:
@@ -775,6 +806,8 @@ class PyclingoDriver(object):
         self.control.load(os.path.join(parent_dir, "concretize.lp"))
         self.control.load(os.path.join(parent_dir, "os_compatibility.lp"))
         self.control.load(os.path.join(parent_dir, "display.lp"))
+        if spack.error.debug:
+            self.control.load(os.path.join(parent_dir, "causation.lp"))
         timer.stop("load")
 
         # Grounding is the first step in the solve -- it turns our facts
@@ -835,7 +868,13 @@ class PyclingoDriver(object):
 
             # print any unknown functions in the model
             for sym in best_model:
-                if sym.name not in ("attr", "error", "opt_criterion"):
+                if sym.name not in (
+                    "attr",
+                    "error",
+                    "opt_criterion",
+                    "condition",
+                    "condition_cause",
+                ):
                     tty.debug(
                         "UNKNOWN SYMBOL: %s(%s)" % (sym.name, ", ".join(stringify(sym.arguments)))
                     )
@@ -1266,7 +1305,11 @@ class SpackSolverSetup(object):
             for when in whens:
                 msg = "%s provides %s when %s" % (pkg.name, provided, when)
                 condition_id = self.condition(when, provided, pkg.name, msg)
-                self.gen.fact(fn.provider_condition(condition_id, when.name, provided.name))
+                self.gen.fact(
+                    fn.imposed_constraint(
+                        condition_id, "virtual_condition_holds", pkg.name, provided.name
+                    )
+                )
             self.gen.newline()
 
     def package_dependencies_rules(self, pkg):
@@ -1287,16 +1330,25 @@ class SpackSolverSetup(object):
                 if not deptypes:
                     continue
 
-                msg = "%s depends on %s" % (pkg.name, dep.spec.name)
+                msg = "%s depends on %s" % (pkg.name, dep.spec)
                 if cond != spack.spec.Spec():
                     msg += " when %s" % cond
 
                 condition_id = self.condition(cond, dep.spec, pkg.name, msg)
-                self.gen.fact(fn.dependency_condition(condition_id, pkg.name, dep.spec.name))
+                self.gen.fact(fn.condition_requirement(condition_id, "spack_installed", pkg.name))
 
                 for t in sorted(deptypes):
                     # there is a declared dependency of type t
-                    self.gen.fact(fn.dependency_type(condition_id, t))
+                    self.gen.fact(
+                        fn.imposed_constraint(
+                            condition_id, "dependency_holds", pkg.name, dep.spec.name, t
+                        )
+                    )
+                self.gen.fact(
+                    fn.imposed_constraint(
+                        condition_id, "virtual_node" if dep.spec.virtual else "node", dep.spec.name
+                    )
+                )
 
                 self.gen.newline()
 
@@ -1450,7 +1502,11 @@ class SpackSolverSetup(object):
             for local_idx, spec in enumerate(external_specs):
                 msg = "%s available as external when satisfying %s" % (spec.name, spec)
                 condition_id = self.condition(spec, msg=msg)
-                self.gen.fact(fn.possible_external(condition_id, pkg_name, local_idx))
+                self.gen.fact(
+                    fn.imposed_constraint(
+                        condition_id, "external_conditions_hold", pkg_name, local_idx
+                    )
+                )
                 self.possible_versions[spec.name].add(spec.version)
                 self.gen.newline()
 
@@ -2294,16 +2350,29 @@ class SpackSolverSetup(object):
         self.define_target_constraints()
 
     def literal_specs(self, specs):
-        for idx, spec in enumerate(specs):
+        for spec in specs:
             self.gen.h2("Spec: %s" % str(spec))
-            self.gen.fact(fn.literal(idx))
 
-            self.gen.fact(fn.literal(idx, "virtual_root" if spec.virtual else "root", spec.name))
+            # cannot use self.condition because it requires condition requirements
+            condition_id = next(self._condition_id_counter)
+            self.gen.fact(fn.condition(condition_id, "%s is provided as input spec" % spec))
+            self.gen.fact(fn.literal(condition_id))
+
+            self.gen.fact(fn.condition_requirement(condition_id, "literal_solved", condition_id))
+
+            self.gen.fact(
+                fn.imposed_constraint(
+                    condition_id, "virtual_root" if spec.virtual else "root", spec.name
+                )
+            )
+
             for clause in self.spec_clauses(spec):
-                self.gen.fact(fn.literal(idx, *clause.args))
+                self.gen.fact(fn.imposed_constraint(condition_id, *clause.args))
                 if clause.args[0] == "variant_set":
                     self.gen.fact(
-                        fn.literal(idx, "variant_default_value_from_cli", *clause.args[1:])
+                        fn.imposed_constraint(
+                            condition_id, "variant_default_value_from_cli", *clause.args[1:]
+                        )
                     )
 
         if self.concretize_everything:
@@ -2397,6 +2466,8 @@ class SpecBuilder(object):
                 r"^root$",
                 r"^virtual_node$",
                 r"^virtual_root$",
+                r"^.*holds?$",
+                r"^literal.*$",
             ]
         )
     )

lib/spack/spack/solver/causation.lp

@@ -0,0 +1,72 @@
+% Copyright 2013-2022 Lawrence Livermore National Security, LLC and other
+% Spack Project Developers. See the top-level COPYRIGHT file for details.
+%
+% SPDX-License-Identifier: (Apache-2.0 OR MIT)
+
+% associated conditions by cause -> effect
+condition_cause(Effect, Cause) :-
+  condition_holds(Effect), condition_holds(Cause),
+  attr(Name, A1),
+  condition_requirement(Effect, Name, A1),
+  imposed_constraint(Cause, Name, A1).
+condition_cause(Effect, Cause) :-
+  condition_holds(Effect), condition_holds(Cause),
+  attr(Name, A1, A2),
+  condition_requirement(Effect, Name, A1, A2),
+  imposed_constraint(Cause, Name, A1, A2).
+condition_cause(Effect, Cause) :-
+  condition_holds(Effect), condition_holds(Cause),
+  attr(Name, A1, A2, A3),
+  condition_requirement(Effect, Name, A1, A2, A3),
+  imposed_constraint(Cause, Name, A1, A2, A3).
+condition_cause(Effect, Cause) :-
+  condition_holds(Effect), condition_holds(Cause),
+  attr(Name, A1, A2, A3, A4),
+  condition_requirement(Effect, Name, A1, A2, A3, A4),
+  imposed_constraint(Cause, Name, A1, A2, A3, A4).
+
+% At most one variant for single valued variants
+error(0, "'{0}' required multiple values for single-valued variant '{1}'\n    Requested 'Spec({1}={2})' and 'Spec({1}={3})'", Package, Variant, Value1, Value2, startcauses, Cause1, Cause2)
+  :- attr("node", Package),
+     variant(Package, Variant),
+     variant_single_value(Package, Variant),
+     build(Package),
+     attr("variant_value", Package, Variant, Value1),
+     imposed_constraint(Cause1, "variant_set", Package, Variant, Value1),
+     condition_holds(Cause1),
+     attr("variant_value", Package, Variant, Value2),
+     imposed_constraint(Cause2, "variant_set", Package, Variant, Value2),
+     condition_holds(Cause2),
+     Value1 < Value2. % see[1] in concretize.lp
+
+% We cannot have a version that violates another version constraint
+error(0, "Version '{0}' of {1} does not satisfy '@{2}'", Version, Package, Constraint, startcauses, VersionCause, ConstraintCause)
+ :- attr("node", Package),
+    attr("version", Package, Version),
+    imposed_constraint(VersionCause, "node_version_satisfies", Package, Version),
+    condition_holds(VersionCause),
+    attr("node_version_satisfies", Package, Constraint),
+    imposed_constraint(ConstraintCause, "node_version_satisfies", Package, Constraint),
+    condition_holds(ConstraintCause),
+    not version_satisfies(Package, Constraint, Version).
+
+% A virtual package may or may not have a version, but never has more than one
+% Error to catch how it happens
+error(0, "Version '{0}' of {1} does not satisfy '@{2}'", Version, Virtual, Constraint, startcauses, VersionCause, ConstraintCause)
+ :- attr("virtual_node", Virtual),
+    attr("version", Virtual, Version),
+    imposed_constraint(VersionCause, "node_version_satisfies", Virtual, Version),
+    condition_holds(VersionCause),
+    attr("node_version_satisfies", Virtual, Constraint),
+    imposed_constraint(ConstraintCause, "node_version_satisfies", Virtual, Constraint),
+    condition_holds(ConstraintCause),
+    not version_satisfies(Virtual, Constraint, Version).
+
+% More specific error message if the version cannot satisfy some constraint
+% Otherwise covered by `no_version_error` and `versions_conflict_error`.
+error(0, "Cannot satisfy '{0}@{1}'", Package, Constraint, startcauses, ConstraintCause)
+  :- attr("node_version_satisfies", Package, Constraint),
+     imposed_constraint(ConstraintCause, "node_version_satisfies", Package, Constraint),
+     condition_holds(ConstraintCause),
+     attr("version", Package, Version),
+     not version_satisfies(Package, Constraint, Version).

lib/spack/spack/solver/concretize.lp

@@ -12,8 +12,8 @@
 %-----------------------------------------------------------------------------
 
 % Give clingo the choice to solve an input spec or not
-{ literal_solved(ID) } :- literal(ID).
-literal_not_solved(ID) :- not literal_solved(ID), literal(ID).
+{ attr("literal_solved", ID) } :- literal(ID).
+literal_not_solved(ID) :- not attr("literal_solved", ID), literal(ID).
 
 % If concretize_everything() is a fact, then we cannot have unsolved specs
 :- literal_not_solved(ID), concretize_everything.
@@ -21,24 +21,14 @@ literal_not_solved(ID) :- not literal_solved(ID), literal(ID).
 % Make a problem with "zero literals solved" unsat. This is to trigger
 % looking for solutions to the ASP problem with "errors", which results
 % in better reporting for users. See #30669 for details.
-1 { literal_solved(ID) : literal(ID) }.
+1 { attr("literal_solved", ID) : literal(ID) }.
 
 opt_criterion(300, "number of input specs not concretized").
 #minimize{ 0@300: #true }.
 #minimize { 1@300,ID : literal_not_solved(ID) }.
 
-% Map constraint on the literal ID to the correct PSID
-attr(Name, A1)             :- literal(LiteralID, Name, A1), literal_solved(LiteralID).
-attr(Name, A1, A2)         :- literal(LiteralID, Name, A1, A2), literal_solved(LiteralID).
-attr(Name, A1, A2, A3)     :- literal(LiteralID, Name, A1, A2, A3), literal_solved(LiteralID).
-attr(Name, A1, A2, A3, A4) :- literal(LiteralID, Name, A1, A2, A3, A4), literal_solved(LiteralID).
-
 #defined concretize_everything/0.
 #defined literal/1.
-#defined literal/3.
-#defined literal/4.
-#defined literal/5.
-#defined literal/6.
 
 % Attributes for node packages which must have a single value
 attr_single_value("version").
@@ -58,6 +48,13 @@ error(100, multiple_values_error, Attribute, Package)
      attr_single_value(Attribute),
      2 { attr(Attribute, Package, Version) }.
 
+%-----------------------------------------------------------------------------
+% Define functions for error handling
+%-----------------------------------------------------------------------------
+
+#defined error/9.
+#defined condition_cause/2.
+
 %-----------------------------------------------------------------------------
 % Version semantics
 %-----------------------------------------------------------------------------
@@ -96,7 +93,18 @@ version_satisfies(Package, Constraint, HashVersion) :- version_satisfies(Package
 { attr("version", Package, Version) : version_declared(Package, Version) }
  :- attr("node", Package).
 
+% Error to ensure structure of the program is not violated
+error(2, "No version from '{0}' satisfies '@{1}' and '@{2}'", Package, Version1, Version2)
+  :- attr("node", Package),
+     attr("version", Package, Version1),
+     attr("version", Package, Version2),
+     Version1 < Version2.  % see[1]
+
+error(2, "No versions available for package '{0}'", Package)
+  :- attr("node", Package), not attr("version", Package, _).
+
 % A virtual package may or may not have a version, but never has more than one
+% fallback error for structure in case there's another way for it to happen
 error(100, "Cannot select a single version for virtual '{0}'", Virtual)
   :- attr("virtual_node", Virtual),
      2 { attr("version", Virtual, Version) }.
@@ -150,8 +158,7 @@ possible_version_weight(Package, Weight)
   :- attr("node_version_satisfies", Package, Constraint),
      version_satisfies(Package, Constraint, _).
 
-% More specific error message if the version cannot satisfy some constraint
-% Otherwise covered by `no_version_error` and `versions_conflict_error`.
+% Error for structure of program
 error(10, "Cannot satisfy '{0}@{1}'", Package, Constraint)
   :- attr("node_version_satisfies", Package, Constraint),
      attr("version", Package, Version),
@@ -182,9 +189,8 @@ condition_holds(ID) :-
   attr(Name, A1, A2, A3)     : condition_requirement(ID, Name, A1, A2, A3);
   attr(Name, A1, A2, A3, A4) : condition_requirement(ID, Name, A1, A2, A3, A4).
 
-% condition_holds(ID) implies all imposed_constraints, unless do_not_impose(ID)
-% is derived. This allows imposed constraints to be canceled in special cases.
-impose(ID) :- condition_holds(ID), not do_not_impose(ID).
+% condition_holds(ID) implies all imposed_constraints.
+impose(ID) :- condition_holds(ID).
 
 % conditions that hold impose constraints on other specs
 attr(Name, A1)             :- impose(ID), imposed_constraint(ID, Name, A1).
@@ -229,33 +235,19 @@ depends_on(Package, Dependency) :- attr("depends_on", Package, Dependency, _).
 % a dependency holds if its condition holds and if it is not external or
 % concrete. We chop off dependencies for externals, and dependencies of
 % concrete specs don't need to be resolved -- they arise from the concrete
-% specs themselves.
-dependency_holds(Package, Dependency, Type) :-
-  dependency_condition(ID, Package, Dependency),
-  dependency_type(ID, Type),
-  build(Package),
-  not external(Package),
-  condition_holds(ID).
-
-% We cut off dependencies of externals (as we don't really know them).
-% Don't impose constraints on dependencies that don't exist.
-do_not_impose(ID) :-
-  not dependency_holds(Package, Dependency, _),
-  dependency_condition(ID, Package, Dependency).
+% specs themselves. This attr is used in constraints from dependency conditions
+attr("spack_installed", Package) :- build(Package), not external(Package).
 
 % declared dependencies are real if they're not virtual AND
 % the package is not an external.
 % They're only triggered if the associated dependnecy condition holds.
 attr("depends_on", Package, Dependency, Type)
- :- dependency_holds(Package, Dependency, Type),
+ :- attr("dependency_holds", Package, Dependency, Type),
     not virtual(Dependency).
 
 % every root must be a node
 attr("node", Package) :- attr("root", Package).
 
-% dependencies imply new nodes
-attr("node", Dependency) :- attr("node", Package), depends_on(Package, Dependency).
-
 % all nodes in the graph must be reachable from some root
 % this ensures a user can't say `zlib ^libiconv` (neither of which have any
 % dependencies) and get a two-node unconnected graph
@@ -296,14 +288,17 @@ error(1, Msg) :- attr("node", Package),
 % if a package depends on a virtual, it's not external and we have a
 % provider for that virtual then it depends on the provider
 attr("depends_on", Package, Provider, Type)
-  :- dependency_holds(Package, Virtual, Type),
+  :- attr("dependency_holds", Package, Virtual, Type),
      provider(Provider, Virtual),
      not external(Package).
 
-% dependencies on virtuals also imply that the virtual is a virtual node
-attr("virtual_node", Virtual)
-  :- dependency_holds(Package, Virtual, Type),
-     virtual(Virtual), not external(Package).
+% If a package depends on a provider, the provider must be a node
+% nodes that are not indirected by a virtual are instantiated
+% directly from the imposed constraints of the dependency condition
+attr("node", Provider)
+  :- attr("dependency_holds", Package, Virtual, Type),
+     provider(Provider, Virtual),
+     not external(Package).
 
 % If there's a virtual node, we must select one and only one provider.
 % The provider must be selected among the possible providers.
@@ -330,17 +325,11 @@ attr("root", Package) :- attr("virtual_root", Virtual), provider(Package, Virtua
 % for environments that are concretized together (e.g. where we
 % asks to install "mpich" and "hdf5+mpi" and we want "mpich" to
 % be the mpi provider)
-provider(Package, Virtual) :- attr("node", Package), virtual_condition_holds(Package, Virtual).
-
-% The provider provides the virtual if some provider condition holds.
-virtual_condition_holds(Provider, Virtual) :-
-   provider_condition(ID, Provider, Virtual),
-   condition_holds(ID),
-   virtual(Virtual).
+provider(Package, Virtual) :- attr("node", Package), attr("virtual_condition_holds", Package, Virtual).
 
 % A package cannot be the actual provider for a virtual if it does not
 % fulfill the conditions to provide that virtual
-:- provider(Package, Virtual), not virtual_condition_holds(Package, Virtual),
+:- provider(Package, Virtual), not attr("virtual_condition_holds", Package, Virtual),
    internal_error("Virtual when provides not respected").
 
 #defined possible_provider/2.
@@ -382,14 +371,8 @@ possible_provider_weight(Dependency, Virtual, 100, "fallback") :- provider(Depen
 
 % do not warn if generated program contains none of these.
 #defined possible_provider/2.
-#defined provider_condition/3.
-#defined required_provider_condition/3.
-#defined required_provider_condition/4.
-#defined required_provider_condition/5.
-#defined required_provider_condition/6.
 #defined declared_dependency/3.
 #defined virtual/1.
-#defined virtual_condition_holds/2.
 #defined external/1.
 #defined external_spec/2.
 #defined external_version_declared/4.
@@ -437,25 +420,15 @@ external(Package) :- attr("external_spec_selected", Package, _).
 
 % determine if an external spec has been selected
 attr("external_spec_selected", Package, LocalIndex) :-
-    external_conditions_hold(Package, LocalIndex),
+    attr("external_conditions_hold", Package, LocalIndex),
     attr("node", Package),
     not attr("hash", Package, _).
 
-external_conditions_hold(Package, LocalIndex) :-
-    possible_external(ID, Package, LocalIndex), condition_holds(ID).
-
 % it cannot happen that a spec is external, but none of the external specs
 % conditions hold.
 error(100, "Attempted to use external for '{0}' which does not satisfy any configured external spec", Package)
  :- external(Package),
-    not external_conditions_hold(Package, _).
-
-#defined possible_external/3.
-#defined external_spec_index/3.
-#defined external_spec_condition/3.
-#defined external_spec_condition/4.
-#defined external_spec_condition/5.
-#defined external_spec_condition/6.
+    not attr("external_conditions_hold", Package, _).
 
 %-----------------------------------------------------------------------------
 % Config required semantics
@@ -594,7 +567,6 @@ attr("variant_value", Package, Variant, Value) :-
     variant(Package, Variant),
     build(Package).
 
-
 error(100, "'{0}' required multiple values for single-valued variant '{1}'", Package, Variant)
   :- attr("node", Package),
      variant(Package, Variant),
@@ -665,7 +637,7 @@ variant_default_not_used(Package, Variant, Value)
 external_with_variant_set(Package, Variant, Value)
  :- attr("variant_value", Package, Variant, Value),
     condition_requirement(ID, "variant_value", Package, Variant, Value),
-    possible_external(ID, Package, _),
+    imposed_constraint(ID, "external_conditions_hold", Package, _),
     external(Package),
     attr("node", Package).
 

lib/spack/spack/solver/display.lp

@@ -23,5 +23,12 @@
 #show error/4.
 #show error/5.
 #show error/6.
+#show error/7.
+#show error/8.
+#show error/9.
+
+% show cause -> effect data for errors
+#show condition_cause/2.
+#show condition/2.
 
 % debug