From 977a30fab3f9f5b34a1859f070beb0b6078ef821 Mon Sep 17 00:00:00 2001
From: Carlo Baldassi <carlobaldassi@gmail.com>
Date: Sat, 6 Jan 2018 00:42:09 +0100
Subject: [PATCH 1/9] Refactor resolve backtrace into a resolution log

---
 src/GraphType.jl | 485 ++++++++++++++++++++++++++++++++++++-----------
 src/Resolve.jl   |  24 ++-
 src/Types.jl     |  10 +-
 test/resolve.jl  |   3 +
 4 files changed, 410 insertions(+), 112 deletions(-)

diff --git a/src/GraphType.jl b/src/GraphType.jl
index 263fa67420e2f..8f49471ac8add 100644
--- a/src/GraphType.jl
+++ b/src/GraphType.jl
@@ -6,32 +6,56 @@ using ..Types
 import ..Types.uuid_julia
 import Pkg3.equalto
 
-export Graph, add_reqs!, add_fixed!, simplify_graph!
-
-# This is used to keep track of dependency relations when propagating
-# requirements, so as to emit useful information in case of unsatisfiable
-# conditions.
-# The `why` field is a Vector which keeps track of the requirements. Each
-# entry is a Tuple of two elements:
-# 1) the first element is the reason, and it can be either :fixed (for
-#    fixed packages), :explicit_requirement (for explicitly required packages),
-#    or a Tuple `(:constr_prop, p, backtrace_item)` (for requirements induced
-#    indirectly), where `p` is the package index and `backtrace_item` is
-#    another ResolveBacktraceItem.
-# 2) the second element is a BitVector representing the requirement as a mask
-#    over the possible states of the package
-mutable struct ResolveBacktraceItem
-    why::Vector{Any}
-    ResolveBacktraceItem() = new(Any[])
+export Graph, add_reqs!, add_fixed!, simplify_graph!, showlog
+
+# The ResolveLog is used to keep track of events that take place during the
+# resolution process. We use one ResolveLogEntry per package, and record all events
+# associated with that package. An event consists of two items: another
+# entry representing another package's influence (or `nothing`) and
+# a message for the log.
+#
+# Specialized functions called `log_event_[...]!` are used to store the
+# various events. The events are also recorded in orded in a shared
+# ResolveJournal, which is used to provide a plain chronological view.
+#
+# The `showlog` functions are used for display, and called to create messages
+# in case of resolution errors.
+
+const ResolveJournal = Vector{Tuple{UUID,String}}
+
+mutable struct ResolveLogEntry
+    journal::ResolveJournal # shared with all other entries
+    pkg::UUID
+    header::String
+    events::Vector{Tuple{Any,String}} # here Any should ideally be Union{ResolveLogEntry,Void}
+    ResolveLogEntry(journal::ResolveJournal, pkg::UUID, msg::String = "") = new(journal, pkg, msg, [])
 end
 
-function Base.push!(ritem::ResolveBacktraceItem, reason, versionmask)
-    push!(ritem.why, (reason, versionmask))
+function Base.push!(entry::ResolveLogEntry, reason::Tuple{Union{ResolveLogEntry,Void},String})
+    push!(entry.events, reason)
+    entry.pkg ≠ uuid_julia && push!(entry.journal, (entry.pkg, reason[2]))
+    return entry
+end
+
+# Note: the `init` field is used to keep track of all entries which were there
+# at the beginning, since the `pool` can be pruned during the resolution process.
+mutable struct ResolveLog
+    init::ResolveLogEntry
+    pool::Dict{UUID,ResolveLogEntry}
+    journal::Vector{Tuple{UUID,String}}
+    function ResolveLog()
+        journal = ResolveJournal()
+        return new(ResolveLogEntry(journal, uuid_julia), Dict(), journal)
+    end
 end
 
 # Installation state: either a version, or uninstalled
 const InstState = Union{VersionNumber,Void}
 
+
+# GraphData is basically a part of Graph that collects data structures useful
+# for interfacing the internal abstract representation of Graph with the
+# input/output (e.g. converts between package UUIDs and node numbers, etc.)
 mutable struct GraphData
     # packages list
     pkgs::Vector{UUID}
@@ -56,8 +80,11 @@ mutable struct GraphData
     #                  pvers[p0][vdict[p0][vn]] = vn
     vdict::Vector{Dict{VersionNumber,Int}}
 
+    # UUID to names
     uuid_to_name::Dict{UUID,String}
 
+    # requirements and fixed packages, passed at initialization
+    # (TODO: these are probably useless?)
     reqs::Requires
     fixed::Dict{UUID,Fixed}
 
@@ -72,6 +99,9 @@ mutable struct GraphData
     #                      states, keep track of other equivalent states
     eq_classes::Dict{UUID,Dict{InstState,Set{InstState}}}
 
