mathport reports "uncaught exception"

Stream: new members

[Laurent Bartholdi]

I'm trying to adapt to lean4/mathlib4, and wanted to port a project using "mathport". I replaced the main.lean file in Oneshot/lean3-in, but kaboom, error message

% more Logs/oneshot.err
porting Main
uncaught exception: failed to port Oneshot:Main with imports [Leanbin.Init.Default, Mathbin.Tactic.Default, Mathbin.Data.
Finset.Basic, Mathbin.Data.Finset.Card, Mathbin.Data.Fintype.Perm, Mathbin.GroupTheory.Subgroup.Basic, Mathbin.GroupTheor
y.Commutator, Mathbin.GroupTheory.GroupAction.Basic, Mathbin.GroupTheory.Exponent, Mathbin.GroupTheory.Perm.Basic, Mathbi
n.Topology.Basic, Mathbin.Topology.SubsetProperties, Mathbin.Topology.Separation, Mathbin.Topology.Homeomorph, Extra]:
function expected
  IsLocallyMoving G
Failed to port { package := "Oneshot", mod3 := `main }

I tried bisecting the file to remove an offending line, but it only got worse. Should I just give up and port manually, or is there a chance?

If someone is brave enough to give the file a chance, I put it at https://www.math.uni-sb.de/ag/bartholdi/rubin.lean

MTIA!

PS. I realize I'm not a "new member" anymore, because of age, but I still have have "new member"-like questions. I hope it's OK for me to post in that thread.

[Patrick Massot]

@Mario Carneiro , this is also a mystery for you. The file above works in mathport's mathlib if you add one sorry on line 891, but then mathport fails to oneshot it.