error messages: condition chaining (#40173)

Create chains of causation for error messages.

The current implementation is only completed for some of the many errors presented by the concretizer. The rest will need to be filled out over time, but this demonstrates the capability.

The basic idea is to associate conditions in the solver with one another in causal relationships, and to associate errors with the proximate causes of their facts in the condition graph. Then we can construct causal trees to explain errors, which will hopefully present users with useful information to avoid the error or report issues.

Technically, this is implemented as a secondary solve. The concretizer computes the optimal model, and if the optimal model contains an error, then a secondary solve computes causation information about the error(s) in the concretizer output.

Examples:

$ spack solve hdf5 ^cmake@3.0.1
==> Error: concretization failed for the following reasons:

   1. Cannot satisfy 'cmake@3.0.1'
   2. Cannot satisfy 'cmake@3.0.1'
        required because hdf5 ^cmake@3.0.1 requested from CLI 
   3. Cannot satisfy 'cmake@3.18:' and 'cmake@3.0.1
        required because hdf5 ^cmake@3.0.1 requested from CLI 
        required because hdf5 depends on cmake@3.18: when @1.13: 
          required because hdf5 ^cmake@3.0.1 requested from CLI 
   4. Cannot satisfy 'cmake@3.12:' and 'cmake@3.0.1
        required because hdf5 depends on cmake@3.12: 
          required because hdf5 ^cmake@3.0.1 requested from CLI 
        required because hdf5 ^cmake@3.0.1 requested from CLI

$ spack spec cmake ^curl~ldap   # <-- with curl configured non-buildable and an external with `+ldap`
==> Error: concretization failed for the following reasons:

   1. Attempted to use external for 'curl' which does not satisfy any configured external spec
   2. Attempted to build package curl which is not buildable and does not have a satisfying external
        attr('variant_value', 'curl', 'ldap', 'True') is an external constraint for curl which was not satisfied
   3. Attempted to build package curl which is not buildable and does not have a satisfying external
        attr('variant_value', 'curl', 'gssapi', 'True') is an external constraint for curl which was not satisfied
   4. Attempted to build package curl which is not buildable and does not have a satisfying external
        'curl+ldap' is an external constraint for curl which was not satisfied
        'curl~ldap' required
        required because cmake ^curl~ldap requested from CLI 

$ spack solve yambo+mpi ^hdf5~mpi
==> Error: concretization failed for the following reasons:

   1. 'hdf5' required multiple values for single-valued variant 'mpi'
   2. 'hdf5' required multiple values for single-valued variant 'mpi'
    Requested '~mpi' and '+mpi'
        required because yambo depends on hdf5+mpi when +mpi 
          required because yambo+mpi ^hdf5~mpi requested from CLI 
        required because yambo+mpi ^hdf5~mpi requested from CLI 
   3. 'hdf5' required multiple values for single-valued variant 'mpi'
    Requested '~mpi' and '+mpi'
        required because netcdf-c depends on hdf5+mpi when +mpi 
          required because netcdf-fortran depends on netcdf-c 
            required because yambo depends on netcdf-fortran 
              required because yambo+mpi ^hdf5~mpi requested from CLI 
          required because netcdf-fortran depends on netcdf-c@4.7.4: when @4.5.3: 
            required because yambo depends on netcdf-fortran 
              required because yambo+mpi ^hdf5~mpi requested from CLI 
          required because yambo depends on netcdf-c 
            required because yambo+mpi ^hdf5~mpi requested from CLI 
          required because yambo depends on netcdf-c+mpi when +mpi 
            required because yambo+mpi ^hdf5~mpi requested from CLI 
        required because yambo+mpi ^hdf5~mpi requested from CLI 

Future work:

In addition to fleshing out the causes of other errors, I would like to find a way to associate different components of the error messages with different causes. In this example it's pretty easy to infer which part is which, but I'm not confident that will always be the case. 

See the previous PR #34500 for discussion of how the condition chains are incomplete. In the future, we may need custom logic for individual attributes to associate some important choice rules with conditions such that clingo choices or other derivations can be part of the explanation.

---------

Co-authored-by: Massimiliano Culpo <massimiliano.culpo@gmail.com>

6 files changed, 592 insertions, 113 deletions

diff --git a/lib/spack/spack/solver/asp.py b/lib/spack/spack/solver/asp.py
index 63e32a7576..6df9a3583e 100644
--- a/lib/spack/spack/solver/asp.py
+++ b/lib/spack/spack/solver/asp.py
@@ -8,11 +8,12 @@ import copy
 import enum
 import itertools
 import os
+import pathlib
 import pprint
 import re
 import types
 import warnings
-from typing import Dict, List, NamedTuple, Optional, Sequence, Tuple, Union
+from typing import Callable, Dict, List, NamedTuple, Optional, Sequence, Set, Tuple, Union
 
 import archspec.cpu
 
@@ -337,6 +338,13 @@ class AspFunctionBuilder:
 
 fn = AspFunctionBuilder()
 
+TransformFunction = Callable[[spack.spec.Spec, List[AspFunction]], List[AspFunction]]
+
+
+def remove_node(spec: spack.spec.Spec, facts: List[AspFunction]) -> List[AspFunction]:
+    """Transformation that removes all "node" and "virtual_node" from the input list of facts."""
+    return list(filter(lambda x: x.args[0] not in ("node", "virtual_node"), facts))
+
 
 def _create_counter(specs, tests):
     strategy = spack.config.CONFIG.get("concretizer:duplicates:strategy", "none")
@@ -684,7 +692,7 @@ def extract_args(model, predicate_name):
 class ErrorHandler:
     def __init__(self, model):
         self.model = model
-        self.error_args = extract_args(model, "error")
+        self.full_model = None
 
     def multiple_values_error(self, attribute, pkg):
         return f'Cannot select a single "{attribute}" for package "{pkg}"'
@@ -692,6 +700,48 @@ 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: Tuple[str, str],
+        conditions: Dict[str, str],
+        condition_causes: List[Tuple[Tuple[str, str], Tuple[str, str]]],
+        seen: Set,
+        indent: str = "        ",
+    ) -> List[str]:
+        """
+        Implementation of recursion for self.get_cause_tree. Much of this operates on tuples
+        (condition_id, set_id) in which the latter idea means that the condition represented by
+        the former held in the condition set represented by the latter.
+        """
+        seen = set(seen) | set(cause)
+        parents = [c for e, c in condition_causes if e == cause and c not in seen]
+        local = "required because %s " % conditions[cause[0]]
+
+        return [indent + local] + [
+            c
+            for parent in parents
+            for c in self._get_cause_tree(
+                parent, conditions, condition_causes, seen, indent=indent + "  "
+            )
+        ]
+
+    def get_cause_tree(self, cause: Tuple[str, str]) -> List[str]:
+        """
+        Get the cause tree associated with the given cause.
+
+        Arguments:
+            cause: The root cause of the tree (final condition)
+
+        Returns:
+            A list of strings describing the causes, formatted to display tree structure.
+        """
+        conditions: Dict[str, str] = dict(extract_args(self.full_model, "condition_reason"))
+        condition_causes: List[Tuple[Tuple[str, str], Tuple[str, str]]] = list(
+            ((Effect, EID), (Cause, CID))
+            for Effect, EID, Cause, CID in extract_args(self.full_model, "condition_cause")
+        )
+        return self._get_cause_tree(cause, conditions, condition_causes, set())
+
     def handle_error(self, msg, *args):
         """Handle an error state derived by the solver."""
         if msg == "multiple_values_error":