+    # resolve log: keep track of the resolution process
+    rlog::ResolveLog
+
     function GraphData(
             versions::Dict{UUID,Set{VersionNumber}},
             deps::Dict{UUID,Dict{VersionRange,Dict{String,UUID}}},
@@ -94,13 +124,21 @@ mutable struct GraphData
         # generate vdict
         vdict = [Dict{VersionNumber,Int}(vn => i for (i,vn) in enumerate(pvers[p0])) for p0 = 1:np]
 
+        # nothing is pruned yet, of course
         pruned = Dict{UUID,VersionNumber}()
 
         # equivalence classes (at the beginning each state represents just itself)
         eq_vn(v0, p0) = (v0 == spp[p0] ? nothing : pvers[p0][v0])
         eq_classes = Dict(pkgs[p0] => Dict(eq_vn(v0,p0) => Set([eq_vn(v0,p0)]) for v0 = 1:spp[p0]) for p0 = 1:np)
 
-        return new(pkgs, np, spp, pdict, pvers, vdict, uuid_to_name, reqs, fixed, pruned, eq_classes)
+        # the resolution log is actually initialized below
+        rlog = ResolveLog()
+
+        data = new(pkgs, np, spp, pdict, pvers, vdict, uuid_to_name, reqs, fixed, pruned, eq_classes, rlog)
+
+        init_log!(data)
+
+        return data
     end
 end
 
@@ -161,9 +199,6 @@ mutable struct Graph
     # states per package: same as in GraphData
     spp::Vector{Int}
 
-    # backtrace: keep track of the resolution process
-    bktrc::Vector{ResolveBacktraceItem}
-
     # number of packages (all Vectors above have this length)
     np::Int
 
@@ -180,7 +215,7 @@ mutable struct Graph
         extra_uuids ⊆ keys(versions) || error("unknown UUID found in reqs/fixed") # TODO?
 
         data = GraphData(versions, deps, compat, uuid_to_name, reqs, fixed)
-        pkgs, np, spp, pdict, pvers, vdict = data.pkgs, data.np, data.spp, data.pdict, data.pvers, data.vdict
+        pkgs, np, spp, pdict, pvers, vdict, rlog = data.pkgs, data.np, data.spp, data.pdict, data.pvers, data.vdict, data.rlog
 
         extended_deps = [[Dict{Int,BitVector}() for v0 = 1:(spp[p0]-1)] for p0 = 1:np]
         for p0 = 1:np, v0 = 1:(spp[p0]-1)
@@ -265,9 +300,7 @@ mutable struct Graph
         req_inds = Set{Int}()
         fix_inds = Set{Int}()
 
-        bktrc = [ResolveBacktraceItem() for p0 = 1:np]
-
-        graph = new(data, gadj, gmsk, gdir, gconstr, adjdict, req_inds, fix_inds, spp, bktrc, np)
+        graph = new(data, gadj, gmsk, gdir, gconstr, adjdict, req_inds, fix_inds, spp, np)
 
         _add_fixed!(graph, fixed)
         _add_reqs!(graph, reqs, :explicit_requirement)
@@ -293,7 +326,6 @@ function _add_reqs!(graph::Graph, reqs::Requires, reason)
     gconstr = graph.gconstr
     spp = graph.spp
     req_inds = graph.req_inds
-    bktrc = graph.bktrc
     pdict = graph.data.pdict
     pvers = graph.data.pvers
 
@@ -309,7 +341,7 @@ function _add_reqs!(graph::Graph, reqs::Requires, reason)
         old_constr = copy(gconstr[rp0])
         gconstr[rp0] .&= new_constr
         reason ≡ :explicit_requirement && push!(req_inds, rp0)
-        old_constr ≠ gconstr[rp0] && push!(bktrc[rp0], reason, new_constr)
+        old_constr ≠ gconstr[rp0] && log_event_req!(graph, rp, rvs, reason)
     end
     return graph
 end
@@ -326,7 +358,6 @@ function _add_fixed!(graph::Graph, fixed::Dict{UUID,Fixed})
     gconstr = graph.gconstr
     spp = graph.spp
     fix_inds = graph.fix_inds
-    bktrc = graph.bktrc
     pdict = graph.data.pdict
     vdict = graph.data.vdict
 
@@ -338,14 +369,15 @@ function _add_fixed!(graph::Graph, fixed::Dict{UUID,Fixed})
         new_constr[fv0] = true
         gconstr[fp0] .&= new_constr
         push!(fix_inds, fp0)
-        push!(bktrc[fp0], :fixed, new_constr)
-        _add_reqs!(graph, fx.requires, (:constr_prop, fp0, bktrc[fp0]))
+        bkitem = log_event_fixed!(graph, fp, fx)
+        _add_reqs!(graph, fx.requires, (fp, bkitem))
     end
     return graph
 end
 
-Types.pkgID(p::UUID, graph::Graph) = pkgID(p, graph.data.uuid_to_name)
-Types.pkgID(p0::Int, graph::Graph) = pkgID(graph.data.pkgs[p0], graph)
+Types.pkgID(p::UUID, data::GraphData) = pkgID(p, data.uuid_to_name)
+Types.pkgID(p0::Int, data::GraphData) = pkgID(data.pkgs[p0], data)
+Types.pkgID(p, graph::Graph) = pkgID(p, graph.data)
 
 function check_consistency(graph::Graph)
     np = graph.np
@@ -357,7 +389,6 @@ function check_consistency(graph::Graph)
     adjdict = graph.adjdict
     req_inds = graph.req_inds
     fix_inds = graph.fix_inds
-    bktrc = graph.bktrc
     data = graph.data
     pkgs = data.pkgs
     pdict = data.pdict
@@ -365,9 +396,10 @@ function check_consistency(graph::Graph)
     vdict = data.vdict
     pruned = data.pruned
     eq_classes = data.eq_classes
+    rlog = data.rlog
 
     @assert np ≥ 0
-    for x in [spp, gadj, gmsk, gdir, gconstr, adjdict, bktrc, pkgs, pdict, pvers, vdict]
+    for x in [spp, gadj, gmsk, gdir, gconstr, adjdict, rlog.pool, pkgs, pdict, pvers, vdict]
         @assert length(x) == np
     end
     for p0 = 1:np
@@ -425,78 +457,320 @@ function check_consistency(graph::Graph)
     return true
 end
 
-"Show the resolution backtrace for some package"
-function showbacktrace(io::IO, graph::Graph, p0::Int)
-    _show(io, graph, p0, graph.bktrc[p0], "", Set{ResolveBacktraceItem}())
+function init_log!(data::GraphData)
+    np = data.np
+    pkgs = data.pkgs
+    pvers = data.pvers
+    rlog = data.rlog
+    for p0 = 1:np
+        p = pkgs[p0]
+        id = pkgID(p0, data)
+        versions = pvers[p0]
+        if isempty(versions)
+            msg = "$id has no known versions!" # This shouldn't happen?
+        else
+            msg = "possible versions are: $(VersionSpec(VersionRange.(versions))) or uninstalled"
+        end
+        first_entry = get!(rlog.pool, p) do; ResolveLogEntry(rlog.journal, p, "$id log:") end
+
+        if p ≠ uuid_julia
+            push!(first_entry, (nothing, msg))
+            push!(rlog.init, (first_entry, ""))
+        end
+    end
+    return data
 end
 
-# Show a recursive tree with requirements applied to a package, either directly or indirectly
-function _show(io::IO, graph::Graph, p0::Int, ritem::ResolveBacktraceItem, indent::String, seen::Set{ResolveBacktraceItem})
-    id0 = pkgID(p0, graph)
+function log_event_fixed!(graph::Graph, fp::UUID, fx::Fixed)
+    rlog = graph.data.rlog
+    id = pkgID(fp, graph)
+    msg = "$id is fixed to version $(fx.version)"
+    entry = rlog.pool[fp]
+    push!(entry, (nothing, msg))
+    return entry
+end
+
+function log_event_req!(graph::Graph, rp::UUID, rvs::VersionSpec, reason)
+    rlog = graph.data.rlog
+    gconstr = graph.gconstr
+    pdict = graph.data.pdict
+    pvers = graph.data.pvers
+    id = pkgID(rp, graph)
+    msg = "restricted to versions $rvs by "
+    if reason isa Symbol
+        @assert reason == :explicit_requirement
+        other_entry = nothing
+        msg *= "an explicit requirement, "
+    else
+        @assert reason isa Tuple{UUID,ResolveLogEntry}
+        other_p, other_entry = reason
+        if other_p == uuid_julia
+            msg *= "julia compatibility requirements, "
+            other_entry = nothing
+        else
+            other_id = pkgID(other_p, graph)
+            msg *= "$other_id, "
+        end
+    end
+    rp0 = pdict[rp]
+    @assert !gconstr[rp0][end]
+    if any(gconstr[rp0])
+        msg *= "leaving only versions $(VersionSpec(VersionRange.(pvers[rp0][gconstr[rp0][1:(end-1)]])))"
+    else
+        msg *= "leaving no versions left"
+    end
+    entry = rlog.pool[rp]
+    push!(entry, (other_entry, msg))
+    return entry
+end
+
+function log_event_implicit_req!(graph::Graph, p1::Int, vmask::BitVector, p0::Int)
+    rlog = graph.data.rlog
     gconstr = graph.gconstr
     pkgs = graph.data.pkgs
     pvers = graph.data.pvers
 
     function vs_string(p0::Int, vmask::BitVector)
-        vns = Vector{Any}(pvers[p0][vmask[1:(end-1)]])
-        vmask[end] && push!(vns, "uninstalled")
-        return join(string.(vns), ", ", " or ")
-    end
-
-    l = length(ritem.why)
-    for (i,(w,vmask)) in enumerate(ritem.why)
-        print(io, indent, (i==l ? '└' : '├'), '─')
-        if w ≡ :fixed
-            @assert count(vmask) == 1
-            println(io, "$id0 is fixed to version ", vs_string(p0, vmask))
-        elseif w ≡ :explicit_requirement
-            @assert !vmask[end]
-            if any(vmask)
-                println(io, "an explicit requirement sets $id0 to versions: ", vs_string(p0, vmask))
-            else
-                println(io, "an explicit requirement cannot be matched by any of the available versions of $id0")
-            end
+        if any(vmask[1:(end-1)])
+            vns = string(VersionSpec(VersionRange.(pvers[p0][vmask[1:(end-1)]])))
+            vmask[end] && (vns *= " or uninstalled")
+        elseif vmask[end]
+            vns = "uninstalled"
         else
-            @assert w isa Tuple{Symbol,Int,ResolveBacktraceItem}
-            @assert w[1] == :constr_prop
-            p1 = w[2]
-            if !is_current_julia(graph, p1)
-                id1 = pkgID(p1, graph)
-                otheritem = w[3]
-                if any(vmask)
-                    println(io, "the only versions of $id0 compatible with $id1 (whose allowed versions are $(vs_string(p1, gconstr[p1])))\n",
-                                indent, (i==l ? "  " : "│ "),"are these: ", vs_string(p0, vmask))
-                else
-                    println(io, "no versions of $id0 are compatible with $id1 (whose allowed versions are $(vs_string(p1, gconstr[p1])))")
-                end
-                if otheritem ∈ seen
-                    println(io, indent, (i==l ? "  " : "│ "), "└─see above for $id1 backtrace")
-                    continue
-                end
-                push!(seen, otheritem)
-                _show(io, graph, p1, otheritem, indent * (i==l ? "  " : "│ "), seen)
+            vns = "no version"
+        end
+        return vns
+    end
+
+    p = pkgs[p1]
+    id = pkgID(p, graph)
+    other_p, other_entry = pkgs[p0], rlog.pool[pkgs[p0]]
+    other_id = pkgID(other_p, graph)
+    if any(vmask)
+        msg = "restricted by "
+        if other_p == uuid_julia
+            msg *= "julia compatibility requirements "
+            other_entry = nothing # don't propagate the log
+        else
+            other_id = pkgID(other_p, graph)
+            msg *= "compatibility requirements with $other_id "
+        end
+        msg *= "to versions: $(vs_string(p1, vmask))"
+        if vmask ≠ gconstr[p1]
+            msg *= ", leaving "
+            if any(gconstr[p1])
+                msg *= "only versions: $(vs_string(p1, gconstr[p1]))"
             else
-                if any(vmask)
-                    println(io, "the only versions of $id0 compatible with julia v$VERSION are these: ", vs_string(p0, vmask))
-                else
-                    println(io, "no versions of $id0 are compatible with julia v$VERSION")
-                end
+                msg *= "no versions left"
             end
         end
+    else
+        msg = "found to have no compatible versions left with "
+        if other_p == uuid_julia
+            msg *= "julia"
+            other_entry = nothing # don't propagate the log
+        else
+            other_id = pkgID(other_p, graph)
+            msg *= "$other_id "
+        end
+    end
+    entry = rlog.pool[p]
+    push!(entry, (other_entry, msg))
+    return entry
+end
+
+function log_event_pruned!(graph::Graph, p0::Int, s0::Int)
+    rlog = graph.data.rlog
+    spp = graph.spp
+    pkgs = graph.data.pkgs
+    pvers = graph.data.pvers
+
+    p = pkgs[p0]
+    id = pkgID(p, graph)
+    if s0 == spp[p0]
+        msg = "determined to be unneeded during graph pruning"
+    else
+        msg = "fixed during graph pruning to its only remaining available version, $(pvers[p0][s0])"
+    end
+    entry = rlog.pool[p]
+    push!(entry, (nothing, msg))
+    return entry
+end
+
+function log_event_greedysolved!(graph::Graph, p0::Int, s0::Int)
+    rlog = graph.data.rlog
+    spp = graph.spp
+    pkgs = graph.data.pkgs
+    pvers = graph.data.pvers
+
+    p = pkgs[p0]
+    id = pkgID(p, graph)
+    if s0 == spp[p0]
+        msg = "determined to be unneeded by the solver"
+    else
+        if s0 == spp[p0] - 1
+            msg = "set by the solver to its maximum version: $(pvers[p0][s0])"
+        else
+            msg = "set by the solver to the maximum version compatible with the constraints: $(pvers[p0][s0])"
+        end
+    end
+    entry = rlog.pool[p]
+    push!(entry, (nothing, msg))
+    return entry
+end
+
+function log_event_maxsumsolved!(graph::Graph, p0::Int, s0::Int, why::Symbol)
+    rlog = graph.data.rlog
+    spp = graph.spp
+    pkgs = graph.data.pkgs
+    pvers = graph.data.pvers
+
+    p = pkgs[p0]
+    id = pkgID(p, graph)
+    if s0 == spp[p0]
+        @assert why == :uninst
+        msg = "determined to be unneeded by the solver"
+    else
+        @assert why == :constr
+        if s0 == spp[p0] - 1
+            msg = "set by the solver to its maximum version: $(pvers[p0][s0])"
+        else
+            msg = "set by the solver version: $(pvers[p0][s0]) (version $(pvers[p0][s0+1]) would violate its constraints)"
+        end
     end
+    entry = rlog.pool[p]
+    push!(entry, (nothing, msg))
+    return entry
 end
 
-function is_current_julia(graph::Graph, p1::Int)
+function log_event_maxsumsolved!(graph::Graph, p0::Int, s0::Int, p1::Int)
+    rlog = graph.data.rlog
+    spp = graph.spp
+    pkgs = graph.data.pkgs
+    pvers = graph.data.pvers
+
+    p = pkgs[p0]
+    id = pkgID(p, graph)
+    other_id = pkgID(p1, graph)
+    @assert s0 ≠ spp[p0]
+    if s0 == spp[p0] - 1
+        msg = "set by the solver to its maximum version: $(pvers[p0][s0]) (installation is required by $other_id)"
+    else
+        msg = "set by the solver version: $(pvers[p0][s0]) (version $(pvers[p0][s0+1]) would violate a dependecy relation with $other_id)"
+    end
+    other_entry = rlog.pool[pkgs[p1]]
+    entry = rlog.pool[p]
+    push!(entry, (other_entry, msg))
+    return entry
+end
+
+function log_event_eq_classes!(graph::Graph, p0::Int)
+    rlog = graph.data.rlog
+    spp = graph.spp
     gconstr = graph.gconstr
-    fix_inds = graph.fix_inds
     pkgs = graph.data.pkgs
     pvers = graph.data.pvers
 
-    (pkgs[p1] == uuid_julia && p1 ∈ fix_inds) || return false
-    jconstr = gconstr[p1]
-    return length(jconstr) == 2 && !jconstr[2] && pvers[p1][1] == VERSION
+    if any(gconstr[p0][1:(end-1)])
+        vns = string(VersionSpec(VersionRange.(pvers[p0][gconstr[p0][1:(end-1)]])))
+        gconstr[p0][end] && (vns *= " or uninstalled")
+    elseif gconstr[p0][end]
+        vns = "uninstalled"
+    else
+        vns = "no version"
+    end
+
+    p = pkgs[p0]
+    id = pkgID(p, graph)
+    msg = "versions reduced by equivalence to: $vns"
+    entry = rlog.pool[p]
+    push!(entry, (nothing, msg))
+    return entry
 end
 
+"""
+Show the full resolution log. The `view` keyword controls how the events are displayed/grouped:
+
+ * `:plain` for a shallow view, grouped by package, alphabetically (the default)
+ * `:tree` for a tree view in which the log of a package is displayed as soon as it appears
+           in the process (the top-level is still grouped by package, alphabetically)
+ * `:chronological` for a flat view of all events in chronological order
+"""
+function showlog(io::IO, graph::Graph; view::Symbol = :plain)
+    view ∈ [:plain, :tree, :chronological] || throw(ArgumentError("the view argument should be `:plain`, `:tree` or `:chronological`"))
+    println(io, "Resolve log:")
+    view == :chronological && return showlogjournal(io, graph)
+    seen = ObjectIdDict()
+    recursive = (view == :tree)
+    initentries = [event[1] for event in graph.data.rlog.init.events]
+    for entry in sort!(initentries, by=(entry->pkgID(entry.pkg, graph)))
+        _show(io, graph, entry, "", seen, recursive)
+        recursive && (seen[entry] = true)
+    end
+end
+
+function showlogjournal(io::IO, graph::Graph)
+    journal = graph.data.rlog.journal
+    padding = maximum(length(pkgID(p, graph)) for (p,_) in journal)
+    for (p, msg) in journal
+        println(io, ' ', rpad(pkgID(p, graph), padding), ": ", msg)
+    end
+end
+
+"""
+Show the resolution log for some package, and all the other packages that affected
+it during resolution. The `view` option can be either `:plain` or `:tree` (works
+the same as for `showlog(io, graph)`); the default is `:tree`.
+"""
+function showlog(io::IO, graph::Graph, p::UUID; view::Symbol = :tree)
+    view ∈ [:plain, :tree] || throw(ArgumentError("the view argument should be `:plain` or `:tree`"))
+    rlog = graph.data.rlog
+    if view == :tree
+        _show(io, graph, rlog.pool[p], "", ObjectIdDict(), true)
+    else
+        entries = ResolveLogEntry[rlog.pool[p]]
+        function getentries(entry)
+            for (other_entry,_) in entry.events
+                (other_entry ≡ nothing || other_entry ∈ entries) && continue
+                push!(entries, other_entry)
+                getentries(other_entry)
+            end
+        end
+        getentries(rlog.pool[p])
+        for entry in entries
+            _show(io, graph, entry, "", ObjectIdDict(), false)
+        end
+    end
+end
+
+# Show a recursive tree with requirements applied to a package, either directly or indirectly
+function _show(io::IO, graph::Graph, entry::ResolveLogEntry, indent::String, seen::ObjectIdDict, recursive::Bool)
+    toplevel = isempty(indent)
+    firstglyph = toplevel ? "" : "└─"
+    pre = toplevel ? "" : "  "
+    println(io, indent, firstglyph, entry.header)
+    l = length(entry.events)
+    for (i,(otheritem,msg)) in enumerate(entry.events)
+        if !isempty(msg)
+            print(io, indent * pre, (i==l ? '└' : '├'), '─')
+            println(io, msg)
+            newindent = indent * pre * (i==l ? "  " : "│ ")
+        else
+            newindent = indent
+        end
+        otheritem ≡ nothing && continue
+        recursive || continue
+        if otheritem ∈ keys(seen)
+            println(io, newindent, "└─", otheritem.header, " see above")
+            continue
+        end
+        seen[otheritem] = true
+        _show(io, graph, otheritem, newindent, seen, recursive)
+    end
+end
+
+is_julia(graph::Graph, p0::Int) = graph.data.pkgs[p0] == uuid_julia
+
 "Check for contradictions in the constraints."
 function check_constraints(graph::Graph)
     np = graph.np
@@ -504,12 +778,12 @@ function check_constraints(graph::Graph)
     pkgs = graph.data.pkgs
     pvers = graph.data.pvers
 
-    id(p0::Int) = pkgID(pkgs[p0], graph)
+    id(p0::Int) = pkgID(p0, graph)
 
     for p0 = 1:np
         any(gconstr[p0]) && continue
         err_msg = "Unsatisfiable requirements detected for package $(id(p0)):\n"
-        err_msg *= sprint(showbacktrace, graph, p0)
+        err_msg *= sprint(showlog, graph, pkgs[p0])
         throw(PkgError(err_msg))
     end
     return true
@@ -518,18 +792,18 @@ end
 """
 Propagates current constraints, determining new implicit constraints.
 Throws an error in case impossible requirements are detected, printing
-a backtrace.
+a log trace.
 """
 function propagate_constraints!(graph::Graph)
     np = graph.np
     spp = graph.spp
     gadj = graph.gadj
     gmsk = graph.gmsk
-    bktrc = graph.bktrc
     gconstr = graph.gconstr
     adjdict = graph.adjdict
     pkgs = graph.data.pkgs
     pvers = graph.data.pvers
+    rlog = graph.data.rlog
 
     id(p0::Int) = pkgID(pkgs[p0], graph)
 
@@ -542,7 +816,7 @@ function propagate_constraints!(graph::Graph)
             gconstr0 = gconstr[p0]
             for (j1,p1) in enumerate(gadj[p0])
                 # we don't propagate to julia (purely to have better error messages)
-                is_current_julia(graph, p1) && continue
+                pkgs[p1] == uuid_julia && continue
 
                 msk = gmsk[p0][j1]
                 # consider the sub-mask with only allowed versions of p0
@@ -560,11 +834,11 @@ function propagate_constraints!(graph::Graph)
                 # previous ones, record it and propagate them next
                 if gconstr1 ≠ old_gconstr1
                     push!(staged_next, p1)
-                    push!(bktrc[p1], (:constr_prop, p0, bktrc[p0]), added_constr1)
+                    log_event_implicit_req!(graph, p1, added_constr1, p0)
                 end
                 if !any(gconstr1)
                     err_msg = "Unsatisfiable requirements detected for package $(id(p1)):\n"
-                    err_msg *= sprint(showbacktrace, graph, p1)
+                    err_msg *= sprint(showlog, graph, pkgs[p1])
                     throw(PkgError(err_msg))
                 end
             end
@@ -636,10 +910,6 @@ function compute_eq_classes!(graph::Graph; verbose::Bool = false)
              """)
     end
 
-    # wipe out backtrace because it doesn't make sense now
-    # TODO: save it somehow?
-    graph.bktrc = [ResolveBacktraceItem() for p0 = 1:np]
-
     @assert check_consistency(graph)
 
     return graph
@@ -657,6 +927,7 @@ function build_eq_classes1!(graph::Graph, p0::Int)
     pvers = data.pvers
     vdict = data.vdict
     eq_classes = data.eq_classes
+    rlog = data.rlog
 
     # concatenate all the constraints; the columns of the
     # result encode the behavior of each version
@@ -709,6 +980,9 @@ function build_eq_classes1!(graph::Graph, p0::Int)
     pvers[p0] = pvers[p0][repr_vers[1:(end-1)]]
     vdict[p0] = Dict(vn => i for (i,vn) in enumerate(pvers[p0]))
 
+    # put a record in the log
+    log_event_eq_classes!(graph, p0)
+
     return
 end
 
@@ -726,13 +1000,13 @@ function prune_graph!(graph::Graph; verbose::Bool = false)
     adjdict = graph.adjdict
     req_inds = graph.req_inds
     fix_inds = graph.fix_inds
-    bktrc = graph.bktrc
     data = graph.data
     pkgs = data.pkgs
     pdict = data.pdict
     pvers = data.pvers
     vdict = data.vdict
     pruned = data.pruned
+    rlog = data.rlog
 
     # We will remove all packages that only have one allowed state
     # (includes fixed packages and forbidden packages)
@@ -768,7 +1042,8 @@ function prune_graph!(graph::Graph; verbose::Bool = false)
         # We don't record fixed packages
         p0 ∈ fix_inds && (@assert s0 ≠ spp[p0]; continue)
         p0 ∈ req_inds && @assert s0 ≠ spp[p0]
-        # We don't record packages that are not going to be installed
+        log_event_pruned!(graph, p0, s0)
+        # We don't record as pruned packages that are not going to be installed
         s0 == spp[p0] && continue
         @assert !haskey(pruned, pkgs[p0])
         pruned[pkgs[p0]] = pvers[p0][s0]
@@ -853,9 +1128,8 @@ function prune_graph!(graph::Graph; verbose::Bool = false)
     end
     new_gmsk = [[compute_gmsk(new_p0, new_j0) for new_j0 = 1:length(new_gadj[new_p0])] for new_p0 = 1:new_np]
 
-    # Clear out resolution backtrace
-    # TODO: save it somehow?
-    new_bktrc = [ResolveBacktraceItem() for new_p0 = 1:new_np]
+    # Reduce log pool (the other items are still reachable through rlog.init)
+    rlog.pool = Dict(p=>rlog.pool[p] for p in new_pkgs)
 
     # Done
 
@@ -876,7 +1150,7 @@ function prune_graph!(graph::Graph; verbose::Bool = false)
     data.vdict = new_vdict
     # Notes:
     #   * uuid_to_name, reqs, fixed, eq_classes are unchanged
-    #   * pruned was updated in-place
+    #   * pruned and rlog were updated in-place
 
     # Replace old structures with new ones
     graph.gadj = new_gadj
@@ -887,7 +1161,6 @@ function prune_graph!(graph::Graph; verbose::Bool = false)
     graph.req_inds = new_req_inds
     graph.fix_inds = new_fix_inds
     graph.spp = new_spp
-    graph.bktrc = new_bktrc
     graph.np = new_np
 
     @assert check_consistency(graph)
diff --git a/src/Resolve.jl b/src/Resolve.jl
index ad856db077bf5..d4e7b6e46114c 100644
--- a/src/Resolve.jl
+++ b/src/Resolve.jl
@@ -9,7 +9,7 @@ using ..Types
 using ..GraphType
 using .MaxSum
 import ..Types: uuid_julia
-import ..GraphType: is_current_julia
+import ..GraphType: is_julia, log_event_greedysolved!, log_event_maxsumsolved!
 
 export resolve, sanity_check
 
@@ -76,8 +76,8 @@ function sanity_check(graph::Graph, sources::Set{UUID} = Set{UUID}(); verbose::B
     id(p) = pkgID(p, graph)
 
     isempty(req_inds) || warn("sanity check called on a graph with non-empty requirements")
-    if !any(is_current_julia(graph, fp0) for fp0 in fix_inds)
-        warn("sanity check called on a graph without current julia requirement, adding it")
+    if !any(is_julia(graph, fp0) for fp0 in fix_inds)
+        warn("sanity check called on a graph without julia requirement, adding it")
         add_fixed!(graph, Dict(uuid_julia=>Fixed(VERSION)))
     end
     if length(fix_inds) ≠ 1
@@ -257,6 +257,10 @@ function greedysolver(graph::Graph)
 
     @assert verify_solution(sol, graph)
 
+    for p0 = 1:np
+        log_event_greedysolved!(graph, p0, sol[p0])
+    end
+
     return true, sol
 end
 
@@ -297,16 +301,20 @@ function enforce_optimality!(sol::Vector{Int}, graph::Graph)
     gmsk = graph.gmsk
     gdir = graph.gdir
     gconstr = graph.gconstr
+    pkgs = graph.data.pkgs
+
+    # keep a track for the log
+    why = Union{Symbol,Int}[0 for p0 = 1:np]
 
     restart = true
     while restart
         restart = false
         for p0 = 1:np
             s0 = sol[p0]
-            s0 == spp[p0] && continue # the package is not installed
+            s0 == spp[p0] && (why[p0] = :uninst; continue) # the package is not installed
 
             # check if bumping to the higher version would violate a constraint
-            gconstr[p0][s0+1] || continue
+            gconstr[p0][s0+1] || (why[p0] = :constr; continue)
 
             # check if bumping to the higher version would violate a constraint
             viol = false
@@ -315,6 +323,7 @@ function enforce_optimality!(sol::Vector{Int}, graph::Graph)
                 msk = gmsk[p0][j1]
                 if !msk[s1, s0+1]
                     viol = true
+                    why[p0] = p1
                     break
                 end
             end
@@ -352,9 +361,14 @@ function enforce_optimality!(sol::Vector{Int}, graph::Graph)
 
     for p0 in find(uninst)
         sol[p0] = spp[p0]
+        why[p0] = :uninst
     end
 
     @assert verify_solution(sol, graph)
+
+    for p0 = 1:np
+        log_event_maxsumsolved!(graph, p0, sol[p0], why[p0])
+    end
 end
 
 end # module
diff --git a/src/Types.jl b/src/Types.jl
index 2f79b9947f005..465ea5b98e665 100644
--- a/src/Types.jl
+++ b/src/Types.jl
@@ -176,6 +176,15 @@ function Base.convert(::Type{VersionRange}, s::AbstractString)
     return VersionRange(lower, upper)
 end
 
+Base.print(io::IO, r::VersionRange{0,0}) = print(io, '*')
+function Base.print(io::IO, r::VersionRange{0,n}) where {n}
+    print(io, "0-")
+    join(io, r.upper.t, '.')
+end
+function Base.print(io::IO, r::VersionRange{m,0}) where {m}
+    join(io, r.lower.t, '.')
+    print(io, "-*")
+end
 function Base.print(io::IO, r::VersionRange)
     join(io, r.lower.t, '.')
     if r.lower != r.upper
@@ -183,7 +192,6 @@ function Base.print(io::IO, r::VersionRange)
         join(io, r.upper.t, '.')
     end
 end
-Base.print(io::IO, ::VersionRange{0,0}) = print(io, "*")
 Base.show(io::IO, r::VersionRange) = print(io, "VersionRange(\"", r, "\")")
 
 Base.in(v::VersionNumber, r::VersionRange) = r.lower ≲ v ≲ r.upper
diff --git a/test/resolve.jl b/test/resolve.jl
index 9194cbca03a4c..c95ee23e800f4 100644
--- a/test/resolve.jl
+++ b/test/resolve.jl
@@ -197,6 +197,8 @@ function resolve_tst(deps_data, reqs_data, want_data = nothing)
     simplify_graph!(graph, verbose = VERBOSE)
     want = resolve(graph, verbose = VERBOSE)
 
+    # info("BACKTRACE:\n" * sprint(showbacktrace, graph))
+
     return want == wantuuids(want_data)
 end
 
@@ -329,6 +331,7 @@ VERBOSE && info("SCHEME 5")
 deps_data = Any[
     ["A", v"1", "B", "2-*"],
     ["A", v"1", "C", "2-*"],
+    # ["A", v"1", "julia", "10"],
     ["A", v"2", "B", "1"],
     ["A", v"2", "C", "1"],
     ["B", v"1", "C", "2-*"],

From 6e97978560038d1702bca06890538ffc32826ddb Mon Sep 17 00:00:00 2001
From: Carlo Baldassi <carlobaldassi@gmail.com>
Date: Wed, 20 Dec 2017 01:05:52 +0100
Subject: [PATCH 2/9] Remove reqs and fixed from GraphData

---
 src/GraphType.jl | 15 ++++-----------
 1 file changed, 4 insertions(+), 11 deletions(-)

diff --git a/src/GraphType.jl b/src/GraphType.jl
index 8f49471ac8add..bcef950f6d3bb 100644
--- a/src/GraphType.jl
+++ b/src/GraphType.jl
@@ -83,11 +83,6 @@ mutable struct GraphData
     # UUID to names
     uuid_to_name::Dict{UUID,String}
 
-    # requirements and fixed packages, passed at initialization
-    # (TODO: these are probably useless?)
-    reqs::Requires
-    fixed::Dict{UUID,Fixed}
-
     # pruned packages: during graph simplification, packages that
     #                  only have one allowed version are pruned.
     #                  This keeps track of them, so that they may
@@ -106,9 +101,7 @@ mutable struct GraphData
             versions::Dict{UUID,Set{VersionNumber}},
             deps::Dict{UUID,Dict{VersionRange,Dict{String,UUID}}},
             compat::Dict{UUID,Dict{VersionRange,Dict{String,VersionSpec}}},
-            uuid_to_name::Dict{UUID,String},
-            reqs::Requires,
-            fixed::Dict{UUID,Fixed}
+            uuid_to_name::Dict{UUID,String}
         )
         # generate pkgs
         pkgs = sort!(collect(keys(versions)))
@@ -134,7 +127,7 @@ mutable struct GraphData
         # the resolution log is actually initialized below
         rlog = ResolveLog()
 
-        data = new(pkgs, np, spp, pdict, pvers, vdict, uuid_to_name, reqs, fixed, pruned, eq_classes, rlog)
+        data = new(pkgs, np, spp, pdict, pvers, vdict, uuid_to_name, pruned, eq_classes, rlog)
 
         init_log!(data)
 
@@ -214,7 +207,7 @@ mutable struct Graph
         extra_uuids = union(keys(reqs), keys(fixed), map(fx->keys(fx.requires), values(fixed))...)
         extra_uuids ⊆ keys(versions) || error("unknown UUID found in reqs/fixed") # TODO?
 
-        data = GraphData(versions, deps, compat, uuid_to_name, reqs, fixed)
+        data = GraphData(versions, deps, compat, uuid_to_name)
         pkgs, np, spp, pdict, pvers, vdict, rlog = data.pkgs, data.np, data.spp, data.pdict, data.pvers, data.vdict, data.rlog
 
         extended_deps = [[Dict{Int,BitVector}() for v0 = 1:(spp[p0]-1)] for p0 = 1:np]
@@ -1149,7 +1142,7 @@ function prune_graph!(graph::Graph; verbose::Bool = false)
     data.pvers = new_pvers
     data.vdict = new_vdict
     # Notes:
-    #   * uuid_to_name, reqs, fixed, eq_classes are unchanged
+    #   * uuid_to_name, eq_classes are unchanged
     #   * pruned and rlog were updated in-place
 
     # Replace old structures with new ones

From 275eb185976676e800801dda4c8d398bd85b2404 Mon Sep 17 00:00:00 2001
From: Carlo Baldassi <carlobaldassi@gmail.com>
Date: Wed, 20 Dec 2017 01:07:26 +0100
Subject: [PATCH 3/9] Implement copy for Graphs

Much faster than deepcopy
---
 src/GraphType.jl | 32 ++++++++++++++++++++++++++++++++
 src/Resolve.jl   |  2 +-
 2 files changed, 33 insertions(+), 1 deletion(-)

diff --git a/src/GraphType.jl b/src/GraphType.jl
index bcef950f6d3bb..852c67115d033 100644
--- a/src/GraphType.jl
+++ b/src/GraphType.jl
@@ -133,8 +133,24 @@ mutable struct GraphData
 
         return data
     end
+
+    function Base.copy(data::GraphData)
+        pkgs = copy(data.pkgs)
+        np = data.np
+        spp = copy(data.spp)
+        pdict = copy(data.pdict)
+        pvers = [copy(data.pvers[p0]) for p0 = 1:np]
+        vdict = [copy(data.vdict[p0]) for p0 = 1:np]
+        uuid_to_name = copy(data.uuid_to_name)
+        pruned = copy(data.pruned)
+        eq_classes = Dict(p => copy(eq) for (p,eq) in data.eq_classes)
+        rlog = deepcopy(data.rlog)
+
+        return new(pkgs, np, spp, pdict, pvers, vdict, uuid_to_name, pruned, eq_classes, rlog)
+    end
 end
 
+
 @enum DepDir FORWARD BACKWARDS BIDIR NONE
 
 function update_depdir(dd0::DepDir, dd1::DepDir)
@@ -303,8 +319,24 @@ mutable struct Graph
 
         return graph
     end
+
+    function Base.copy(graph::Graph)
+        data = copy(graph.data)
+        np = graph.np
+        spp = data.spp
+        gadj = [copy(graph.gadj[p0]) for p0 = 1:np]
+        gmsk = [[copy(graph.gmsk[p0][j0]) for j0 = 1:length(gadj[p0])] for p0 = 1:np]
+        gdir = [copy(graph.gdir[p0]) for p0 = 1:np]
+        gconstr = [copy(graph.gconstr[p0]) for p0 = 1:np]
+        adjdict = [copy(graph.adjdict[p0]) for p0 = 1:np]
+        req_inds = copy(graph.req_inds)
+        fix_inds = copy(graph.fix_inds)
+
+        return new(data, gadj, gmsk, gdir, gconstr, adjdict, req_inds, fix_inds, spp, np)
+    end
 end
 
+
 """
 Add explicit requirements to the graph.
 """
diff --git a/src/Resolve.jl b/src/Resolve.jl
index d4e7b6e46114c..82c10af91f0fa 100644
--- a/src/Resolve.jl
+++ b/src/Resolve.jl
@@ -117,8 +117,8 @@ function sanity_check(graph::Graph, sources::Set{UUID} = Set{UUID}(); verbose::B
         length(gadj[pdict[p]]) == 0 && break
         checked[i] && (i += 1; continue)
 
-        sub_graph = deepcopy(graph)
         req = Requires(p => vn)
+        sub_graph = copy(graph)
         add_reqs!(sub_graph, req)
 
         try

From d35292edc03f6f21e0b7b44439020008107595bc Mon Sep 17 00:00:00 2001
From: Carlo Baldassi <carlobaldassi@gmail.com>
Date: Wed, 20 Dec 2017 01:08:21 +0100
Subject: [PATCH 4/9] Add STDOUT fallback argument to showlog

---
 src/GraphType.jl | 2 ++
 1 file changed, 2 insertions(+)

diff --git a/src/GraphType.jl b/src/GraphType.jl
index 852c67115d033..171ed5c85aff2 100644
--- a/src/GraphType.jl
+++ b/src/GraphType.jl
@@ -713,6 +713,8 @@ function log_event_eq_classes!(graph::Graph, p0::Int)
     return entry
 end
 
+showlog(graph::Graph, args...; kw...) = showlog(STDOUT, graph, args...; kw...)
+
 """
 Show the full resolution log. The `view` keyword controls how the events are displayed/grouped:
 

From 2aa577c984f3a7a945afd12cbbeec23dd7d9dbe7 Mon Sep 17 00:00:00 2001
From: Carlo Baldassi <carlobaldassi@gmail.com>
Date: Wed, 20 Dec 2017 01:15:28 +0100
Subject: [PATCH 5/9] Maxsum decimation builds an explicit solution

Also checks the constraints at decimation, not just the
interaction masks.
Also makes sure that all variables get decimated.
Also builds a trace of the decimation process and returns
that in the error message (preparatory step for future improvements)
---
 src/Resolve.jl        |  7 +---
 src/resolve/MaxSum.jl | 91 ++++++++++++++++++++-----------------------
 test/resolve.jl       |  4 +-
 3 files changed, 47 insertions(+), 55 deletions(-)

diff --git a/src/Resolve.jl b/src/Resolve.jl
index 82c10af91f0fa..1e35b1d3a1f90 100644
--- a/src/Resolve.jl
+++ b/src/Resolve.jl
@@ -32,16 +32,11 @@ function resolve(graph::Graph; verbose::Bool = false)
     catch err
         isa(err, UnsatError) || rethrow(err)
         verbose && info("resolve: maxsum failed")
-        p = graph.data.pkgs[err.info]
+        # p = graph.data.pkgs[err.info]
         # TODO: build tools to analyze the problem, and suggest to use them here.
         msg =
             """
             resolve is unable to satisfy package requirements.
-              The problem was detected when trying to find a feasible version
-              for package $(id(p)).
-              However, this only means that package $(id(p)) is involved in an
-              unsatisfiable or difficult dependency relation, and the root of
-              the problem may be elsewhere.
             """
         if msgs.num_nondecimated != graph.np
             msg *= """
diff --git a/src/resolve/MaxSum.jl b/src/resolve/MaxSum.jl
index 584d44b1cc8f4..e62e53597c6e4 100644
--- a/src/resolve/MaxSum.jl
+++ b/src/resolve/MaxSum.jl
@@ -52,10 +52,13 @@ mutable struct Messages
     # backup of the initial value of fld, to be used when resetting
     initial_fld::Vector{Field}
 
-    # keep track of which variables have been decimated
-    decimated::BitVector
+    # the solution is built progressively by a decimation process
+    solution::Vector{Int}
     num_nondecimated::Int
 
+    # try to build a trace
+    trace::Vector{Any}
+
     function Messages(graph::Graph)
         np = graph.np
         spp = graph.spp
@@ -103,26 +106,13 @@ mutable struct Messages
         gadj = graph.gadj
         msg = [[zeros(FieldValue, spp[p0]) for j1 = 1:length(gadj[p0])] for p0 = 1:np]
 
-        return new(msg, fld, initial_fld, falses(np), np)
-    end
-end
+        solution = zeros(Int, np)
+        num_nondecimated = np
 
-function getsolution(msgs::Messages)
-    # the solution is just the location of the maximum in
-    # each field
+        trace = []
 
-    fld = msgs.fld
-    np = length(fld)
-    sol = Vector{Int}(np)
-    for p0 = 1:np
-        fld0 = fld[p0]
-        s0 = indmax(fld0)
-        if !validmax(fld0[s0])
-            throw(UnsatError(p0))
-        end
-        sol[p0] = s0
+        return new(msg, fld, initial_fld, solution, num_nondecimated, trace)
     end
-    return sol
 end
 
 # This is the core of the max-sum solver:
@@ -137,7 +127,7 @@ function update(p0::Int, graph::Graph, msgs::Messages)
     np = graph.np
     msg = msgs.msg
     fld = msgs.fld
-    decimated = msgs.decimated
+    solution = msgs.solution
 
     maxdiff = zero(FieldValue)
 
@@ -151,7 +141,7 @@ function update(p0::Int, graph::Graph, msgs::Messages)
     for j0 in 1:length(gadj0)
 
         p1 = gadj0[j0]
-        decimated[p1] && continue
+        solution[p1] > 0 && continue # already decimated
         j1 = adjdict0[p1]
         #@assert j0 == adjdict[p1][p0]
         bm1 = gmsk[p1][j1]
@@ -196,7 +186,7 @@ function update(p0::Int, graph::Graph, msgs::Messages)
         if !validmax(m)
             # No state available without violating some
             # hard constraint
-            throw(UnsatError(p1))
+            throw(UnsatError(msgs.trace))
         end
 
         # normalize the new message
@@ -254,17 +244,20 @@ function iterate(graph::Graph, msgs::Messages, perm::NodePerm)
 end
 
 function decimate1(p0::Int, graph::Graph, msgs::Messages)
-    decimated = msgs.decimated
+    solution = msgs.solution
     fld = msgs.fld
     adjdict = graph.adjdict
     gmsk = graph.gmsk
+    gconstr = graph.gconstr
 
-    @assert !decimated[p0]
+    @assert solution[p0] == 0
     fld0 = fld[p0]
     s0 = indmax(fld0)
     # only do the decimation if it is consistent with
-    # the previously decimated nodes
-    for p1 in find(decimated)
+    # the constraints...
+    gconstr[p0][s0] || return false
+    # ...and with the previously decimated nodes
+    for p1 in find(solution .> 0)
         haskey(adjdict[p0], p1) || continue
         s1 = indmax(fld[p1])
         j1 = adjdict[p0][p1]
@@ -275,8 +268,9 @@ function decimate1(p0::Int, graph::Graph, msgs::Messages)
         v0 == s0 && continue
         fld0[v0] = FieldValue(-1)
     end
-    msgs.decimated[p0] = true
+    msgs.solution[p0] = s0
     msgs.num_nondecimated -= 1
+    push!(msgs.trace, (p0,s0))
     return true
 end
 
@@ -284,11 +278,11 @@ function reset_messages!(msgs::Messages)
     msg = msgs.msg
     fld = msgs.fld
     initial_fld = msgs.initial_fld
-    decimated = msgs.decimated
+    solution = msgs.solution
     np = length(fld)
     for p0 = 1:np
         map(m->fill!(m, zero(FieldValue)), msg[p0])
-        decimated[p0] && continue
+        solution[p0] > 0 && continue
         fld[p0] = copy(initial_fld[p0])
     end
     return msgs
@@ -301,33 +295,32 @@ function decimate(n::Int, graph::Graph, msgs::Messages)
     #println("DECIMATING $n NODES")
     adjdict = graph.adjdict
     fld = msgs.fld
-    decimated = msgs.decimated
+    solution = msgs.solution
     fldorder = sortperm(fld, by=secondmax)
     did_dec = false
     for p0 in fldorder
-        decimated[p0] && continue
+        solution[p0] > 0 && continue
         did_dec |= decimate1(p0, graph, msgs)
         n -= 1
         n == 0 && break
     end
     @assert n == 0
-    if !did_dec
-        # did not succeed in decimating anything;
-        # try to decimate at least one node
-        for p0 in fldorder
-            decimated[p0] && continue
-            if decimate1(p0, graph, msgs)
-                did_dec = true
-                break
-            end
-        end
-    end
-    if !did_dec
-        # still didn't succeed, give up
-        p0 = first(fldorder[.~(decimated)])
-        throw(UnsatError(p0))
+
+    did_dec && @goto ok
+
+    # did not succeed in decimating anything;
+    # try to decimate at least one node
+    for p0 in fldorder
+        solution[p0] > 0 && continue
+        decimate1(p0, graph, msgs) && @goto ok
     end
 
+    # still didn't succeed, give up
+    p0 = findfirst(solution .== 0)
+    throw(UnsatError(msgs.trace))
+
+    @label ok
+
     reset_messages!(msgs)
     return
 end
@@ -389,10 +382,12 @@ function maxsum(graph::Graph, msgs::Messages)
     # (old_numnondec is saved just to prevent
     # wrong messages about accuracy)
     old_numnondec = msgs.num_nondecimated
-    decimate(msgs.num_nondecimated, graph, msgs)
+    while msgs.num_nondecimated > 0
+        decimate(msgs.num_nondecimated, graph, msgs)
+    end
     msgs.num_nondecimated = old_numnondec
 
-    return getsolution(msgs)
+    return copy(msgs.solution)
 end
 
 end
diff --git a/test/resolve.jl b/test/resolve.jl
index c95ee23e800f4..f99a3f37a60cb 100644
--- a/test/resolve.jl
+++ b/test/resolve.jl
@@ -197,7 +197,9 @@ function resolve_tst(deps_data, reqs_data, want_data = nothing)
     simplify_graph!(graph, verbose = VERBOSE)
     want = resolve(graph, verbose = VERBOSE)
 
-    # info("BACKTRACE:\n" * sprint(showbacktrace, graph))
+    # info(sprint(io->showlog(io, graph)))
+    # println()
+    # info(sprint(io->showlog(io, graph, view=:chronological)))
 
     return want == wantuuids(want_data)
 end

From 1591c8b6f473e737ead93f577ba49f82b4c9e42b Mon Sep 17 00:00:00 2001
From: Carlo Baldassi <carlobaldassi@gmail.com>
Date: Thu, 21 Dec 2017 13:23:38 +0100
Subject: [PATCH 6/9] Apply maxsum trace, log it, simplify after

Provides meaningful error messages about what happened.

Also, minor cosmetics to resolve logs.
---
 src/GraphType.jl      | 76 ++++++++++++++++++++++++++++---------------
 src/Resolve.jl        | 46 +++++++++++++++++---------
 src/resolve/MaxSum.jl |  2 +-
 3 files changed, 80 insertions(+), 44 deletions(-)

diff --git a/src/GraphType.jl b/src/GraphType.jl
index 171ed5c85aff2..80bfde3438212 100644
--- a/src/GraphType.jl
+++ b/src/GraphType.jl
@@ -525,24 +525,23 @@ function log_event_req!(graph::Graph, rp::UUID, rvs::VersionSpec, reason)
     if reason isa Symbol
         @assert reason == :explicit_requirement
         other_entry = nothing
-        msg *= "an explicit requirement, "
+        msg *= "an explicit requirement"
     else
-        @assert reason isa Tuple{UUID,ResolveLogEntry}
-        other_p, other_entry = reason
+        other_p, other_entry = reason::Tuple{UUID,ResolveLogEntry}
         if other_p == uuid_julia
-            msg *= "julia compatibility requirements, "
-            other_entry = nothing
+            msg *= "julia compatibility requirements"
+            other_entry = nothing # don't propagate the log
         else
             other_id = pkgID(other_p, graph)
-            msg *= "$other_id, "
+            msg *= "$other_id"
         end
     end
     rp0 = pdict[rp]
     @assert !gconstr[rp0][end]
     if any(gconstr[rp0])
-        msg *= "leaving only versions $(VersionSpec(VersionRange.(pvers[rp0][gconstr[rp0][1:(end-1)]])))"
+        msg *= ", leaving only versions $(VersionSpec(VersionRange.(pvers[rp0][gconstr[rp0][1:(end-1)]])))"
     else
-        msg *= "leaving no versions left"
+        msg *= " — no versions left"
     end
     entry = rlog.pool[rp]
     push!(entry, (other_entry, msg))
@@ -559,10 +558,9 @@ function log_event_implicit_req!(graph::Graph, p1::Int, vmask::BitVector, p0::In
         if any(vmask[1:(end-1)])
             vns = string(VersionSpec(VersionRange.(pvers[p0][vmask[1:(end-1)]])))
             vmask[end] && (vns *= " or uninstalled")
-        elseif vmask[end]
-            vns = "uninstalled"
         else
-            vns = "no version"
+            @assert vmask[end]
+            vns = "uninstalled"
         end
         return vns
     end
@@ -582,11 +580,10 @@ function log_event_implicit_req!(graph::Graph, p1::Int, vmask::BitVector, p0::In
         end
         msg *= "to versions: $(vs_string(p1, vmask))"
         if vmask ≠ gconstr[p1]
-            msg *= ", leaving "
             if any(gconstr[p1])
-                msg *= "only versions: $(vs_string(p1, gconstr[p1]))"
+                msg *= ", leaving only versions: $(vs_string(p1, gconstr[p1]))"
             else
-                msg *= "no versions left"
+                msg *= " — no versions left"
             end
         end
     else
@@ -713,6 +710,22 @@ function log_event_eq_classes!(graph::Graph, p0::Int)
     return entry
 end
 
+function log_event_maxsumtrace!(graph::Graph, p0::Int, s0::Int)
+    rlog = graph.data.rlog
+    p = graph.data.pkgs[p0]
+    id = pkgID(p0, graph)
+    if s0 < graph.spp[p0]
+        msg = "fixed by the MaxSum heuristic to version $(graph.data.pvers[p0][s0])"
+    else
+        msg = "determined to be unneeded by the MaxSum heuristic"
+    end
+    entry = rlog.pool[p]
+    push!(entry, (nothing, msg))
+    return entry
+end
+
+const _logindent = " "
+
 showlog(graph::Graph, args...; kw...) = showlog(STDOUT, graph, args...; kw...)
 
 """
@@ -731,8 +744,8 @@ function showlog(io::IO, graph::Graph; view::Symbol = :plain)
     recursive = (view == :tree)
     initentries = [event[1] for event in graph.data.rlog.init.events]
     for entry in sort!(initentries, by=(entry->pkgID(entry.pkg, graph)))
-        _show(io, graph, entry, "", seen, recursive)
-        recursive && (seen[entry] = true)
+        seen[entry] = true
+        _show(io, graph, entry, _logindent, seen, recursive)
     end
 end
 
@@ -752,10 +765,11 @@ the same as for `showlog(io, graph)`); the default is `:tree`.
 function showlog(io::IO, graph::Graph, p::UUID; view::Symbol = :tree)
     view ∈ [:plain, :tree] || throw(ArgumentError("the view argument should be `:plain` or `:tree`"))
     rlog = graph.data.rlog
