mathport and leanproject build

Stream: mathlib4

[Ashley Blacquiere]

I'm following the mathport instructions and have gotten to the bit that says "make sure that leanproject build runs cleanly". That just means run it and make sure there are no errors then cancel, correct? I don't have to wait for the entire build process...?

[Yury G. Kudryashov]

Are you using it on mathlib or on a project?

[Ashley Blacquiere]

On a project.

[Yury G. Kudryashov]

You'll recompile the project anyway on the lean --make --recursive --ast --tlean src line

[Scott Morrison]

How long does leanproject build take on your project, anyway?

[Ashley Blacquiere]

Not sure. Started it ten minutes ago and its only in the topology library at the moment... Seems like maybe a while.

[Yury G. Kudryashov]

Do you recompile the whole mathlib?

[Yury G. Kudryashov]

Or just your project?

[Yury G. Kudryashov]

Should we add leanproject get-cache to the instructions?

[Ashley Blacquiere]

Hm. Ya, if that's a necessary step. I created a new clone of my project before the leanproject mk-all step, but didn't think to grab oleans...

[Yury G. Kudryashov]

This is not a necessary step because you're going to run leanproject clean and rebuild it later.

[Ashley Blacquiere]

Think I've got it now. Thanks for the help. Tho I did realize when running leanproject build that I completely missed updating an entire file when upgrading to Lean 3.51... :laughing: