fix: keep Lake workspace axioms out of library imports

[kim-em]

Library code needed module traversal and summary cache checks, but those utilities shared files with Lake workspace loading. Importing the utilities therefore also loaded Lake.Config.Workspace / Lake.Load.Workspace and their build axioms. Private imports still load these dependencies when the importing file does not use module, as with ordinary import Mathlib.

This PR cuts those dependencies:

• Move traversal utilities from ImportGraph.Lake to ImportGraph.Util.Modules and switch library callers to that module.
• Move cache checks from Summary.Lake to Summary.Cache and switch Summary.Get to that module.

Workspace loading remains available to the workspace-summary executable. The library import closure no longer includes it, so ordinary import Mathlib no longer loads Lake’s build axioms.

Zulip discussion

🤖 Prepared with Codex

[thorimur]

Aha, this looks good to me, thanks, and sorry again about this!

The one small comment I have is that in the tests, I'd worry that the ImportGraph and Lake files we want to ensure are not imported might not exist under the provided names in the future if refactoring occurs, which would render the test silently ineffective.

Instead of ensuring certain module names aren't imported, maybe it would make sense to ensure stable public-facing declarations from them are not present, e.g. using assert_not_exists Lake.Workspace and others, for example?

(I also considered suggesting just explicitly logging all Lake.* imports, but it turns out there are a bunch of Lake.Util.* files, so this might not be stable.)