+    entry = rlog.pool[p]
     if view == :tree
-        _show(io, graph, rlog.pool[p], "", ObjectIdDict(), true)
+        _show(io, graph, entry, _logindent, ObjectIdDict(entry=>true), true)
     else
-        entries = ResolveLogEntry[rlog.pool[p]]
+        entries = ResolveLogEntry[entry]
         function getentries(entry)
             for (other_entry,_) in entry.events
                 (other_entry ≡ nothing || other_entry ∈ entries) && continue
@@ -763,16 +777,16 @@ function showlog(io::IO, graph::Graph, p::UUID; view::Symbol = :tree)
                 getentries(other_entry)
             end
         end
-        getentries(rlog.pool[p])
+        getentries(entry)
         for entry in entries
-            _show(io, graph, entry, "", ObjectIdDict(), false)
+            _show(io, graph, entry, _logindent, ObjectIdDict(), false)
         end
     end
 end
 
 # Show a recursive tree with requirements applied to a package, either directly or indirectly
 function _show(io::IO, graph::Graph, entry::ResolveLogEntry, indent::String, seen::ObjectIdDict, recursive::Bool)
-    toplevel = isempty(indent)
+    toplevel = (indent == _logindent)
     firstglyph = toplevel ? "" : "└─"
     pre = toplevel ? "" : "  "
     println(io, indent, firstglyph, entry.header)
