Feature Request - Check for disconnected dependency graph

Based off this discussion it would be nice to check for and report on a disconnected dependency graph. A simple pass/fail signal would be useful, but one could imagine a more rich report including:

• Cycle detection, as suggested here
• Declarations not in the dependency tree of a specified 'main theorem'