fix: resolve module sources via search paths in findTransitiveImportsFromSource

[josaum]

Fixes #150.

findTransitiveImportsFromSource resolved each module to a working-directory-relative path via modToRelFilePath and silently skipped it if no file existed there, so the returned NameSet could be an incomplete closure with no indication that anything was missed. This bit in the two situations described in the issue: imports from Lake dependency packages (whose sources live under .lake/packages/...), and invocations from a directory other than the package root — e.g. running it on ImportGraph/Imports/FromSource.lean from a package root used to return just Lean.Elab.ParseImportsFast with none of that module's own transitive imports.

Changes

• New public helper findModuleSource? (mod : Name) : IO (Option FilePath), which locates a module's source by trying, in order:
  1. the source search path (Lean.getSrcSearchPath) — LEAN_SRC_PATH, which under lake exe / lake env contains the source directories of every workspace package (including dependencies), plus the toolchain's own src/lean directory, so core modules resolve too;
  2. the .olean search path (LEAN_PATH);
  3. the previous working-directory-relative path.
• findTransitiveImportsFromSource uses it for traversal; modules whose source still cannot be found are collected and reported by throwing an IO.userError listing them, instead of being silently treated as leaves. The function signature is unchanged, and callers whose modules all resolve see no behavioural change (Mathlib's lint-style use, run from the repo root with rootFilter := some \Mathlib`, is unaffected: every traversed module resolves).
• The docstring now also documents that rootFilter prunes the traversal itself rather than filtering the final result, as suggested in the issue.
• Regression tests in ImportGraphTest/FromSource.lean: source-search-path resolution of a toolchain module, closure extending beyond a file's direct imports, none for an unresolvable module, and the error raised when traversal hits an unresolvable module.

Verification

Locally against the pinned toolchain (leanprover/lean4:v4.35.0): lake build passes, lake exe graph --help works, and lake build ImportGraphTest passes for every target except the pre-existing ImportGraphTest.AnotherFileWithTransitiveImports, which exceeds my sandbox's memory limit (OOM-kill, exit 137) identically on unmodified main, so it is unrelated to this change. A probe under lake env confirms Cli.Basic resolves to .lake/packages/Cli/Cli/Basic.lean and Lean.Parser.Module to the toolchain's src/lean. No sorry/admit anywhere.