@@ -799,7 +813,7 @@ end
 is_julia(graph::Graph, p0::Int) = graph.data.pkgs[p0] == uuid_julia
 
 "Check for contradictions in the constraints."
-function check_constraints(graph::Graph)
+function check_constraints(graph::Graph; arewesure::Bool = true)
     np = graph.np
     gconstr = graph.gconstr
     pkgs = graph.data.pkgs
@@ -809,7 +823,11 @@ function check_constraints(graph::Graph)
 
     for p0 = 1:np
         any(gconstr[p0]) && continue
-        err_msg = "Unsatisfiable requirements detected for package $(id(p0)):\n"
+        if arewesure
+            err_msg = "Unsatisfiable requirements detected for package $(id(p0)):\n"
+        else
+            err_msg = "Resolve failed to satisfy requirements for package $(id(p0)):\n"
+        end
         err_msg *= sprint(showlog, graph, pkgs[p0])
         throw(PkgError(err_msg))
     end
@@ -821,7 +839,7 @@ Propagates current constraints, determining new implicit constraints.
 Throws an error in case impossible requirements are detected, printing
 a log trace.
 """
-function propagate_constraints!(graph::Graph)
+function propagate_constraints!(graph::Graph; arewesure::Bool = true)
     np = graph.np
     spp = graph.spp
     gadj = graph.gadj
@@ -864,7 +882,11 @@ function propagate_constraints!(graph::Graph)
                     log_event_implicit_req!(graph, p1, added_constr1, p0)
                 end
                 if !any(gconstr1)
-                    err_msg = "Unsatisfiable requirements detected for package $(id(p1)):\n"
+                    if arewesure
+                        err_msg = "Unsatisfiable requirements detected for package $(id(p1)):\n"
+                    else
+                        err_msg = "Resolve failed to satisfy requirements for package $(id(p1)):\n"
+                    end
                     err_msg *= sprint(showlog, graph, pkgs[p1])
                     throw(PkgError(err_msg))
                 end
@@ -1199,8 +1221,8 @@ end
 Simplifies the graph by propagating constraints, disabling unreachable versions, pruning
 and grouping versions into equivalence classes.
 """
