mathport on a branch

Stream: mathlib4

[Jireh Loreaux]

What instructions should I follow to run mathport on a branch of mathlib? Oneshot won't work because I have edited several files lower down. I realize I will actually have to run mathport (and it will take a while). Are there any pitfalls I should be wary of? For example, do I need to merge master on this branch so that I'm running with a recent copy of mathlib3 + my edits?

[Eric Wieser]

I think you're likely going to have a better time with the latest mathlib3 master

[Scott Morrison]

The makefile itself doesn't care if you are running against something close to master, but Eric is right that the closer you are the less room for surprises there is.

Hopefully you just need to change the line:

# Select which commit of mathlib3 to use.
MATHBIN_COMMIT=origin/master

in the Makefile, and then follow the instructions for running everything from scratch.

[Jireh Loreaux]

Great, thanks. I'll give it a shot.