when does mathlib3port run / running it myself

Stream: mathlib4

[Kevin Buzzard]

I started porting Algebra.Group.WithOne yesterday but it simultaneously got split into several files in mathlib3, so now my job is to port Alegbra.Group.WithOne.Defs. I just sat down to do this but mathlib3port is still on Algebra.Group.WithOne. When will it make an Algebra.Group.WithOne.Defs file? The changes have been made to mathlib3. Alternatively is there a way I can just generate what the autoporter will do to this new file the next time it runs?

[Moritz Doll]

it runs every day. I've tried to run it myself and I found it a bit annoying to set up (even the oneshot variant). the instructions are in the mathport github if you want to try.

[Kevin Buzzard]

I just found this message. I had guessed it ran every day but what I really want to know is what time it runs ;-)

[Kevin Buzzard]

Oh, given that the last commit was 20 hours ago, I guses one could conjecture that it's 4 hours' time...

[Jakob von Raumer]

Should we maybe consider running it more often so that changed #aligns get propagated more quickly? ( :eyes:ing the longest dependency chains)

[Scott Morrison]

https://github.com/leanprover-community/mathport/pull/208