-function simplify_graph!(graph::Graph, sources::Set{Int} = Set{Int}(); verbose::Bool = false)
-    propagate_constraints!(graph)
+function simplify_graph!(graph::Graph, sources::Set{Int} = Set{Int}(); verbose::Bool = false, arewesure::Bool = true)
+    propagate_constraints!(graph, arewesure = arewesure)
     disable_unreachable!(graph, sources)
     prune_graph!(graph, verbose = verbose)
     compute_eq_classes!(graph, verbose = verbose)
diff --git a/src/Resolve.jl b/src/Resolve.jl
index 1e35b1d3a1f90..12676b6e83e65 100644
--- a/src/Resolve.jl
+++ b/src/Resolve.jl
@@ -9,7 +9,7 @@ using ..Types
 using ..GraphType
 using .MaxSum
 import ..Types: uuid_julia
-import ..GraphType: is_julia, log_event_greedysolved!, log_event_maxsumsolved!
+import ..GraphType: is_julia, check_constraints, log_event_greedysolved!, log_event_maxsumsolved!, log_event_maxsumtrace!
 
 export resolve, sanity_check
 
@@ -29,25 +29,25 @@ function resolve(graph::Graph; verbose::Bool = false)
 
     try
         sol = maxsum(graph, msgs)
+        @goto check
     catch err
         isa(err, UnsatError) || rethrow(err)
-        verbose && info("resolve: maxsum failed")
-        # p = graph.data.pkgs[err.info]
-        # TODO: build tools to analyze the problem, and suggest to use them here.
-        msg =
-            """
-            resolve is unable to satisfy package requirements.
-            """
-        if msgs.num_nondecimated != graph.np
-            msg *= """
-                     (you may try increasing the value of the JULIA_PKGRESOLVE_ACCURACY
-                      environment variable)
-                   """
-        end
-        ## info("ERROR MESSAGE:\n" * msg)
-        throw(PkgError(msg))
+        apply_maxsum_trace!(graph, err.trace)
     end
 
+    verbose && info("resolve: maxsum failed")
+
+    check_constraints(graph, arewesure = false) # will throw if it fails
+    simplify_graph!(graph, arewesure = false)   # will throw if it fails
+    # NOTE: here it seems like there could be an infinite recursion loop.
+    #       However, if maxsum fails with an empty trace (which could lead to
+    #       the recursion) then the two above checks should be able to
+    #       detect an error. Nevertheless, it's probably better to put some
+    #       kind of failsafe here.
+    return resolve(graph, verbose = verbose)
+
+    @label check
+
     # verify solution (debug code) and enforce its optimality
     @assert verify_solution(sol, graph)
     enforce_optimality!(sol, graph)
@@ -366,4 +366,18 @@ function enforce_optimality!(sol::Vector{Int}, graph::Graph)
     end
 end
 
+function apply_maxsum_trace!(graph::Graph, trace::Vector{Any})
+    np = graph.np
+    spp = graph.spp
+    gconstr = graph.gconstr
+
+    for (p0,s0) in trace
+        new_constr = falses(spp[p0])
+        new_constr[s0] = true
+        old_constr = copy(gconstr[p0])
+        gconstr[p0] .&= new_constr
+        gconstr[p0] ≠ old_constr && log_event_maxsumtrace!(graph, p0, s0)
+    end
+end
+
 end # module
diff --git a/src/resolve/MaxSum.jl b/src/resolve/MaxSum.jl
index e62e53597c6e4..3dcbd6229c31d 100644
--- a/src/resolve/MaxSum.jl
+++ b/src/resolve/MaxSum.jl
@@ -11,7 +11,7 @@ export UnsatError, Messages, maxsum
 # An exception type used internally to signal that an unsatisfiable
 # constraint was detected
 struct UnsatError <: Exception
-    info
+    trace
 end
 
 # Some parameters to drive the decimation process

From e65b076c3079233aec5a03435046841419d2530d Mon Sep 17 00:00:00 2001
From: Carlo Baldassi <carlobaldassi@gmail.com>
Date: Thu, 21 Dec 2017 18:29:34 +0100
Subject: [PATCH 7/9] Add global events to resolve log, remove verbosity

---
 src/GraphType.jl | 77 +++++++++++++++++++++++++++---------------------
 src/Resolve.jl   | 22 +++++++-------
 test/resolve.jl  |  6 ++--
 3 files changed, 58 insertions(+), 47 deletions(-)

diff --git a/src/GraphType.jl b/src/GraphType.jl
index 80bfde3438212..135f801d3dfb2 100644
--- a/src/GraphType.jl
+++ b/src/GraphType.jl
@@ -21,6 +21,8 @@ export Graph, add_reqs!, add_fixed!, simplify_graph!, showlog
 # The `showlog` functions are used for display, and called to create messages
 # in case of resolution errors.
 
+const UUID0 = UUID(UInt128(0))
+
 const ResolveJournal = Vector{Tuple{UUID,String}}
 
 mutable struct ResolveLogEntry
@@ -28,24 +30,29 @@ mutable struct ResolveLogEntry
     pkg::UUID
     header::String
     events::Vector{Tuple{Any,String}} # here Any should ideally be Union{ResolveLogEntry,Void}
-    ResolveLogEntry(journal::ResolveJournal, pkg::UUID, msg::String = "") = new(journal, pkg, msg, [])
+    ResolveLogEntry(journal::ResolveJournal, pkg::UUID, header::String = "") = new(journal, pkg, header, [])
 end
 
-function Base.push!(entry::ResolveLogEntry, reason::Tuple{Union{ResolveLogEntry,Void},String})
+function Base.push!(entry::ResolveLogEntry, reason::Tuple{Union{ResolveLogEntry,Void},String}, to_journal::Bool = true)
     push!(entry.events, reason)
-    entry.pkg ≠ uuid_julia && push!(entry.journal, (entry.pkg, reason[2]))
+    to_journal && entry.pkg ≠ uuid_julia && push!(entry.journal, (entry.pkg, reason[2]))
     return entry
 end
 
-# Note: the `init` field is used to keep track of all entries which were there
-# at the beginning, since the `pool` can be pruned during the resolution process.
+# Note: the `init` field is used to keep track of all package entries which were
+# created during intialization, since the `pool` can be pruned during the resolution
+# process.
 mutable struct ResolveLog
     init::ResolveLogEntry
+    globals::ResolveLogEntry
     pool::Dict{UUID,ResolveLogEntry}
     journal::Vector{Tuple{UUID,String}}
+    exact::Bool
     function ResolveLog()
         journal = ResolveJournal()
-        return new(ResolveLogEntry(journal, uuid_julia), Dict(), journal)
+        init = ResolveLogEntry(journal, UUID0, "")
+        globals = ResolveLogEntry(journal, UUID0, "Global events:")
+        return new(init, globals, Dict(), journal, true)
     end
 end
 
@@ -500,7 +507,7 @@ function init_log!(data::GraphData)
 
         if p ≠ uuid_julia
             push!(first_entry, (nothing, msg))
-            push!(rlog.init, (first_entry, ""))
+            push!(rlog.init, (first_entry, ""), false)
         end
     end
     return data
@@ -548,6 +555,11 @@ function log_event_req!(graph::Graph, rp::UUID, rvs::VersionSpec, reason)
     return entry
 end
 
+function log_event_global!(graph::Graph, msg::String)
+    rlog = graph.data.rlog
+    push!(rlog.globals, (nothing, msg))
+end
+
 function log_event_implicit_req!(graph::Graph, p1::Int, vmask::BitVector, p0::Int)
     rlog = graph.data.rlog
     gconstr = graph.gconstr
@@ -712,6 +724,7 @@ end
 
 function log_event_maxsumtrace!(graph::Graph, p0::Int, s0::Int)
     rlog = graph.data.rlog
+    rlog.exact = false
     p = graph.data.pkgs[p0]
     id = pkgID(p0, graph)
     if s0 < graph.spp[p0]
@@ -742,6 +755,7 @@ function showlog(io::IO, graph::Graph; view::Symbol = :plain)
     view == :chronological && return showlogjournal(io, graph)
     seen = ObjectIdDict()
     recursive = (view == :tree)
+    _show(io, graph, graph.data.rlog.globals, _logindent, seen, false)
     initentries = [event[1] for event in graph.data.rlog.init.events]
     for entry in sort!(initentries, by=(entry->pkgID(entry.pkg, graph)))
         seen[entry] = true
@@ -751,9 +765,10 @@ end
 
 function showlogjournal(io::IO, graph::Graph)
     journal = graph.data.rlog.journal
-    padding = maximum(length(pkgID(p, graph)) for (p,_) in journal)
+    id(p) = p == UUID0 ? "[global event]" : pkgID(p, graph)
+    padding = maximum(length(id(p)) for (p,_) in journal)
     for (p, msg) in journal
-        println(io, ' ', rpad(pkgID(p, graph), padding), ": ", msg)
+        println(io, ' ', rpad(id(p), padding), ": ", msg)
     end
 end
 
@@ -813,17 +828,18 @@ end
 is_julia(graph::Graph, p0::Int) = graph.data.pkgs[p0] == uuid_julia
 
 "Check for contradictions in the constraints."
-function check_constraints(graph::Graph; arewesure::Bool = true)
+function check_constraints(graph::Graph)
     np = graph.np
     gconstr = graph.gconstr
     pkgs = graph.data.pkgs
     pvers = graph.data.pvers
+    exact = graph.data.rlog.exact
 
     id(p0::Int) = pkgID(p0, graph)
 
     for p0 = 1:np
         any(gconstr[p0]) && continue
-        if arewesure
+        if exact
             err_msg = "Unsatisfiable requirements detected for package $(id(p0)):\n"
         else
             err_msg = "Resolve failed to satisfy requirements for package $(id(p0)):\n"
@@ -839,7 +855,7 @@ Propagates current constraints, determining new implicit constraints.
 Throws an error in case impossible requirements are detected, printing
 a log trace.
 """
-function propagate_constraints!(graph::Graph; arewesure::Bool = true)
+function propagate_constraints!(graph::Graph)
     np = graph.np
     spp = graph.spp
     gadj = graph.gadj
@@ -849,9 +865,12 @@ function propagate_constraints!(graph::Graph; arewesure::Bool = true)
     pkgs = graph.data.pkgs
     pvers = graph.data.pvers
     rlog = graph.data.rlog
+    exact = rlog.exact
 
     id(p0::Int) = pkgID(pkgs[p0], graph)
 
+    log_event_global!(graph, "propagating constraints")
+
     # packages which are not allowed to be uninstalled
     staged = Set{Int}(p0 for p0 = 1:np if !gconstr[p0][end])
 
@@ -882,7 +901,7 @@ function propagate_constraints!(graph::Graph; arewesure::Bool = true)
                     log_event_implicit_req!(graph, p1, added_constr1, p0)
                 end
                 if !any(gconstr1)
-                    if arewesure
+                    if exact
                         err_msg = "Unsatisfiable requirements detected for package $(id(p1)):\n"
                     else
                         err_msg = "Resolve failed to satisfy requirements for package $(id(p1)):\n"
@@ -910,6 +929,8 @@ function disable_unreachable!(graph::Graph, sources::Set{Int} = Set{Int}())
     adjdict = graph.adjdict
     pkgs = graph.data.pkgs
 
+    log_event_global!(graph, "disabling unreachable nodes")
+
     # packages which are not allowed to be uninstalled
     staged = union(sources, Set{Int}(p0 for p0 = 1:np if !gconstr[p0][end]))
     seen = copy(staged)
@@ -944,20 +965,16 @@ Reduce the number of versions in the graph by putting all the versions of
 a package that behave identically into equivalence classes, keeping only
 the highest version of the class as representative.
 """
-function compute_eq_classes!(graph::Graph; verbose::Bool = false)
+function compute_eq_classes!(graph::Graph)
+    log_event_global!(graph, "computing version equivalence classes")
+
     np = graph.np
     sumspp = sum(graph.spp)
     for p0 = 1:np
         build_eq_classes1!(graph, p0)
     end
 
-    if verbose
-        info("""
-             EQ CLASSES STATS:
-               before: $(sumspp)
-               after:  $(sum(graph.spp))
-             """)
-    end
+    log_event_global!(graph, "computed version equivalence classes, stats (total n. of states): before = $(sumspp) after = $(sum(graph.spp))")
 
     @assert check_consistency(graph)
 
