mathport recompiles mathlib

Stream: mathlib4

[Yury G. Kudryashov]

I'm following instructions on https://github.com/leanprover-community/mathport/blob/master/Oneshot/README.md
When I run make build, it rebuilds many files from Mathlib.

[Yury G. Kudryashov]

This looks strange because lake exe cache get just downloaded these oleans.

[Yury G. Kudryashov]

Is it because of some inconsistency of lake flags?

[Floris van Doorn]

It should only compile them, and therefore it should go 10-100x quicker than building Mathlib from scratch.

[Yury G. Kudryashov]

Yes, thank you! (Also, I duplicated the question in another thread and Mario already got the same answer).

[Arthur Paulino]

It's probably worth mentioning this detail in the README so people don't think they've done something wrong or that something is broken