> On Jan 22, 2022, at 7:41 AM, Mingli Yuan <[email protected]> wrote: > Good news from cn mirror, the page > http://cn.metamath.org/mpeuni/mmrecent.html was updated. > My assumption is that Norm had set up some automatic mechanism to sync > between mirrors and the main site?
Yes, and/or the mirrors automatically updated. I don't think it's true for all mirrors though. I'm working to make the current us2.metamath.org setup so it will auto-generate every day from the merged work. I got the pieces working by hand & hopefully it'll be working automatically soon. (My personal life is complicated & it takes hours to see if a run succeeded, or it would all be working now.) *Temporarily* I want to make us.metamath.org update daily from us2.metamath.org, until I can be confident that this update works. In the longer term, we should figure out how to decide when to update us.metamath.org from us2.metamath.org. Historically that was decided by Norm like a software release is. I don't think that makes as much sense nowadays; all the theorems are formally proven & every change is approved by someone else. If we can avoid unnecessary work I'm all for it :-). I propose that we automatically update from us2.metamath.org to us.metamath, though perhaps not as often. E.g., maybe us2.metmath.org is updated every day, while us.metamath.org is updated only once a week (or on certain days of the week). That way, people could merge in changes & see the final effect, while giving a little time to actually make the change. We could force an out-of-band update earlier on special cases. --- David A. Wheeler -- You received this message because you are subscribed to the Google Groups "Metamath" group. To unsubscribe from this group and stop receiving emails from it, send an email to [email protected]. To view this discussion on the web visit https://groups.google.com/d/msgid/metamath/6EEDC34C-C224-44AF-9BAC-74F77EF5218A%40dwheeler.com.