@@ -1039,7 +1056,7 @@ end
 Prune away fixed and unnecessary packages, and the
 disallowed versions for the remaining packages.
 """
-function prune_graph!(graph::Graph; verbose::Bool = false)
+function prune_graph!(graph::Graph)
     np = graph.np
     spp = graph.spp
     gadj = graph.gadj
@@ -1182,13 +1199,7 @@ function prune_graph!(graph::Graph; verbose::Bool = false)
 
     # Done
 
-    if verbose
-        info("""
-             GRAPH SIMPLIFY STATS:
-               before: np = $np ⟨spp⟩ = $(mean(spp))
-               after:  np = $new_np ⟨spp⟩ = $(mean(new_spp))
-             """)
-    end
+    log_event_global!(graph, "pruned graph — stats (n. of packages, mean connectivity): before = ($np,$(mean(spp))) after = ($new_np,$(mean(new_spp)))")
 
     # Replace old data with new
     data.pkgs = new_pkgs
@@ -1221,11 +1232,11 @@ end
 Simplifies the graph by propagating constraints, disabling unreachable versions, pruning
 and grouping versions into equivalence classes.
 """
-function simplify_graph!(graph::Graph, sources::Set{Int} = Set{Int}(); verbose::Bool = false, arewesure::Bool = true)
-    propagate_constraints!(graph, arewesure = arewesure)
+function simplify_graph!(graph::Graph, sources::Set{Int} = Set{Int}())
+    propagate_constraints!(graph)
     disable_unreachable!(graph, sources)
-    prune_graph!(graph, verbose = verbose)
-    compute_eq_classes!(graph, verbose = verbose)
+    prune_graph!(graph)
+    compute_eq_classes!(graph)
     return graph
 end
 
diff --git a/src/Resolve.jl b/src/Resolve.jl
index 12676b6e83e65..337d5ef1eb8dd 100644
--- a/src/Resolve.jl
+++ b/src/Resolve.jl
@@ -9,12 +9,12 @@ using ..Types
 using ..GraphType
 using .MaxSum
 import ..Types: uuid_julia
-import ..GraphType: is_julia, check_constraints, log_event_greedysolved!, log_event_maxsumsolved!, log_event_maxsumtrace!
+import ..GraphType: is_julia, check_constraints, log_event_global!, log_event_greedysolved!, log_event_maxsumsolved!, log_event_maxsumtrace!
 
 export resolve, sanity_check
 
 "Resolve package dependencies."
-function resolve(graph::Graph; verbose::Bool = false)
+function resolve(graph::Graph)
     id(p) = pkgID(p, graph)
 
     # attempt trivial solution first
@@ -22,7 +22,7 @@ function resolve(graph::Graph; verbose::Bool = false)
 
     ok && @goto solved
 
-    verbose && info("resolve: greedy failed")
+    log_event_global!(graph, "greedy solver failed")
 
     # trivial solution failed, use maxsum solver
     msgs = Messages(graph)
@@ -35,16 +35,16 @@ function resolve(graph::Graph; verbose::Bool = false)
         apply_maxsum_trace!(graph, err.trace)
     end
 
-    verbose && info("resolve: maxsum failed")
+    log_event_global!(graph, "maxsum solver failed")
 
-    check_constraints(graph, arewesure = false) # will throw if it fails
-    simplify_graph!(graph, arewesure = false)   # will throw if it fails
+    check_constraints(graph) # will throw if it fails
+    simplify_graph!(graph)   # will throw if it fails
     # NOTE: here it seems like there could be an infinite recursion loop.
     #       However, if maxsum fails with an empty trace (which could lead to
     #       the recursion) then the two above checks should be able to
     #       detect an error. Nevertheless, it's probably better to put some
     #       kind of failsafe here.
-    return resolve(graph, verbose = verbose)
+    return resolve(graph)
 
     @label check
 
@@ -54,7 +54,7 @@ function resolve(graph::Graph; verbose::Bool = false)
 
     @label solved
 
-    verbose && info("resolve: succeeded")
+    log_event_global!(graph, "the solver found a feasible configuration")
 
     # return the solution as a Dict mapping UUID => VersionNumber
     return compute_output_dict(sol, graph)
@@ -64,7 +64,7 @@ end
 Scan the graph for (explicit or implicit) contradictions. Returns a list of problematic
 (package,version) combinations.
 """
-function sanity_check(graph::Graph, sources::Set{UUID} = Set{UUID}(); verbose::Bool = false)
+function sanity_check(graph::Graph, sources::Set{UUID} = Set{UUID}())
     req_inds = graph.req_inds
     fix_inds = graph.fix_inds
 
@@ -83,7 +83,7 @@ function sanity_check(graph::Graph, sources::Set{UUID} = Set{UUID}(); verbose::B
         Set{Int}(1:graph.np) :
         Set{Int}(graph.data.pdict[p] for p in sources)
 
-    simplify_graph!(graph, isources, verbose = verbose)
+    simplify_graph!(graph, isources)
 
     np = graph.np
     spp = graph.spp
@@ -117,7 +117,7 @@ function sanity_check(graph::Graph, sources::Set{UUID} = Set{UUID}(); verbose::B
         add_reqs!(sub_graph, req)
 
         try
-            simplify_graph!(sub_graph, verbose = verbose)
+            simplify_graph!(sub_graph)
         catch err
             isa(err, PkgError) || rethrow(err)
             ## info("ERROR MESSAGE:\n" * err.msg)
diff --git a/test/resolve.jl b/test/resolve.jl
index f99a3f37a60cb..ed696ed24ce91 100644
--- a/test/resolve.jl
+++ b/test/resolve.jl
@@ -172,7 +172,7 @@ function sanity_tst(deps_data, expected_result; pkgs=[])
         @show deps_data
         @show pkgs
     end
-    result = sanity_check(graph, Set(pkguuid(p) for p in pkgs), verbose = VERBOSE)
+    result = sanity_check(graph, Set(pkguuid(p) for p in pkgs))
 
     length(result) == length(expected_result) || return false
     expected_result_uuid = [(id(p), vn) for (p,vn) in expected_result]
@@ -194,8 +194,8 @@ function resolve_tst(deps_data, reqs_data, want_data = nothing)
     reqs = reqs_from_data(reqs_data, graph)
     add_reqs!(graph, reqs)
 
-    simplify_graph!(graph, verbose = VERBOSE)
-    want = resolve(graph, verbose = VERBOSE)
+    simplify_graph!(graph)
+    want = resolve(graph)
 
     # info(sprint(io->showlog(io, graph)))
     # println()

From 7b636b516b4fc839226fd65d9b23e8edfadbb85f Mon Sep 17 00:00:00 2001
From: Carlo Baldassi <carlobaldassi@gmail.com>
Date: Thu, 21 Dec 2017 21:32:52 +0100
Subject: [PATCH 8/9] Make resolve log detachable

---
 src/GraphType.jl | 101 ++++++++++++++++++++++++++++-------------------
 test/resolve.jl  |   5 ++-
 2 files changed, 63 insertions(+), 43 deletions(-)

diff --git a/src/GraphType.jl b/src/GraphType.jl
index 135f801d3dfb2..53d8c810cbf0e 100644
--- a/src/GraphType.jl
+++ b/src/GraphType.jl
@@ -6,7 +6,7 @@ using ..Types
 import ..Types.uuid_julia
 import Pkg3.equalto
 
-export Graph, add_reqs!, add_fixed!, simplify_graph!, showlog
+export Graph, ResolveLog, add_reqs!, add_fixed!, simplify_graph!, get_resolve_log, showlog
 
 # The ResolveLog is used to keep track of events that take place during the
 # resolution process. We use one ResolveLogEntry per package, and record all events
@@ -39,20 +39,33 @@ function Base.push!(entry::ResolveLogEntry, reason::Tuple{Union{ResolveLogEntry,
     return entry
 end
 
-# Note: the `init` field is used to keep track of all package entries which were
-# created during intialization, since the `pool` can be pruned during the resolution
-# process.
 mutable struct ResolveLog
+    # init: used to keep track of all package entries which were created during
+    #       intialization, since the `pool` can be pruned during the resolution
+    #       process.
     init::ResolveLogEntry
+
+    # globals: records global events not associated to any particular package
     globals::ResolveLogEntry
+
+    # pool: records entries associated to each package
     pool::Dict{UUID,ResolveLogEntry}
+
+    # journal: record all messages in order (shared between all entries)
     journal::Vector{Tuple{UUID,String}}
+
+    # exact: keeps track of whether the resolve process is still exact, or
+    #        heuristics have been employed
     exact::Bool
-    function ResolveLog()
+
+    # UUID to names
+    uuid_to_name::Dict{UUID,String}
+
+    function ResolveLog(uuid_to_name::Dict{UUID,String})
         journal = ResolveJournal()
         init = ResolveLogEntry(journal, UUID0, "")
         globals = ResolveLogEntry(journal, UUID0, "Global events:")
-        return new(init, globals, Dict(), journal, true)
+        return new(init, globals, Dict(), journal, true, uuid_to_name)
     end
 end
 
@@ -132,7 +145,7 @@ mutable struct GraphData
         eq_classes = Dict(pkgs[p0] => Dict(eq_vn(v0,p0) => Set([eq_vn(v0,p0)]) for v0 = 1:spp[p0]) for p0 = 1:np)
 
         # the resolution log is actually initialized below
-        rlog = ResolveLog()
+        rlog = ResolveLog(uuid_to_name)
 
         data = new(pkgs, np, spp, pdict, pvers, vdict, uuid_to_name, pruned, eq_classes, rlog)
 
@@ -148,10 +161,10 @@ mutable struct GraphData
         pdict = copy(data.pdict)
         pvers = [copy(data.pvers[p0]) for p0 = 1:np]
         vdict = [copy(data.vdict[p0]) for p0 = 1:np]
-        uuid_to_name = copy(data.uuid_to_name)
         pruned = copy(data.pruned)
         eq_classes = Dict(p => copy(eq) for (p,eq) in data.eq_classes)
         rlog = deepcopy(data.rlog)
+        uuid_to_name = rlog.uuid_to_name
 
         return new(pkgs, np, spp, pdict, pvers, vdict, uuid_to_name, pruned, eq_classes, rlog)
     end
@@ -407,6 +420,7 @@ function _add_fixed!(graph::Graph, fixed::Dict{UUID,Fixed})
     return graph
 end
 
+Types.pkgID(p::UUID, rlog::ResolveLog) = pkgID(p, rlog.uuid_to_name)
 Types.pkgID(p::UUID, data::GraphData) = pkgID(p, data.uuid_to_name)
 Types.pkgID(p0::Int, data::GraphData) = pkgID(data.pkgs[p0], data)
 Types.pkgID(p, graph::Graph) = pkgID(p, graph.data)
@@ -515,7 +529,7 @@ end
 
 function log_event_fixed!(graph::Graph, fp::UUID, fx::Fixed)
     rlog = graph.data.rlog
-    id = pkgID(fp, graph)
+    id = pkgID(fp, rlog)
     msg = "$id is fixed to version $(fx.version)"
     entry = rlog.pool[fp]
     push!(entry, (nothing, msg))
@@ -527,7 +541,7 @@ function log_event_req!(graph::Graph, rp::UUID, rvs::VersionSpec, reason)
     gconstr = graph.gconstr
     pdict = graph.data.pdict
     pvers = graph.data.pvers
-    id = pkgID(rp, graph)
+    id = pkgID(rp, rlog)
     msg = "restricted to versions $rvs by "
     if reason isa Symbol
         @assert reason == :explicit_requirement
@@ -539,7 +553,7 @@ function log_event_req!(graph::Graph, rp::UUID, rvs::VersionSpec, reason)
             msg *= "julia compatibility requirements"
             other_entry = nothing # don't propagate the log
         else
-            other_id = pkgID(other_p, graph)
+            other_id = pkgID(other_p, rlog)
             msg *= "$other_id"
         end
     end
@@ -578,16 +592,16 @@ function log_event_implicit_req!(graph::Graph, p1::Int, vmask::BitVector, p0::In
     end
 
     p = pkgs[p1]
-    id = pkgID(p, graph)
+    id = pkgID(p, rlog)
     other_p, other_entry = pkgs[p0], rlog.pool[pkgs[p0]]
-    other_id = pkgID(other_p, graph)
+    other_id = pkgID(other_p, rlog)
     if any(vmask)
         msg = "restricted by "
         if other_p == uuid_julia
             msg *= "julia compatibility requirements "
             other_entry = nothing # don't propagate the log
         else
-            other_id = pkgID(other_p, graph)
+            other_id = pkgID(other_p, rlog)
             msg *= "compatibility requirements with $other_id "
         end
         msg *= "to versions: $(vs_string(p1, vmask))"
@@ -604,7 +618,7 @@ function log_event_implicit_req!(graph::Graph, p1::Int, vmask::BitVector, p0::In
             msg *= "julia"
             other_entry = nothing # don't propagate the log
         else
-            other_id = pkgID(other_p, graph)
+            other_id = pkgID(other_p, rlog)
             msg *= "$other_id "
         end
     end
@@ -620,7 +634,7 @@ function log_event_pruned!(graph::Graph, p0::Int, s0::Int)
     pvers = graph.data.pvers
 
     p = pkgs[p0]
-    id = pkgID(p, graph)
+    id = pkgID(p, rlog)
     if s0 == spp[p0]
         msg = "determined to be unneeded during graph pruning"
     else
@@ -638,7 +652,7 @@ function log_event_greedysolved!(graph::Graph, p0::Int, s0::Int)
     pvers = graph.data.pvers
 
     p = pkgs[p0]
-    id = pkgID(p, graph)
+    id = pkgID(p, rlog)
     if s0 == spp[p0]
         msg = "determined to be unneeded by the solver"
     else
@@ -660,7 +674,7 @@ function log_event_maxsumsolved!(graph::Graph, p0::Int, s0::Int, why::Symbol)
     pvers = graph.data.pvers
 
     p = pkgs[p0]
-    id = pkgID(p, graph)
+    id = pkgID(p, rlog)
     if s0 == spp[p0]
         @assert why == :uninst
         msg = "determined to be unneeded by the solver"
@@ -684,8 +698,8 @@ function log_event_maxsumsolved!(graph::Graph, p0::Int, s0::Int, p1::Int)
     pvers = graph.data.pvers
 
     p = pkgs[p0]
-    id = pkgID(p, graph)
-    other_id = pkgID(p1, graph)
+    id = pkgID(p, rlog)
+    other_id = pkgID(pkgs[p1], rlog)
     @assert s0 ≠ spp[p0]
     if s0 == spp[p0] - 1
         msg = "set by the solver to its maximum version: $(pvers[p0][s0]) (installation is required by $other_id)"
@@ -715,7 +729,7 @@ function log_event_eq_classes!(graph::Graph, p0::Int)
     end
 
     p = pkgs[p0]
-    id = pkgID(p, graph)
+    id = pkgID(p, rlog)
     msg = "versions reduced by equivalence to: $vns"
     entry = rlog.pool[p]
     push!(entry, (nothing, msg))
@@ -726,7 +740,7 @@ function log_event_maxsumtrace!(graph::Graph, p0::Int, s0::Int)
     rlog = graph.data.rlog
     rlog.exact = false
     p = graph.data.pkgs[p0]
-    id = pkgID(p0, graph)
+    id = pkgID(p, rlog)
     if s0 < graph.spp[p0]
         msg = "fixed by the MaxSum heuristic to version $(graph.data.pvers[p0][s0])"
     else
@@ -737,9 +751,14 @@ function log_event_maxsumtrace!(graph::Graph, p0::Int, s0::Int)
     return entry
 end
 
+"Get the resolution log, detached"
+get_resolve_log(graph::Graph) = deepcopy(graph.data.rlog)
+
 const _logindent = " "
 
 showlog(graph::Graph, args...; kw...) = showlog(STDOUT, graph, args...; kw...)
+showlog(io::IO, graph::Graph, args...; kw...) = showlog(io, graph.data.rlog, args...; kw...)
+showlog(rlog::ResolveLog, args...; kw...) = showlog(STDOUT, rlog, args...; kw...)
 
 """
 Show the full resolution log. The `view` keyword controls how the events are displayed/grouped:
