Zulip Chat Archive

Stream: mathlib4

Topic: when does mathlib3port run / running it myself


Kevin Buzzard (Dec 03 2022 at 14:02):

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 (Dec 03 2022 at 14:08):

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 (Dec 03 2022 at 14:09):

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 (Dec 03 2022 at 14:09):

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

Jakob von Raumer (Dec 06 2022 at 13:17):

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

Scott Morrison (Dec 06 2022 at 22:04):

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


Last updated: Dec 20 2023 at 11:08 UTC