@kha I disabled this test for now. It seems to fail because we don't
have a `leanpkg.path` there. I thought about hacking the test and adding
a dummy `leanpkg.path` file there, but you might have a better idea.
It is not clear to me why we always need `leanpkg.path` now. It seems
this a new requirement that was introduced when you simplified the
module manager.