@@ -749,25 +768,25 @@ Show the full resolution log. The `view` keyword controls how the events are dis
            in the process (the top-level is still grouped by package, alphabetically)
  * `:chronological` for a flat view of all events in chronological order
 """
-function showlog(io::IO, graph::Graph; view::Symbol = :plain)
+function showlog(io::IO, rlog::ResolveLog; view::Symbol = :plain)
     view ∈ [:plain, :tree, :chronological] || throw(ArgumentError("the view argument should be `:plain`, `:tree` or `:chronological`"))
     println(io, "Resolve log:")
-    view == :chronological && return showlogjournal(io, graph)
+    view == :chronological && return showlogjournal(io, rlog)
     seen = ObjectIdDict()
     recursive = (view == :tree)
-    _show(io, graph, graph.data.rlog.globals, _logindent, seen, false)
-    initentries = [event[1] for event in graph.data.rlog.init.events]
-    for entry in sort!(initentries, by=(entry->pkgID(entry.pkg, graph)))
+    _show(io, rlog, rlog.globals, _logindent, seen, false)
+    initentries = [event[1] for event in rlog.init.events]
+    for entry in sort!(initentries, by=(entry->pkgID(entry.pkg, rlog)))
         seen[entry] = true
-        _show(io, graph, entry, _logindent, seen, recursive)
+        _show(io, rlog, entry, _logindent, seen, recursive)
     end
 end
 
-function showlogjournal(io::IO, graph::Graph)
-    journal = graph.data.rlog.journal
-    id(p) = p == UUID0 ? "[global event]" : pkgID(p, graph)
+function showlogjournal(io::IO, rlog::ResolveLog)
+    journal = rlog.journal
+    id(p) = p == UUID0 ? "[global event]" : pkgID(p, rlog)
     padding = maximum(length(id(p)) for (p,_) in journal)
-    for (p, msg) in journal
+    for (p,msg) in journal
         println(io, ' ', rpad(id(p), padding), ": ", msg)
     end
 end
@@ -775,14 +794,13 @@ end
 """
 Show the resolution log for some package, and all the other packages that affected
 it during resolution. The `view` option can be either `:plain` or `:tree` (works
-the same as for `showlog(io, graph)`); the default is `:tree`.
+the same as for `showlog(io, rlog)`); the default is `:tree`.
 """
-function showlog(io::IO, graph::Graph, p::UUID; view::Symbol = :tree)
+function showlog(io::IO, rlog::ResolveLog, p::UUID; view::Symbol = :tree)
     view ∈ [:plain, :tree] || throw(ArgumentError("the view argument should be `:plain` or `:tree`"))
-    rlog = graph.data.rlog
     entry = rlog.pool[p]
     if view == :tree
-        _show(io, graph, entry, _logindent, ObjectIdDict(entry=>true), true)
+        _show(io, rlog, entry, _logindent, ObjectIdDict(entry=>true), true)
     else
         entries = ResolveLogEntry[entry]
         function getentries(entry)
@@ -794,13 +812,13 @@ function showlog(io::IO, graph::Graph, p::UUID; view::Symbol = :tree)
         end
         getentries(entry)
         for entry in entries
-            _show(io, graph, entry, _logindent, ObjectIdDict(), false)
+            _show(io, rlog, entry, _logindent, ObjectIdDict(), false)
         end
     end
 end
 
 # Show a recursive tree with requirements applied to a package, either directly or indirectly
-function _show(io::IO, graph::Graph, entry::ResolveLogEntry, indent::String, seen::ObjectIdDict, recursive::Bool)
+function _show(io::IO, rlog::ResolveLog, entry::ResolveLogEntry, indent::String, seen::ObjectIdDict, recursive::Bool)
     toplevel = (indent == _logindent)
     firstglyph = toplevel ? "" : "└─"
     pre = toplevel ? "" : "  "
@@ -821,7 +839,7 @@ function _show(io::IO, graph::Graph, entry::ResolveLogEntry, indent::String, see
             continue
         end
         seen[otheritem] = true
-        _show(io, graph, otheritem, newindent, seen, recursive)
+        _show(io, rlog, otheritem, newindent, seen, recursive)
     end
 end
 
@@ -833,6 +851,7 @@ function check_constraints(graph::Graph)
     gconstr = graph.gconstr
     pkgs = graph.data.pkgs
     pvers = graph.data.pvers
+    rlog = graph.data.rlog
     exact = graph.data.rlog.exact
 
     id(p0::Int) = pkgID(p0, graph)
@@ -844,7 +863,7 @@ function check_constraints(graph::Graph)
         else
             err_msg = "Resolve failed to satisfy requirements for package $(id(p0)):\n"
         end
-        err_msg *= sprint(showlog, graph, pkgs[p0])
+        err_msg *= sprint(showlog, rlog, pkgs[p0])
         throw(PkgError(err_msg))
     end
     return true
@@ -906,7 +925,7 @@ function propagate_constraints!(graph::Graph)
                     else
                         err_msg = "Resolve failed to satisfy requirements for package $(id(p1)):\n"
                     end
-                    err_msg *= sprint(showlog, graph, pkgs[p1])
+                    err_msg *= sprint(showlog, rlog, pkgs[p1])
                     throw(PkgError(err_msg))
                 end
             end
diff --git a/test/resolve.jl b/test/resolve.jl
index ed696ed24ce91..aa51d933fda85 100644
--- a/test/resolve.jl
+++ b/test/resolve.jl
@@ -197,9 +197,10 @@ function resolve_tst(deps_data, reqs_data, want_data = nothing)
     simplify_graph!(graph)
     want = resolve(graph)
 
-    # info(sprint(io->showlog(io, graph)))
+    # rlog = get_resolve_log(graph)
+    # info(sprint(io->showlog(io, rlog)))
     # println()
-    # info(sprint(io->showlog(io, graph, view=:chronological)))
+    # info(sprint(io->showlog(io, rlog, view=:chronological)))
 
     return want == wantuuids(want_data)
 end

From 698be150575c40f75d9864f12fd7a5a4a604ba60 Mon Sep 17 00:00:00 2001
From: Carlo Baldassi <carlobaldassi@gmail.com>
Date: Thu, 21 Dec 2017 21:56:15 +0100
Subject: [PATCH 9/9] Add (optional) progress report in sanity_check

---
 src/Resolve.jl  | 13 ++++++++++++-
 test/resolve.jl |  2 +-
 2 files changed, 13 insertions(+), 2 deletions(-)

diff --git a/src/Resolve.jl b/src/Resolve.jl
index 337d5ef1eb8dd..fe489588d24e2 100644
--- a/src/Resolve.jl
+++ b/src/Resolve.jl
@@ -64,7 +64,7 @@ end
 Scan the graph for (explicit or implicit) contradictions. Returns a list of problematic
 (package,version) combinations.
 """
-function sanity_check(graph::Graph, sources::Set{UUID} = Set{UUID}())
+function sanity_check(graph::Graph, sources::Set{UUID} = Set{UUID}(); verbose = true)
     req_inds = graph.req_inds
     fix_inds = graph.fix_inds
 
@@ -107,8 +107,18 @@ function sanity_check(graph::Graph, sources::Set{UUID} = Set{UUID}())
 
     checked = falses(nv)
 
+    last_str_len = 0
+
     i = 1
     for (p,vn) in vers
+        if verbose
+            frac_compl = i / nv
+            print("\r", " "^last_str_len)
+            progr_msg = @sprintf("\r%.3i/%.3i (%i%%) — problematic so far: %i", i, nv, round(Int, 100 * frac_compl), length(problematic))
+            print(progr_msg)
+            last_str_len = length(progr_msg)
+        end
+
         length(gadj[pdict[p]]) == 0 && break
         checked[i] && (i += 1; continue)
 
@@ -156,6 +166,7 @@ function sanity_check(graph::Graph, sources::Set{UUID} = Set{UUID}())
 
         i += 1
     end
+    verbose && println()
 
     return sort!(problematic)
 end
diff --git a/test/resolve.jl b/test/resolve.jl
index aa51d933fda85..ed9d18691b91b 100644
--- a/test/resolve.jl
+++ b/test/resolve.jl
@@ -172,7 +172,7 @@ function sanity_tst(deps_data, expected_result; pkgs=[])
         @show deps_data
         @show pkgs
     end
-    result = sanity_check(graph, Set(pkguuid(p) for p in pkgs))
+    result = sanity_check(graph, Set(pkguuid(p) for p in pkgs), verbose = VERBOSE)
 
     length(result) == length(expected_result) || return false
     expected_result_uuid = [(id(p), vn) for (p,vn) in expected_result]