Avoid dependency on Lake in CurrentModule

[jtristan]

The use of the definition Lake.Manifest.load? creates a dependency on Lake. For work that needs todo reverse FII with Mathlib, it is an issue because Lean doesn't create a dynamic library for the Lake library. It is possible to work around it, but it is less than ideal. Perhaps the use of this definition could be avoided?

[joneugster]

definitely, the current definition is a hack as good as any other. There is no direct reason why it needs to go via the lake manifest.

However, I think it would be desirable if it was replaced by some logic that gets the correct module for reasonably set up projects.