@@ -700,14 +750,31 @@ class ErrorHandler:
         if msg == "no_value_error":
             return self.no_value_error(*args)
 
+        try:
+            idx = args.index("startcauses")
+        except ValueError:
+            msg_args = args
+            causes = []
+        else:
+            msg_args = args[:idx]
+            cause_args = args[idx + 1 :]
+            cause_args_conditions = cause_args[::2]
+            cause_args_ids = cause_args[1::2]
+            causes = list(zip(cause_args_conditions, cause_args_ids))
+
+        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(causes):
+            for c in self.get_cause_tree(cause):
+                msg += f"\n{c}"
+
         return msg
 
     def message(self, errors) -> str:
@@ -719,11 +786,31 @@ class ErrorHandler:
         return "\n".join([header] + messages)
 
     def raise_if_errors(self):
-        if not self.error_args:
+        initial_error_args = extract_args(self.model, "error")
+        if not initial_error_args:
             return
 
+        error_causation = clingo.Control()
+
+        parent_dir = pathlib.Path(__file__).parent
+        errors_lp = parent_dir / "error_messages.lp"
+
+        def on_model(model):
+            self.full_model = model.symbols(shown=True, terms=True)
+
+        with error_causation.backend() as backend:
+            for atom in self.model:
+                atom_id = backend.add_atom(atom)
+                backend.add_rule([atom_id], [], choice=False)
+
+            error_causation.load(str(errors_lp))
+            error_causation.ground([("base", []), ("error_messages", [])])
+            _ = error_causation.solve(on_model=on_model)
+
+        # No choices so there will be only one model
+        error_args = extract_args(self.full_model, "error")
         errors = sorted(
-            [(int(priority), msg, args) for priority, msg, *args in self.error_args], reverse=True
+            [(int(priority), msg, args) for priority, msg, *args in error_args], reverse=True
         )
         msg = self.message(errors)
         raise UnsatisfiableSpecError(msg)
@@ -924,7 +1011,7 @@ class PyclingoDriver:
                 if sym.name not in ("attr", "error", "opt_criterion"):
                     tty.debug(
                         "UNKNOWN SYMBOL: %s(%s)"
-                        % (sym.name, ", ".join(intermediate_repr(sym.arguments)))
+                        % (sym.name, ", ".join([str(s) for s in intermediate_repr(sym.arguments)]))
                     )
 
         elif cores:
@@ -1116,7 +1203,7 @@ class SpackSolverSetup:
         default_msg = "{0}: '{1}' conflicts with '{2}'"
         no_constraint_msg = "{0}: conflicts with '{1}'"
         for trigger, constraints in pkg.conflicts.items():
