Lake mathport panic

Stream: lean4

[Alex J. Best]

I was trying to get mathport running on my machine, by cloning the mathport repo and running various make targets.
I kept getting the error unknown package 'Mathbin' when I opened files in Vscode so I tried to run lake configure as that seemed sensible.
This gave me a Panic about get! not being some, building lake locally and running under lldb I traced this to Package.buildDepOleans and the following change fixed it (at least gave me a version of lake that would run lake configure in my mathport repo):

diff --git a/Lake/Build/Package.lean b/Lake/Build/Package.lean
index b6819e2..a43cd19 100644
--- a/Lake/Build/Package.lean
+++ b/Lake/Build/Package.lean
@@ -77,7 +77,7 @@ def Package.buildOleanAndCTarget (self : Package) : SchedulerM ActiveOpaqueTarge

 def Package.buildDepOleans (self : Package) : BuildM PUnit := do
   let targets ← self.dependencies.mapM fun dep => do
-    (← getPackageForModule? dep.name).get!.buildOleanTarget
+    (← getPackageByName? dep.name).get!.buildOleanTarget
   targets.forM fun target => discard <| target.materialize

 def Package.oleanTarget (self : Package) : OpaqueTarget :=

I have many lingering questions:

• Is this a correct fix for a lake bug, or is my setup or mathport somehow wrong?
• should I need to run lake configure in mathport at all?
• is there another reason mathport may not be able to find Mathbin?

[Mac]

You are entirely correct, this a bug an your fix is exactly right.

[Mac]

I just pushed the fix to Lake: 02cd07c