Mathport trouble with Default.olean?

Stream: general

[Ashley Blacquiere]

I've been trying to port an old project to Mathlib4, but I've been getting the following error on the mathport build step:

failed to read file './Outputs/oleans/leanbin/Leanbin/Init/Default.olean', invalid header

while I'm not sure it's actually pointing to the root cause, it might help me narrow down the issue, if anyone has any insight...

[Mario Carneiro]

This indicates that you have mismatched lean4 versions of some kind. Maybe the Outputs folder already contains some files generated by an earlier version? Run make unport to clear Outputs and ensure a fresh build.