-            trigger_msg = "conflict trigger %s" % str(trigger)
+            trigger_msg = f"conflict is triggered when {str(trigger)}"
             trigger_spec = spack.spec.Spec(trigger)
             trigger_id = self.condition(
                 trigger_spec, name=trigger_spec.name or pkg.name, msg=trigger_msg
@@ -1128,7 +1215,11 @@ class SpackSolverSetup:
                         conflict_msg = no_constraint_msg.format(pkg.name, trigger)
                     else:
                         conflict_msg = default_msg.format(pkg.name, trigger, constraint)
-                constraint_msg = "conflict constraint %s" % str(constraint)
+
+                spec_for_msg = (
+                    spack.spec.Spec(pkg.name) if constraint == spack.spec.Spec() else constraint
+                )
+                constraint_msg = f"conflict applies to spec {str(spec_for_msg)}"
                 constraint_id = self.condition(constraint, name=pkg.name, msg=constraint_msg)
                 self.gen.fact(
                     fn.pkg_fact(pkg.name, fn.conflict(trigger_id, constraint_id, conflict_msg))
@@ -1310,7 +1401,7 @@ class SpackSolverSetup:
         self.gen.h2("Trigger conditions")
         for name in self._trigger_cache:
             cache = self._trigger_cache[name]
-            for spec_str, (trigger_id, requirements) in cache.items():
+            for (spec_str, _), (trigger_id, requirements) in cache.items():
                 self.gen.fact(fn.pkg_fact(name, fn.trigger_id(trigger_id)))
                 self.gen.fact(fn.pkg_fact(name, fn.trigger_msg(spec_str)))
                 for predicate in requirements:
@@ -1323,7 +1414,7 @@ class SpackSolverSetup:
         self.gen.h2("Imposed requirements")
         for name in self._effect_cache:
             cache = self._effect_cache[name]
-            for spec_str, (effect_id, requirements) in cache.items():
+            for (spec_str, _), (effect_id, requirements) in cache.items():
                 self.gen.fact(fn.pkg_fact(name, fn.effect_id(effect_id)))
                 self.gen.fact(fn.pkg_fact(name, fn.effect_msg(spec_str)))
                 for predicate in requirements:
@@ -1422,18 +1513,26 @@ class SpackSolverSetup:
 
             self.gen.newline()
 
-    def condition(self, required_spec, imposed_spec=None, name=None, msg=None, node=False):
+    def condition(
+        self,
+        required_spec: spack.spec.Spec,
+        imposed_spec: Optional[spack.spec.Spec] = None,
+        name: Optional[str] = None,
+        msg: Optional[str] = None,
+        transform_required: Optional[TransformFunction] = None,
+        transform_imposed: Optional[TransformFunction] = remove_node,
+    ):
         """Generate facts for a dependency or virtual provider condition.
 
         Arguments:
-            required_spec (spack.spec.Spec): the spec that triggers this condition
-            imposed_spec (spack.spec.Spec or None): the spec with constraints that
-                are imposed when this condition is triggered
-            name (str or None): name for `required_spec` (required if
-                required_spec is anonymous, ignored if not)
-            msg (str or None): description of the condition
-            node (bool): if False does not emit "node" or "virtual_node" requirements
-                from the imposed spec
+            required_spec: the constraints that triggers this condition
+            imposed_spec: the constraints that are imposed when this condition is triggered
+            name: name for `required_spec` (required if required_spec is anonymous, ignored if not)
+            msg: description of the condition
+            transform_required: transformation applied to facts from the required spec. Defaults
+                to leave facts as they are.
+            transform_imposed: transformation applied to facts from the imposed spec. Defaults
+                to removing "node" and "virtual_node" facts.
         Returns:
             int: id of the condition created by this function
         """
@@ -1451,10 +1550,14 @@ class SpackSolverSetup:
 
         cache = self._trigger_cache[named_cond.name]
 
-        named_cond_key = str(named_cond)
+        named_cond_key = (str(named_cond), transform_required)
         if named_cond_key not in cache:
             trigger_id = next(self._trigger_id_counter)
             requirements = self.spec_clauses(named_cond, body=True, required_from=name)
+
+            if transform_required:
+                requirements = transform_required(named_cond, requirements)
+
             cache[named_cond_key] = (trigger_id, requirements)
         trigger_id, requirements = cache[named_cond_key]
         self.gen.fact(fn.pkg_fact(named_cond.name, fn.condition_trigger(condition_id, trigger_id)))
@@ -1463,14 +1566,14 @@ class SpackSolverSetup:
             return condition_id
 
         cache = self._effect_cache[named_cond.name]
-        imposed_spec_key = str(imposed_spec)
+        imposed_spec_key = (str(imposed_spec), transform_imposed)
         if imposed_spec_key not in cache:
             effect_id = next(self._effect_id_counter)
             requirements = self.spec_clauses(imposed_spec, body=False, required_from=name)
-            if not node:
-                requirements = list(
-                    filter(lambda x: x.args[0] not in ("node", "virtual_node"), requirements)
-                )
+
+            if transform_imposed:
+                requirements = transform_imposed(imposed_spec, requirements)
+
             cache[imposed_spec_key] = (effect_id, requirements)
         effect_id, requirements = cache[imposed_spec_key]
         self.gen.fact(fn.pkg_fact(named_cond.name, fn.condition_effect(condition_id, effect_id)))
@@ -1530,21 +1633,32 @@ class SpackSolverSetup:
                 if not depflag:
                     continue
 
-                msg = "%s depends on %s" % (pkg.name, dep.spec.name)
+                msg = f"{pkg.name} depends on {dep.spec}"
                 if cond != spack.spec.Spec():
-                    msg += " when %s" % cond
+                    msg += f" when {cond}"
                 else:
                     pass
 
-                condition_id = self.condition(cond, dep.spec, pkg.name, msg)
-                self.gen.fact(
-                    fn.pkg_fact(pkg.name, fn.dependency_condition(condition_id, dep.spec.name))
-                )
+                def track_dependencies(input_spec, requirements):
+                    return requirements + [fn.attr("track_dependencies", input_spec.name)]
 
-                for t in dt.ALL_FLAGS:
-                    if t & depflag:
-                        # there is a declared dependency of type t
-                        self.gen.fact(fn.dependency_type(condition_id, dt.flag_to_string(t)))
+                def dependency_holds(input_spec, requirements):
+                    return remove_node(input_spec, requirements) + [
+                        fn.attr(
+                            "dependency_holds", pkg.name, input_spec.name, dt.flag_to_string(t)
+                        )
+                        for t in dt.ALL_FLAGS
+                        if t & depflag
+                    ]
+
+                self.condition(
+                    cond,
+                    dep.spec,
+                    name=pkg.name,
+                    msg=msg,
+                    transform_required=track_dependencies,
+                    transform_imposed=dependency_holds,
+                )
 
                 self.gen.newline()
 
@@ -1639,8 +1753,17 @@ class SpackSolverSetup:
                     when_spec = spack.spec.Spec(pkg_name)
 
                 try:
+                    # With virtual we want to emit "node" and "virtual_node" in imposed specs
+                    transform: Optional[TransformFunction] = remove_node
+                    if virtual:
+                        transform = None
+
                     member_id = self.condition(
-                        required_spec=when_spec, imposed_spec=spec, name=pkg_name, node=virtual
+                        required_spec=when_spec,
+                        imposed_spec=spec,
+                        name=pkg_name,
+                        transform_imposed=transform,
+                        msg=f"{spec_str} is a requirement for package {pkg_name}",
                     )
                 except Exception as e:
                     # Do not raise if the rule comes from the 'all' subsection, since usability
@@ -1703,8 +1826,16 @@ class SpackSolverSetup:
             # Declare external conditions with a local index into packages.yaml
             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.pkg_fact(pkg_name, fn.possible_external(condition_id, local_idx)))
+
+                def external_imposition(input_spec, _):
+                    return [fn.attr("external_conditions_hold", input_spec.name, local_idx)]
+
+                self.condition(
+                    spec,
+                    spack.spec.Spec(spec.name),
+                    msg=msg,
+                    transform_imposed=external_imposition,
+                )
                 self.possible_versions[spec.name].add(spec.version)
                 self.gen.newline()
 
@@ -1918,6 +2049,7 @@ class SpackSolverSetup:
         if not body:
             for virtual in virtuals:
                 clauses.append(fn.attr("provider_set", spec.name, virtual))
+                clauses.append(fn.attr("virtual_node", virtual))
         else:
             for virtual in virtuals:
                 clauses.append(fn.attr("virtual_on_incoming_edges", spec.name, virtual))
@@ -2555,20 +2687,45 @@ class SpackSolverSetup:
         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))
+            condition_id = next(self._condition_id_counter)
+            trigger_id = next(self._trigger_id_counter)
 
