Add option to minimize full debug cores. include warning message about performance (#27970)

Co-authored-by: Harmen Stoppels <harmenstoppels@gmail.com>
This commit is contained in:
Greg Becker 2021-12-14 23:52:53 -08:00 committed by Massimiliano Culpo
parent adf4e91658
commit 9345bf81b9
5 changed files with 74 additions and 22 deletions

View File

@ -123,18 +123,11 @@ class UnsatisfiableSpecError(SpecError):
For original concretizer, provide the requirement that was violated when
raising.
"""
def __init__(self, provided, required=None, constraint_type=None, conflicts=None):
# required is only set by the original concretizer.
# clingo concretizer handles error messages differently.
if required is not None:
assert not conflicts # can't mix formats
super(UnsatisfiableSpecError, self).__init__(
"%s does not satisfy %s" % (provided, required))
else:
indented = [' %s\n' % conflict for conflict in conflicts]
conflict_msg = ''.join(indented)
msg = '%s is unsatisfiable, conflicts are:\n%s' % (provided, conflict_msg)
super(UnsatisfiableSpecError, self).__init__(msg)
def __init__(self, provided, required, constraint_type):
# This is only the entrypoint for old concretizer errors
super(UnsatisfiableSpecError, self).__init__(
"%s does not satisfy %s" % (provided, required))
self.provided = provided
self.required = required
self.constraint_type = constraint_type

View File

@ -41,6 +41,7 @@
import spack.paths
import spack.platforms
import spack.repo
import spack.solver.asp
import spack.spec
import spack.store
import spack.util.debug
@ -380,6 +381,13 @@ def make_argument_parser(**kwargs):
# stat names in groups of 7, for nice wrapping.
stat_lines = list(zip(*(iter(stat_names),) * 7))
# help message for --show-cores
show_cores_help = 'provide additional information on concretization failures\n'
show_cores_help += 'off (default): show only the violated rule\n'
show_cores_help += 'full: show raw unsat cores from clingo\n'
show_cores_help += 'minimized: show subset-minimal unsat cores '
show_cores_help += '(Warning: this may take hours for some specs)'
parser.add_argument(
'-h', '--help',
dest='help', action='store_const', const='short', default=None,
@ -403,6 +411,9 @@ def make_argument_parser(**kwargs):
'-d', '--debug', action='count', default=0,
help="write out debug messages "
"(more d's for more verbosity: -d, -dd, -ddd, etc.)")
parser.add_argument(
'--show-cores', choices=["off", "full", "minimized"], default="off",
help=show_cores_help)
parser.add_argument(
'--timestamp', action='store_true',
help="Add a timestamp to tty output")
@ -486,6 +497,13 @@ def setup_main_options(args):
spack.config.set('config:debug', True, scope='command_line')
spack.util.environment.tracing_enabled = True
if args.show_cores != "off":
# minimize_cores defaults to true, turn it off if we're showing full core
# but don't want to wait to minimize it.
spack.solver.asp.full_cores = True
if args.show_cores == 'full':
spack.solver.asp.minimize_cores = False
if args.timestamp:
tty.set_timestamp(True)

View File

@ -59,6 +59,14 @@
parse_files = None
#: whether we should write ASP unsat cores quickly in debug mode when the cores
#: may be very large or take the time (sometimes hours) to minimize them
minimize_cores = True
#: whether we should include all facts in the unsat cores or only error messages
full_cores = False
# backward compatibility functions for clingo ASTs
def ast_getter(*names):
def getter(node):
@ -393,10 +401,12 @@ def raise_if_unsat(self):
if len(constraints) == 1:
constraints = constraints[0]
debug = spack.config.get('config:debug', False)
conflicts = self.format_cores() if debug else self.format_minimal_cores()
if minimize_cores:
conflicts = self.format_minimal_cores()
else:
conflicts = self.format_cores()
raise spack.error.UnsatisfiableSpecError(constraints, conflicts=conflicts)
raise UnsatisfiableSpecError(constraints, conflicts=conflicts)
@property
def specs(self):
@ -512,10 +522,9 @@ def fact(self, head, assumption=False):
atom = self.backend.add_atom(symbol)
# in debug mode, make all facts choices/assumptions
# otherwise, only if we're generating cores and assumption=True
debug = spack.config.get('config:debug', False)
choice = debug or (self.cores and assumption)
# with `--show-cores=full or --show-cores=minimized, make all facts
# choices/assumptions, otherwise only if assumption=True
choice = self.cores and (full_cores or assumption)
self.backend.add_rule([atom], [], choice=choice)
if choice:
@ -2044,3 +2053,33 @@ def solve(specs, dump=(), models=0, timers=False, stats=False, tests=False,
return driver.solve(
setup, specs, dump, models, timers, stats, tests, reuse
)
class UnsatisfiableSpecError(spack.error.UnsatisfiableSpecError):
"""
Subclass for new constructor signature for new concretizer
"""
def __init__(self, provided, conflicts):
indented = [' %s\n' % conflict for conflict in conflicts]
conflict_msg = ''.join(indented)
issue = 'conflicts' if full_cores else 'errors'
msg = '%s is unsatisfiable, %s are:\n%s' % (provided, issue, conflict_msg)
newline_indent = '\n '
if not full_cores:
msg += newline_indent + 'To see full clingo unsat cores, '
msg += 're-run with `spack --show-cores=full`'
if not minimize_cores or not full_cores:
# not solver.minimalize_cores and not solver.full_cores impossible
msg += newline_indent + 'For full, subset-minimal unsat cores, '
msg += 're-run with `spack --show-cores=minimized'
msg += newline_indent
msg += 'Warning: This may take (up to) hours for some specs'
super(spack.error.UnsatisfiableSpecError, self).__init__(msg)
self.provided = provided
# Add attribute expected of the superclass interface
self.required = None
self.constraint_type = None

View File

@ -557,11 +557,13 @@ def test_conflicts_in_spec(self, conflict_spec):
with pytest.raises(spack.error.SpackError):
s.concretize()
def test_conflicts_new_concretizer_debug(self, conflict_spec, mutable_config):
def test_conflicts_show_cores(self, conflict_spec, monkeypatch):
if spack.config.get('config:concretizer') == 'original':
pytest.skip('Testing debug statements specific to new concretizer')
spack.config.set('config:debug', True)
monkeypatch.setattr(spack.solver.asp, 'full_cores', True)
monkeypatch.setattr(spack.solver.asp, 'minimize_cores', False)
s = Spec(conflict_spec)
with pytest.raises(spack.error.SpackError) as e:
s.concretize()

View File

@ -335,7 +335,7 @@ _spacktivate() {
_spack() {
if $list_options
then
SPACK_COMPREPLY="-h --help -H --all-help --color -c --config -C --config-scope -d --debug --timestamp --pdb -e --env -D --env-dir -E --no-env --use-env-repo -k --insecure -l --enable-locks -L --disable-locks -m --mock -p --profile --sorted-profile --lines -v --verbose --stacktrace -V --version --print-shell-vars"
SPACK_COMPREPLY="-h --help -H --all-help --color -c --config -C --config-scope -d --debug --show-cores --timestamp --pdb -e --env -D --env-dir -E --no-env --use-env-repo -k --insecure -l --enable-locks -L --disable-locks -m --mock -p --profile --sorted-profile --lines -v --verbose --stacktrace -V --version --print-shell-vars"
else
SPACK_COMPREPLY="activate add analyze arch audit blame bootstrap build-env buildcache cd checksum ci clean clone commands compiler compilers concretize config containerize create deactivate debug dependencies dependents deprecate dev-build develop diff docs edit env extensions external fetch find flake8 gc gpg graph help info install license list load location log-parse maintainers mark mirror module monitor patch pkg providers pydoc python reindex remove rm repo resource restage solve spec stage style tags test test-env tutorial undevelop uninstall unit-test unload url verify versions view"
fi