show-cores: fewer modes required

This commit is contained in:
Gregory Becker
2022-04-19 16:47:22 -07:00
parent 57889ec446
commit 11d382bff1
2 changed files with 9 additions and 21 deletions

View File

@@ -377,10 +377,9 @@ def make_argument_parser(**kwargs):
# help message for --show-cores # help message for --show-cores
show_cores_help = 'provide additional information on concretization failures\n' 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 (default): show raw unsat cores from clingo\n'
show_cores_help += 'full: show raw unsat cores from clingo\n'
show_cores_help += 'minimized: show subset-minimal unsat cores ' show_cores_help += 'minimized: show subset-minimal unsat cores '
show_cores_help += '(Warning: this may take hours for some specs)' show_cores_help += '(Warning: this may take hours in the worse case)'
parser.add_argument( parser.add_argument(
'-h', '--help', '-h', '--help',
@@ -406,7 +405,7 @@ def make_argument_parser(**kwargs):
help="write out debug messages " help="write out debug messages "
"(more d's for more verbosity: -d, -dd, -ddd, etc.)") "(more d's for more verbosity: -d, -dd, -ddd, etc.)")
parser.add_argument( parser.add_argument(
'--show-cores', choices=["off", "full", "minimized"], default="off", '--show-cores', choices=["full", "minimized"], default="full",
help=show_cores_help) help=show_cores_help)
parser.add_argument( parser.add_argument(
'--timestamp', action='store_true', '--timestamp', action='store_true',
@@ -495,12 +494,8 @@ def setup_main_options(args):
spack.config.set('config:debug', True, scope='command_line') spack.config.set('config:debug', True, scope='command_line')
spack.util.environment.tracing_enabled = True spack.util.environment.tracing_enabled = True
if args.show_cores != "off": if args.show_cores == "minimized":
# minimize_cores defaults to true, turn it off if we're showing full core spack.solver.asp.minimize_cores = True
# 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: if args.timestamp:
tty.set_timestamp(True) tty.set_timestamp(True)

View File

@@ -57,10 +57,7 @@
#: whether we should write ASP unsat cores quickly in debug mode when the cores #: 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 #: may be very large or take the time (sometimes hours) to minimize them
minimize_cores = True minimize_cores = False
#: whether we should include all facts in the unsat cores or only error messages
full_cores = False
# backward compatibility functions for clingo ASTs # backward compatibility functions for clingo ASTs
@@ -2221,19 +2218,15 @@ class UnsatisfiableSpecError(spack.error.UnsatisfiableSpecError):
def __init__(self, provided, conflicts): def __init__(self, provided, conflicts):
indented = [' %s\n' % conflict for conflict in conflicts] indented = [' %s\n' % conflict for conflict in conflicts]
conflict_msg = ''.join(indented) conflict_msg = ''.join(indented)
issue = 'conflicts' if full_cores else 'errors' msg = '%s is unsatisfiable, errors are:\n%s' % (provided, conflict_msg)
msg = '%s is unsatisfiable, %s are:\n%s' % (provided, issue, conflict_msg)
newline_indent = '\n ' newline_indent = '\n '
if not full_cores: if not minimize_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 # not solver.minimalize_cores and not solver.full_cores impossible
msg += newline_indent + 'For full, subset-minimal unsat cores, ' msg += newline_indent + 'For full, subset-minimal unsat cores, '
msg += 're-run with `spack --show-cores=minimized' msg += 're-run with `spack --show-cores=minimized'
msg += newline_indent msg += newline_indent
msg += 'Warning: This may take (up to) hours for some specs' msg += 'Warning: This may take (up to) hours in the worst-case'
super(spack.error.UnsatisfiableSpecError, self).__init__(msg) super(spack.error.UnsatisfiableSpecError, self).__init__(msg)