-            self.gen.fact(fn.literal(idx, "virtual_root" if spec.virtual else "root", spec.name))
-            for clause in self.spec_clauses(spec):
-                self.gen.fact(fn.literal(idx, *clause.args))
-                if clause.args[0] == "variant_set":
-                    self.gen.fact(
-                        fn.literal(idx, "variant_default_value_from_cli", *clause.args[1:])
+            # Special condition triggered by "literal_solved"
+            self.gen.fact(fn.literal(trigger_id))
+            self.gen.fact(fn.pkg_fact(spec.name, fn.condition_trigger(condition_id, trigger_id)))
+            self.gen.fact(fn.condition_reason(condition_id, f"{spec} requested from CLI"))
+
+            # Effect imposes the spec
+            imposed_spec_key = str(spec), None
+            cache = self._effect_cache[spec.name]
+            msg = (
+                "literal specs have different requirements. clear cache before computing literals"
+            )
+            assert imposed_spec_key not in cache, msg
+            effect_id = next(self._effect_id_counter)
+            requirements = self.spec_clauses(spec)
+            root_name = spec.name
+            for clause in requirements:
+                clause_name = clause.args[0]
+                if clause_name == "variant_set":
+                    requirements.append(
+                        fn.attr("variant_default_value_from_cli", *clause.args[1:])
                     )
+                elif clause_name in ("node", "virtual_node", "hash"):
+                    # These facts are needed to compute the "condition_set" of the root
+                    pkg_name = clause.args[1]
+                    self.gen.fact(fn.mentioned_in_literal(trigger_id, root_name, pkg_name))
+
+            requirements.append(fn.attr("virtual_root" if spec.virtual else "root", spec.name))
+            cache[imposed_spec_key] = (effect_id, requirements)
+            self.gen.fact(fn.pkg_fact(spec.name, fn.condition_effect(condition_id, effect_id)))
 
             if self.concretize_everything:
-                self.gen.fact(fn.solve_literal(idx))
+                self.gen.fact(fn.solve_literal(trigger_id))
+
+        self.effect_rules()
 
     def validate_and_define_versions_from_requirements(
         self, *, allow_deprecated: bool, require_checksum: bool
diff --git a/lib/spack/spack/solver/concretize.lp b/lib/spack/spack/solver/concretize.lp
index 340e1b04ee..0b2b83dc20 100644
--- a/lib/spack/spack/solver/concretize.lp
+++ b/lib/spack/spack/solver/concretize.lp
@@ -10,9 +10,8 @@
 % ID of the nodes in the "root" link-run sub-DAG
 #const min_dupe_id = 0.
 
-#const link_run = 0.
-#const direct_link_run =1.
-#const direct_build = 2.
+#const direct_link_run = 0.
+#const direct_build = 1.
 
 % Allow clingo to create nodes
 { attr("node", node(0..X-1, Package))         } :- max_dupes(Package, X), not virtual(Package).
@@ -30,23 +29,21 @@
 :- attr("variant_value", PackageNode, _, _), not attr("node", PackageNode).
 :- attr("node_flag_compiler_default", PackageNode), not attr("node", PackageNode).
 :- attr("node_flag", PackageNode, _, _), not attr("node", PackageNode).
-:- attr("node_flag_source", PackageNode, _, _), not attr("node", PackageNode).
 :- attr("no_flags", PackageNode, _), not attr("node", PackageNode).
 :- attr("external_spec_selected", PackageNode, _), not attr("node", PackageNode).
 :- attr("depends_on", ParentNode, _, _), not attr("node", ParentNode).
 :- attr("depends_on", _, ChildNode, _), not attr("node", ChildNode).
 :- attr("node_flag_source", ParentNode, _, _), not attr("node", ParentNode).
 :- attr("node_flag_source", _, _, ChildNode), not attr("node", ChildNode).
+:- attr("virtual_node", VirtualNode), not provider(_, VirtualNode), internal_error("virtual node with no provider").
+:- provider(_, VirtualNode), not attr("virtual_node", VirtualNode), internal_error("provider with no virtual node").
+:- provider(PackageNode, _), not attr("node", PackageNode), internal_error("provider with no real node").
 
-:- attr("virtual_node", VirtualNode), not provider(_, VirtualNode).
-:- provider(_, VirtualNode), not attr("virtual_node", VirtualNode).
-:- provider(PackageNode, _), not attr("node", PackageNode).
-
-:- attr("root", node(ID, PackageNode)), ID > min_dupe_id.
+:- attr("root", node(ID, PackageNode)), ID > min_dupe_id, internal_error("root with a non-minimal duplicate ID").
 
 % Nodes in the "root" unification set cannot depend on non-root nodes if the dependency is "link" or "run"
-:- attr("depends_on", node(min_dupe_id, Package), node(ID, _), "link"), ID != min_dupe_id, unification_set("root", node(min_dupe_id, Package)).
-:- attr("depends_on", node(min_dupe_id, Package), node(ID, _), "run"),  ID != min_dupe_id, unification_set("root", node(min_dupe_id, Package)).
+:- attr("depends_on", node(min_dupe_id, Package), node(ID, _), "link"), ID != min_dupe_id, unification_set("root", node(min_dupe_id, Package)), internal_error("link dependency out of the root unification set").
+:- attr("depends_on", node(min_dupe_id, Package), node(ID, _), "run"),  ID != min_dupe_id, unification_set("root", node(min_dupe_id, Package)), internal_error("run dependency out of the root unification set").
 
 % Rules on "unification sets", i.e. on sets of nodes allowing a single configuration of any given package
 unify(SetID, PackageName) :- unification_set(SetID, node(_, PackageName)).
@@ -86,22 +83,24 @@ unification_set(SetID, VirtualNode)
 %----
 
 % In the "root" unification set only ID = 0 are allowed
-:- unification_set("root", node(ID, _)), ID != 0.
+:- unification_set("root", node(ID, _)), ID != 0, internal_error("root unification set has node with non-zero unification set ID").
 
 % In the "root" unification set we allow only packages from the link-run possible subDAG
-:- unification_set("root", node(_, Package)), not possible_in_link_run(Package), not virtual(Package).
+:- unification_set("root", node(_, Package)), not possible_in_link_run(Package), not virtual(Package), internal_error("package outside possible link/run graph in root unification set").
 
 % Each node must belong to at least one unification set
-:- attr("node", PackageNode), not unification_set(_, PackageNode).
+:- attr("node", PackageNode), not unification_set(_, PackageNode), internal_error("node belongs to no unification set").
 
 % Cannot have a node with an ID, if lower ID of the same package are not used
 :- attr("node", node(ID1, Package)),
    not attr("node", node(ID2, Package)),
-   max_dupes(Package, X), ID1=0..X-1, ID2=0..X-1, ID2 < ID1.
+   max_dupes(Package, X), ID1=0..X-1, ID2=0..X-1, ID2 < ID1,
+   internal_error("node skipped id number").
 
 :- attr("virtual_node", node(ID1, Package)),
    not attr("virtual_node", node(ID2, Package)),
-   max_dupes(Package, X), ID1=0..X-1, ID2=0..X-1, ID2 < ID1.
+   max_dupes(Package, X), ID1=0..X-1, ID2=0..X-1, ID2 < ID1,
+   internal_error("virtual node skipped id number").
 
 %-----------------------------------------------------------------------------
 % Map literal input specs to facts that drive the solve
@@ -115,29 +114,28 @@ multiple_nodes_attribute("depends_on").
 multiple_nodes_attribute("virtual_on_edge").
 multiple_nodes_attribute("provider_set").
 
-% Map constraint on the literal ID to facts on the node
-attr(Name, node(min_dupe_id, A1))             :- literal(LiteralID, Name, A1), solve_literal(LiteralID).
-attr(Name, node(min_dupe_id, A1), A2)         :- literal(LiteralID, Name, A1, A2), solve_literal(LiteralID), not multiple_nodes_attribute(Name).
-attr(Name, node(min_dupe_id, A1), A2, A3)     :- literal(LiteralID, Name, A1, A2, A3), solve_literal(LiteralID), not multiple_nodes_attribute(Name).
-attr(Name, node(min_dupe_id, A1), A2, A3, A4) :- literal(LiteralID, Name, A1, A2, A3, A4), solve_literal(LiteralID).
+trigger_condition_holds(TriggerID, node(min_dupe_id, Package)) :-
+  solve_literal(TriggerID),
+  pkg_fact(Package, condition_trigger(_, TriggerID)),
+  literal(TriggerID).
 
-% Special cases where nodes occur in arguments other than A1
-attr("node_flag_source", node(min_dupe_id, A1), A2, node(min_dupe_id, A3)) :- literal(LiteralID, "node_flag_source", A1, A2, A3), solve_literal(LiteralID).
-attr("depends_on",       node(min_dupe_id, A1), node(min_dupe_id, A2), A3) :- literal(LiteralID, "depends_on",       A1, A2, A3), solve_literal(LiteralID).
+trigger_node(TriggerID, Node, Node) :-
+  trigger_condition_holds(TriggerID, Node),
+  literal(TriggerID).
 
-attr("virtual_node", node(min_dupe_id, Virtual))                              :- literal(LiteralID, "provider_set", _,        Virtual), solve_literal(LiteralID).
-attr("provider_set", node(min_dupe_id, Provider), node(min_dupe_id, Virtual)) :- literal(LiteralID, "provider_set", Provider, Virtual), solve_literal(LiteralID).
-provider(node(min_dupe_id, Provider), node(min_dupe_id, Virtual))             :- literal(LiteralID, "provider_set", Provider, Virtual), solve_literal(LiteralID).
+% Since we trigger the existence of literal nodes from a condition, we need to construct
+% the condition_set/2 manually below
+mentioned_in_literal(Root, Mentioned) :- mentioned_in_literal(TriggerID, Root, Mentioned), solve_literal(TriggerID).
+condition_set(node(min_dupe_id, Root), node(min_dupe_id, Mentioned)) :-  mentioned_in_literal(Root, Mentioned).
 
 % Discriminate between "roots" that have been explicitly requested, and roots that are deduced from "virtual roots"
-explicitly_requested_root(node(min_dupe_id, A1)) :- literal(LiteralID, "root", A1), solve_literal(LiteralID).
+explicitly_requested_root(node(min_dupe_id, Package)) :-
+  solve_literal(TriggerID),
+  trigger_and_effect(Package, TriggerID, EffectID),
+  imposed_constraint(EffectID, "root", Package).
 
 #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").
@@ -235,7 +233,8 @@ possible_version_weight(node(ID, Package), Weight)
 
 1 { version_weight(node(ID, Package), Weight) : pkg_fact(Package, version_declared(Version, Weight)) } 1
   :- attr("version", node(ID, Package), Version),
-     attr("node", node(ID, Package)).
+     attr("node", node(ID, Package)),
+     internal_error("version weights must exist and be unique").
 
 % node_version_satisfies implies that exactly one of the satisfying versions
 % is the package's version, and vice versa.
@@ -249,7 +248,8 @@ possible_version_weight(node(ID, Package), Weight)
 % bound on the choice rule to avoid false positives with the error below
 1 { attr("version", node(ID, Package), Version) : pkg_fact(Package, version_satisfies(Constraint, Version)) }
   :- attr("node_version_satisfies", node(ID, Package), Constraint),
-     pkg_fact(Package, version_satisfies(Constraint, _)).
+     pkg_fact(Package, version_satisfies(Constraint, _)),
+     internal_error("must choose a single version to satisfy version constraints").
 
 % More specific error message if the version cannot satisfy some constraint
 % Otherwise covered by `no_version_error` and `versions_conflict_error`.
@@ -362,7 +362,7 @@ imposed_nodes(ConditionID, PackageNode, node(X, A1))
 
 % Conditions that hold impose may impose constraints on other specs
 attr(Name, node(X, A1))             :- impose(ID, PackageNode), imposed_constraint(ID, Name, A1),             imposed_nodes(ID, PackageNode, node(X, A1)).
-attr(Name, node(X, A1), A2)         :- impose(ID, PackageNode), imposed_constraint(ID, Name, A1, A2),         imposed_nodes(ID, PackageNode, node(X, A1)).
+attr(Name, node(X, A1), A2)         :- impose(ID, PackageNode), imposed_constraint(ID, Name, A1, A2),         imposed_nodes(ID, PackageNode, node(X, A1)), not multiple_nodes_attribute(Name).
 attr(Name, node(X, A1), A2, A3)     :- impose(ID, PackageNode), imposed_constraint(ID, Name, A1, A2, A3),     imposed_nodes(ID, PackageNode, node(X, A1)), not multiple_nodes_attribute(Name).
 attr(Name, node(X, A1), A2, A3, A4) :- impose(ID, PackageNode), imposed_constraint(ID, Name, A1, A2, A3, A4), imposed_nodes(ID, PackageNode, node(X, A1)).
 
@@ -373,6 +373,16 @@ attr("node_flag_source", node(X, A1), A2, node(Y, A3))
      imposed_constraint(ID, "node_flag_source", A1, A2, A3),
      condition_set(node(Y, A3), node(X, A1)).
 
+% Provider set is relevant only for literals, since it's the only place where `^[virtuals=foo] bar`
+% might appear in the HEAD of a rule
+attr("provider_set", node(min_dupe_id, Provider), node(min_dupe_id, Virtual))
+  :- solve_literal(TriggerID),
+     trigger_and_effect(_, TriggerID, EffectID),
+     impose(EffectID, _),
+     imposed_constraint(EffectID, "provider_set", Provider, Virtual).
+
+provider(ProviderNode, VirtualNode) :- attr("provider_set", ProviderNode, VirtualNode).
+
 % Here we can't use the condition set because it's a recursive definition, that doesn't define the
 % node index, and leads to unsatisfiability. Hence we say that one and only one node index must
 % satisfy the dependency.
@@ -432,24 +442,11 @@ depends_on(PackageNode, DependencyNode) :- attr("depends_on", PackageNode, Depen
 % 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(node(NodeID, Package), Dependency, Type) :-
-  pkg_fact(Package, dependency_condition(ID, Dependency)),
-  dependency_type(ID, Type),
-  build(node(NodeID, Package)),
-  not external(node(NodeID, Package)),
-  condition_holds(ID, node(NodeID, Package)).
-
-% 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(EffectID, node(NodeID, Package)) :-
-  not dependency_holds(node(NodeID, Package), Dependency, _),
-  attr("node", node(NodeID, Package)),
-  pkg_fact(Package, dependency_condition(ID, Dependency)),
-  pkg_fact(Package, condition_effect(ID, EffectID)).
+attr("track_dependencies", Node) :- build(Node), not external(Node).
 
 % If a dependency holds on a package node, there must be one and only one dependency node satisfying it
 1 { attr("depends_on", PackageNode, node(0..Y-1, Dependency), Type) : max_dupes(Dependency, Y) } 1
-  :- dependency_holds(PackageNode, Dependency, Type),
+  :- attr("dependency_holds", PackageNode, Dependency, Type),
      not virtual(Dependency).
 
 % all nodes in the graph must be reachable from some root
@@ -499,7 +496,7 @@ error(100, "Package '{0}' needs to provide both '{1}' and '{2}' together, but pr
 % 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
 node_depends_on_virtual(PackageNode, Virtual, Type)
-  :- dependency_holds(PackageNode, Virtual, Type),
+  :- attr("dependency_holds", PackageNode, Virtual, Type),
      virtual(Virtual),
      not external(PackageNode).
 
@@ -509,7 +506,7 @@ node_depends_on_virtual(PackageNode, Virtual) :- node_depends_on_virtual(Package
   :- node_depends_on_virtual(PackageNode, Virtual, Type).
 
 attr("virtual_on_edge", PackageNode, ProviderNode, Virtual)
-  :- dependency_holds(PackageNode, Virtual, Type),
+  :- attr("dependency_holds", PackageNode, Virtual, Type),
      attr("depends_on", PackageNode, ProviderNode, Type),
      provider(ProviderNode, node(_, Virtual)),
      not external(PackageNode).
@@ -624,11 +621,11 @@ possible_provider_weight(node(DependencyID, Dependency), VirtualNode, 100, "fall
     pkg_fact(Package, version_declared(Version, Weight, "external")) }
     :- external(node(ID, Package)).
 
-error(100, "Attempted to use external for '{0}' which does not satisfy any configured external spec", Package)
+error(100, "Attempted to use external for '{0}' which does not satisfy any configured external spec version", Package)
   :- external(node(ID, Package)),
      not external_version(node(ID, Package), _, _).
 
-error(100, "Attempted to use external for '{0}' which does not satisfy any configured external spec", Package)
+error(100, "Attempted to use external for '{0}' which does not satisfy a unique configured external spec version", Package)
   :- external(node(ID, Package)),
      2 { external_version(node(ID, Package), Version, Weight) }.
 
@@ -657,18 +654,15 @@ external(PackageNode) :- attr("external_spec_selected", PackageNode, _).
 
 % determine if an external spec has been selected
 attr("external_spec_selected", node(ID, Package), LocalIndex) :-
-    external_conditions_hold(node(ID, Package), LocalIndex),
+    attr("external_conditions_hold", node(ID, Package), LocalIndex),
     attr("node", node(ID, Package)),
     not attr("hash", node(ID, Package), _).
 
-external_conditions_hold(node(PackageID, Package), LocalIndex) :-
-    pkg_fact(Package, possible_external(ID, LocalIndex)), condition_holds(ID, node(PackageID, Package)).
-
 % 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(node(ID, Package)),
-    not external_conditions_hold(node(ID, Package), _).
+    not attr("external_conditions_hold", node(ID, Package), _).
 
 %-----------------------------------------------------------------------------
 % Config required semantics
@@ -887,8 +881,9 @@ variant_default_not_used(node(ID, Package), Variant, Value)
 % The variant is set in an external spec
 external_with_variant_set(node(NodeID, Package), Variant, Value)
  :- attr("variant_value", node(NodeID, Package), Variant, Value),
-    condition_requirement(ID, "variant_value", Package, Variant, Value),
-    pkg_fact(Package, possible_external(ID, _)),
+    condition_requirement(TriggerID, "variant_value", Package, Variant, Value),
+    trigger_and_effect(Package, TriggerID, EffectID),
+    imposed_constraint(EffectID, "external_conditions_hold", Package, _),
     external(node(NodeID, Package)),
     attr("node", node(NodeID, Package)).
 
diff --git a/lib/spack/spack/solver/display.lp b/lib/spack/spack/solver/display.lp
index fffffb2c04..58d04d42ea 100644
--- a/lib/spack/spack/solver/display.lp
+++ b/lib/spack/spack/solver/display.lp
@@ -24,4 +24,29 @@
 #show error/5.
 #show error/6.
 
+% for error causation
+#show condition_reason/2.
+
+% For error messages to use later
+#show pkg_fact/2.
+#show condition_holds/2.
+#show imposed_constraint/3.
+#show imposed_constraint/4.
+#show imposed_constraint/5.
+#show imposed_constraint/6.
+#show condition_requirement/3.
+#show condition_requirement/4.
+#show condition_requirement/5.
+#show condition_requirement/6.
+#show node_has_variant/2.
+#show build/1.
+#show external/1.
+#show external_version/3.
+#show trigger_and_effect/3.
+#show unification_set/2.
+#show provider/2.
+#show condition_nodes/3.
+#show trigger_node/3.
+#show imposed_nodes/3.
+
 % debug
diff --git a/lib/spack/spack/solver/error_messages.lp b/lib/spack/spack/solver/error_messages.lp
new file mode 100644
index 0000000000..7eb383860d
--- /dev/null
+++ b/lib/spack/spack/solver/error_messages.lp
@@ -0,0 +1,239 @@
+% Copyright 2013-2023 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)
+
+%=============================================================================
+% This logic program adds detailed error messages to Spack's concretizer
+%=============================================================================
+
+#program error_messages.
+
+% Create a causal tree between trigger conditions by locating the effect conditions
+% that are triggers for another condition. Condition2 is caused by Condition1
+condition_cause(Condition2, ID2, Condition1, ID1) :-
+  condition_holds(Condition2, node(ID2, Package2)),
+  pkg_fact(Package2, condition_trigger(Condition2, Trigger)),
+  condition_requirement(Trigger, Name, Package),
+  condition_nodes(Trigger, TriggerNode, node(ID, Package)),
+  trigger_node(Trigger, TriggerNode, node(ID2, Package2)),
+  attr(Name, node(ID, Package)),
+  condition_holds(Condition1, node(ID1, Package1)),
+  pkg_fact(Package1, condition_effect(Condition1, Effect)),
+  imposed_constraint(Effect, Name, Package),
+  imposed_nodes(Effect, node(ID1, Package1), node(ID, Package)).
+
+condition_cause(Condition2, ID2, Condition1, ID1) :-
+  condition_holds(Condition2, node(ID2, Package2)),
+  pkg_fact(Package2, condition_trigger(Condition2, Trigger)),
+  condition_requirement(Trigger, Name, Package, A1),
+  condition_nodes(Trigger, TriggerNode, node(ID, Package)),
+  trigger_node(Trigger, TriggerNode, node(ID2, Package2)),
+  attr(Name, node(ID, Package), A1),
+  condition_holds(Condition1, node(ID1, Package1)),
+  pkg_fact(Package1, condition_effect(Condition1, Effect)),
+  imposed_constraint(Effect, Name, Package, A1),
+  imposed_nodes(Effect, node(ID1, Package1), node(ID, Package)).
+
+condition_cause(Condition2, ID2, Condition1, ID1) :-
+  condition_holds(Condition2, node(ID2, Package2)),
+  pkg_fact(Package2, condition_trigger(Condition2, Trigger)),
+  condition_requirement(Trigger, Name, Package, A1, A2),
+  condition_nodes(Trigger, TriggerNode, node(ID, Package)),
+  trigger_node(Trigger, TriggerNode, node(ID2, Package2)),
+  attr(Name, node(ID, Package), A1, A2),
+  condition_holds(Condition1, node(ID1, Package1)),
+  pkg_fact(Package1, condition_effect(Condition1, Effect)),
+  imposed_constraint(Effect, Name, Package, A1, A2),
+  imposed_nodes(Effect, node(ID1, Package1), node(ID, Package)).
+
+condition_cause(Condition2, ID2, Condition1, ID1) :-
+  condition_holds(Condition2, node(ID2, Package2)),
+  pkg_fact(Package2, condition_trigger(Condition2, Trigger)),
+  condition_requirement(Trigger, Name, Package, A1, A2, A3),
+  condition_nodes(Trigger, TriggerNode, node(ID, Package)),
+  trigger_node(Trigger, TriggerNode, node(ID2, Package2)),
+  attr(Name, node(ID, Package), A1, A2, A3),
+  condition_holds(Condition1, node(ID1, Package1)),
+  pkg_fact(Package1, condition_effect(Condition1, Effect)),
+  imposed_constraint(Effect, Name, Package, A1, A2, A3),
+  imposed_nodes(Effect, node(ID1, Package1), node(ID, Package)).
+
+% special condition cause for dependency conditions
+% we can't simply impose the existence of the node for dependency conditions
+% because we need to allow for the choice of which dupe ID the node gets
+condition_cause(Condition2, ID2, Condition1, ID1) :-
+  condition_holds(Condition2, node(ID2, Package2)),
+  pkg_fact(Package2, condition_trigger(Condition2, Trigger)),
+  condition_requirement(Trigger, "node", Package),
+  condition_nodes(Trigger, TriggerNode, node(ID, Package)),
+  trigger_node(Trigger, TriggerNode, node(ID2, Package2)),
+  attr("node", node(ID, Package)),
+  condition_holds(Condition1, node(ID1, Package1)),
+  pkg_fact(Package1, condition_effect(Condition1, Effect)),
+  imposed_constraint(Effect, "dependency_holds", Parent, Package, Type),
+  imposed_nodes(Effect, node(ID1, Package1), node(ID, Package)),
+  attr("depends_on", node(X, Parent), node(ID, Package), Type).
+
+% The literal startcauses is used to separate the variables that are part of the error from the
+% ones describing the causal tree of the error. After startcauses, each successive pair must be
+% a condition and a condition_set id for which it holds.
+
+% More specific error message if the version cannot satisfy some constraint
+% Otherwise covered by `no_version_error` and `versions_conflict_error`.
+error(1, "Cannot satisfy '{0}@{1}'", Package, Constraint, startcauses, ConstraintCause, CauseID)
+  :- attr("node_version_satisfies", node(ID, Package), Constraint),
+     pkg_fact(TriggerPkg, condition_effect(ConstraintCause, EffectID)),
+     imposed_constraint(EffectID, "node_version_satisfies", Package, Constraint),
+     condition_holds(ConstraintCause, node(CauseID, TriggerPkg)),
+     attr("version", node(ID, Package), Version),
+     not pkg_fact(Package, version_satisfies(Constraint, Version)).
+
+error(0, "Cannot satisfy '{0}@{1}' and '{0}@{2}", Package, Constraint1, Constraint2, startcauses, Cause1, C1ID, Cause2, C2ID)
+  :- attr("node_version_satisfies", node(ID, Package), Constraint1),
+     pkg_fact(TriggerPkg1, condition_effect(Cause1, EffectID1)),
+     imposed_constraint(EffectID1, "node_version_satisfies", Package, Constraint1),
+     condition_holds(Cause1, node(C1ID, TriggerPkg1)),
+     % two constraints
+     attr("node_version_satisfies", node(ID, Package), Constraint2),
+     pkg_fact(TriggerPkg2, condition_effect(Cause2, EffectID2)),
+     imposed_constraint(EffectID2, "node_version_satisfies", Package, Constraint2),
+     condition_holds(Cause2, node(C2ID, TriggerPkg2)),
+     % version chosen
+     attr("version", node(ID, Package), Version),
+     % version satisfies one but not the other
+     pkg_fact(Package, version_satisfies(Constraint1, Version)),
+     not pkg_fact(Package, version_satisfies(Constraint2, Version)).
+
+% causation tracking error for no or multiple virtual providers
+error(0, "Cannot find a valid provider for virtual {0}", Virtual, startcauses, Cause, CID)
+  :- attr("virtual_node", node(X, Virtual)),
+     not provider(_, node(X, Virtual)),
+     imposed_constraint(EID, "dependency_holds", Parent, Virtual, Type),
+     pkg_fact(TriggerPkg, condition_effect(Cause, EID)),
+     condition_holds(Cause, node(CID, TriggerPkg)).
+
+
+% At most one variant value 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, X, Cause2, X)
+  :- attr("node", node(X, Package)),
+     node_has_variant(node(X, Package), Variant),
+     pkg_fact(Package, variant_single_value(Variant)),
+     build(node(X, Package)),
+     attr("variant_value", node(X, Package), Variant, Value1),
+     imposed_constraint(EID1, "variant_set", Package, Variant, Value1),
+     pkg_fact(TriggerPkg1, condition_effect(Cause1, EID1)),
+     condition_holds(Cause1, node(X, TriggerPkg1)),
+     attr("variant_value", node(X, Package), Variant, Value2),
+     imposed_constraint(EID2, "variant_set", Package, Variant, Value2),
+     pkg_fact(TriggerPkg2, condition_effect(Cause2, EID2)),
+     condition_holds(Cause2, node(X, TriggerPkg2)),
+     Value1 < Value2. % see[1] in concretize.lp
+
+% Externals have to specify external conditions
+error(0, "Attempted to use external for {0} which does not satisfy any configured external spec version", Package, startcauses, ExternalCause, CID)
+  :- external(node(ID, Package)),
+     attr("external_spec_selected", node(ID, Package), Index),
+     imposed_constraint(EID, "external_conditions_hold", Package, Index),
+     pkg_fact(TriggerPkg, condition_effect(ExternalCause, EID)),
+     condition_holds(ExternalCause, node(CID, TriggerPkg)),
+     not external_version(node(ID, Package), _, _).
+
+error(0, "Attempted to build package {0} which is not buildable and does not have a satisfying external\n        attr('{1}', '{2}') is an external constraint for {0} which was not satisfied", Package, Name, A1)
+  :- external(node(ID, Package)),
+     not attr("external_conditions_hold", node(ID, Package), _),
+     imposed_constraint(EID, "external_conditions_hold", Package, _),
+     trigger_and_effect(Package, TID, EID),
+     condition_requirement(TID, Name, A1),
+     not attr(Name, node(_, A1)).
+
+error(0, "Attempted to build package {0} which is not buildable and does not have a satisfying external\n        attr('{1}', '{2}', '{3}') is an external constraint for {0} which was not satisfied", Package, Name, A1, A2)
+  :- external(node(ID, Package)),
+     not attr("external_conditions_hold", node(ID, Package), _),
+     imposed_constraint(EID, "external_conditions_hold", Package, _),
+     trigger_and_effect(Package, TID, EID),
+     condition_requirement(TID, Name, A1, A2),
+     not attr(Name, node(_, A1), A2).
+
+error(0, "Attempted to build package {0} which is not buildable and does not have a satisfying external\n        attr('{1}', '{2}', '{3}', '{4}') is an external constraint for {0} which was not satisfied", Package, Name, A1, A2, A3)
+  :- external(node(ID, Package)),
+     not attr("external_conditions_hold", node(ID, Package), _),
+     imposed_constraint(EID, "external_conditions_hold", Package, _),
+     trigger_and_effect(Package, TID, EID),
+     condition_requirement(TID, Name, A1, A2, A3),
+     not attr(Name, node(_, A1), A2, A3).
+
+error(0, "Attempted to build package {0} which is not buildable and does not have a satisfying external\n        'Spec({0} {1}={2})' is an external constraint for {0} which was not satisfied\n        'Spec({0} {1}={3})' required", Package, Variant, Value, OtherValue, startcauses, OtherValueCause, CID)
+  :- external(node(ID, Package)),
+     not attr("external_conditions_hold", node(ID, Package), _),
+     imposed_constraint(EID, "external_conditions_hold", Package, _),
+     trigger_and_effect(Package, TID, EID),
+     condition_requirement(TID, "variant_value", Package, Variant, Value),
+     not attr("variant_value", node(ID, Package), Variant, Value),
+     attr("variant_value", node(ID, Package), Variant, OtherValue),
+     imposed_constraint(EID2, "variant_set", Package, Variant, OtherValue),
+     pkg_fact(TriggerPkg, condition_effect(OtherValueCause, EID2)),
+     condition_holds(OtherValueCause, node(CID, TriggerPkg)).
+
+error(0, "Attempted to build package {0} which is not buildable and does not have a satisfying external\n        attr('{1}', '{2}', '{3}', '{4}', '{5}') is an external constraint for {0} which was not satisfied", Package, Name, A1, A2, A3, A4)
+  :- external(node(ID, Package)),
+     not attr("external_conditions_hold", node(ID, Package), _),
+     imposed_constraint(EID, "external_conditions_hold", Package, _),
+     trigger_and_effect(Package, TID, EID),
+     condition_requirement(TID, Name, A1, A2, A3, A4),
+     not attr(Name, node(_, A1), A2, A3, A4).
+
+% error message with causes for conflicts
+error(0, Msg, startcauses, TriggerID, ID1, ConstraintID, ID2)
+  :- attr("node", node(ID, Package)),
+     pkg_fact(Package, conflict(TriggerID, ConstraintID, Msg)),
+     % node(ID1, TriggerPackage) is node(ID2, Package) in most, but not all, cases
+     condition_holds(TriggerID, node(ID1, TriggerPackage)),
+     condition_holds(ConstraintID, node(ID2, Package)),
+     unification_set(X, node(ID2, Package)),
+     unification_set(X, node(ID1, TriggerPackage)),
+     not external(node(ID, Package)),  % ignore conflicts for externals
+     not attr("hash", node(ID, Package), _).  % ignore conflicts for installed packages
+
+% variables to show
+#show error/2.
+#show error/3.
+#show error/4.
+#show error/5.
+#show error/6.
+#show error/7.
+#show error/8.
+#show error/9.
+#show error/10.
+#show error/11.
+
+#show condition_cause/4.
+#show condition_reason/2.
+
+% Define all variables used to avoid warnings at runtime when the model doesn't happen to have one
+#defined error/2.
+#defined error/3.
+#defined error/4.
+#defined error/5.
+#defined error/6.
+#defined attr/2.
+#defined attr/3.
+#defined attr/4.
+#defined attr/5.
+#defined pkg_fact/2.
+#defined imposed_constraint/3.
+#defined imposed_constraint/4.
+#defined imposed_constraint/5.
+#defined imposed_constraint/6.
+#defined condition_requirement/3.
+#defined condition_requirement/4.
+#defined condition_requirement/5.
+#defined condition_requirement/6.
+#defined condition_holds/2.
+#defined unification_set/2.
+#defined external/1.
+#defined trigger_and_effect/3.
+#defined build/1.
+#defined node_has_variant/2.
+#defined provider/2.
+#defined external_version/3.
diff --git a/lib/spack/spack/solver/heuristic.lp b/lib/spack/spack/solver/heuristic.lp
index 69f925180f..745ea4f962 100644
--- a/lib/spack/spack/solver/heuristic.lp
+++ b/lib/spack/spack/solver/heuristic.lp
@@ -11,10 +11,6 @@
 %-----------------
 % Domain heuristic
 %-----------------
-#heuristic attr("hash", node(0, Package), Hash) : literal(_, "root", Package). [45, init]
-#heuristic attr("root", node(0, Package)) : literal(_, "root", Package). [45, true]
-#heuristic attr("node", node(0, Package)) : literal(_, "root", Package). [45, true]
-#heuristic attr("node", node(0, Package)) : literal(_, "node", Package). [45, true]
 
 % Root node
 #heuristic attr("version", node(0, Package), Version) : pkg_fact(Package, version_declared(Version, 0)), attr("root", node(0, Package)). [35, true]
@@ -26,4 +22,3 @@
 
 % Providers
 #heuristic attr("node", node(0, Package)) : default_provider_preference(Virtual, Package, 0), possible_in_link_run(Package). [30, true]
-
diff --git a/lib/spack/spack/test/concretize_errors.py b/lib/spack/spack/test/concretize_errors.py
new file mode 100644
index 0000000000..2a8be3e045
--- /dev/null
+++ b/lib/spack/spack/test/concretize_errors.py
@@ -0,0 +1,68 @@
+# Copyright 2013-2023 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)
+
+import pytest
+
+import spack.solver.asp
+import spack.spec
+
+pytestmark = [
+    pytest.mark.not_on_windows("Windows uses old concretizer"),
+    pytest.mark.only_clingo("Original concretizer does not support configuration requirements"),
+]
+
+version_error_messages = [
+    "Cannot satisfy 'fftw@:1.0' and 'fftw@1.1:",
+    "        required because quantum-espresso depends on fftw@:1.0",
+    "          required because quantum-espresso ^fftw@1.1: requested from CLI",
+    "        required because quantum-espresso ^fftw@1.1: requested from CLI",
+]
+
+external_error_messages = [
+    (
+        "Attempted to build package quantum-espresso which is not buildable and does not have"
+        " a satisfying external"
+    ),
+    (
+        "        'quantum-espresso~veritas' is an external constraint for quantum-espresso"
+        " which was not satisfied"
+    ),
+    "        'quantum-espresso+veritas' required",
+    "        required because quantum-espresso+veritas requested from CLI",
+]
+
+variant_error_messages = [
+    "'fftw' required multiple values for single-valued variant 'mpi'",
+    "    Requested '~mpi' and '+mpi'",
+    "        required because quantum-espresso depends on fftw+mpi when +invino",
+    "          required because quantum-espresso+invino ^fftw~mpi requested from CLI",
+    "        required because quantum-espresso+invino ^fftw~mpi requested from CLI",
+]
+
+external_config = {
+    "packages:quantum-espresso": {
+        "buildable": False,
+        "externals": [{"spec": "quantum-espresso@1.0~veritas", "prefix": "/path/to/qe"}],
+    }
+}
+
+
+@pytest.mark.parametrize(
+    "error_messages,config_set,spec",
+    [
+        (version_error_messages, {}, "quantum-espresso^fftw@1.1:"),
+        (external_error_messages, external_config, "quantum-espresso+veritas"),
+        (variant_error_messages, {}, "quantum-espresso+invino^fftw~mpi"),
+    ],
+)
+def test_error_messages(error_messages, config_set, spec, mock_packages, mutable_config):
+    for path, conf in config_set.items():
+        spack.config.set(path, conf)
+
+    with pytest.raises(spack.solver.asp.UnsatisfiableSpecError) as e:
+        _ = spack.spec.Spec(spec).concretized()
+
+    for em in error_messages:
+        assert em in str(e.value)