Big progress on metamath.org and us2.metamath.org

[David A. Wheeler]

All:

I wanted to give everyone an update that we are making
big progress on getting metamath.org updated.

Norm Megill normally generated the metamath.org site from
the latest version of the set.mm repo. Norm did this by logging in to
us2.metamath.org, regenerating everything, and then sending
the results to metamath.org. While we'd thought we'd set things up
if he passed, I couldn't log in to us2.metamath.org to get things going.

I'm now logged into us2.metamath.org & I'm checking through the
steps to regenerate the main site. So in the not too distant
future the main site should be updated. If something goes wrong,
please let me know so that Mario or I can correct it.

My sincere thanks to Susan Cass, Norm's partner, for
helping me regain control over the metamath systems so
we can keep them going. We had started some steps to get
ready for this, but the timing of Norm's passing was a surprise so we weren't
as ready as I guess we should have been. I expect we'll eventually make
some larger changes in the long term to keep things going.
However, right now we're just trying to quickly get things working as they were.

--- David A. Wheeler

[Glauco]

Great news!

Thank you for all the effort you put into this.

Glauco

[Jim Kingdon]

Thank you for putting in the time and effort. I knew that Norm's
planning for this was nonzero but I'm not surprised that it didn't go as
smoothly as hoped especially the first time.

Let us know if there is anything we can help with (and if you just want
encouragement and patience, I can do that too!).

[David A. Wheeler]

> On Jan 17, 2022, at 10:36 PM, Jim Kingdon <kin...@panix.com> wrote:
>
> Thank you for putting in the time and effort. I knew that Norm's planning for this was nonzero but I'm not surprised that it didn't go as smoothly as hoped especially the first time.
>
> Let us know if there is anything we can help with (and if you just want encouragement and patience, I can do that too!).

Encouragement & patience is definitely appreciated!
I have notes from Norm on how to do things, but it turns out
that actually trying to follow his directions reveals some... omissions :-).

My current goal is to have the existing us2.metamath.org system periodically download the
GitHub set.mm repo (and eventually the GitHub metamath-exe repo),
regenerate the website, and then upload that to metamath.org... while
using the existing scripts & setup to the extent possible (so we can quickly get things
back to normal).

I've successfully run Norm's "rebuilder" script on us2.metamath.org using
old (unchanged) data. There's no *visible* result from that, but it's a key first step
that shows that we at least have all the pieces working.
It turns out that Norm's "rebuilder" script requires data to be in specific
places that aren't the same as the repos we use. I think he copied files
as they changed into specific locations by hand, and those locations
are presumed by later scripts. I'm reviewing the
scripts & current setup to figure out how to automate things with his setup.

Hopefully by this morning the us2.metamath.org will have an updated
set of theorems from set.mm.
I've downloaded the latest files set.mm & mmset.raw.html from
the GitHub "set.mm" repo (develop branch) & I'm rebuilding
the website tonight. Norm said it normally takes about 4-5 hours.
If that works, I'll upload that updated data set to us.metamath.org, and begin
expanding the set of data that is automatically downloaded from GitHub
and used to generate the site. E.g., other .html files, other databases such
as iset.mm, and so on. Once regeneration is fully automated, I'll set up a cron job
automatically update the website on certain days of the week.

In the longer term I'm sure there are ways to make the generation process
better, and I'd like to do that. The current scripts are a mess
(I'm sure Norm would agree :-) ). But since I don't currently know which parts are
necessary workarounds & which are obsolete complications, that
should wait until later.

--- David A. Wheeler

[David A. Wheeler]

The Metamath website seems to have regenerated correctly at:
http://us2.metamath.org

In particular, the most recent set.mm work is shown here:
http://us2.metamath.org/mpeuni/mmrecent.html
... where the most recent addition is dated 15-Jan-2022,
tgoldbachgtALTV - Variant of Thierry Arnoux's tgoldbachgt 30715 using the symbols Odd and GoldbachOdd: The ternary Goldbach conjecture is valid for large odd numbers (i.e. for all odd numbers greater than a fixed 𝑚). This is proven by Helfgott (see section 7.4 in [Helfgott] p. 70) for 𝑚 = 10^27. (Contributed by AV, 2-Aug-2020.) (Revised by AV, 15-Jan-2022.)

Please let me know of any serious problems with the us2 site.

If I don't hear soon, I'll copy that revision from
us2.metamath.org to us.metamath.org, probably tonight.
I have to work out the commands to do that, but Norm's hints will give me a hand.

--- David A. Wheeler

[Alexander van der Vekens]

Hi David,

I had a quick look at the  http://us2.metamath.org pages:  Most recent proofs, Theorem List (Table of Contents), some pages of the Theorem list (about the friendship theorem and my mathbox) and some single theorem pages. I had to perform a Shift-Refresh (refreshing with clearing the browser cache) before I got consistent pages. Afterwards, the theorems seem to be up to date, and the appearance of everything I looked at was fine, except the formatting of the section header of 20.34.8.10  Goldbach's conjectures (http://us2.metamath.org:88/mpeuni/mmtheorems414.html): it is a big block of unformatted text now, compare it with the corresponding page http://us.metamath.org/mpeuni/mmtheorems410.html on http://us.metamath.org/. Please check what went wrong with this (I do not know if there are additional cases, and some other section header comments look fine...).

Alexander

[Alexander van der Vekens]

On Tuesday, January 18, 2022 at 8:51:23 PM UTC+1 Alexander van der Vekens wrote:

Hi David,

I had a quick look at the  http://us2.metamath.org pages:  Most recent proofs, Theorem List (Table of Contents), some pages of the Theorem list (about the friendship theorem and my mathbox) and some single theorem pages. I had to perform a Shift-Refresh (refreshing with clearing the browser cache) before I got consistent pages. Afterwards, the theorems seem to be up to date, and the appearance of everything I looked at was fine, except the formatting of the section header of 20.34.8.10  Goldbach's conjectures (http://us2.metamath.org:88/mpeuni/mmtheorems414.html): it is a big block of unformatted text now, compare it with the corresponding page http://us.metamath.org/mpeuni/mmtheorems410.html on http://us.metamath.org/. Please check what went wrong with this (I do not know if there are additional cases, and some other section header comments look fine...).

Forget about my remark about section  20.34.8.10  Goldbach's conjectures - I think it is my mistake: I added a glossary as html table, and this may have caused the text before it to be displayed unformatted. Maybe I have to provide the whole comment as html...

Alexander

[David A. Wheeler]

> On Jan 18, 2022, at 2:59 PM, 'Alexander van der Vekens' via Metamath <meta...@googlegroups.com> wrote:
> Forget about my remark about section 20.34.8.10 Goldbach's conjectures...

Okay, clearly there's been some checking, and I've learned more about Norm's setup,
so I think we're ready to go.

I have done some prep work on us2.metamath.org (using cd /opt/dts; mv 1 xxold; mv xxnew/ 1).
I believe the main site us.metamath.org will begin, at 4:07am US Eastern Time tomorrow,
to copy the updated generated website from us2.metamath.org to us.metamath.org using rsync.

So by tomorrow midday US Eastern Time I *think* we'll have an updated site. This may not work correctly,
so if it fails, please be kind as I try to figure out what the system is doing or not doing :-).

My plan is to make things entirely depend on the GitHub files, so if you update a file, it
should appear on us2.metamath.org within a day, and then on us.metamath.org not too
long after that. We're not there yet, but that's a reasonable step.

--- David A. Wheeler

[Benoit]

Thanks David.  This should be debated (and there is no urgency), but I think it would be nice to have us.metamath.org purposefully "lagging" behind us2, in order to really have two different versions and be able to compare them.  I do not know if the lagging should be expressed in terms of duration, or number/importance of commits, or if us2 should be updated with the "develop" branch and us with the "master" branch...

When I asked this to Norm a few years ago, he created the folder "http://us2.metamath.org:88/old/mpeuni/" which contains somewhat older versions (but I do not know exactly how much older, nor if it is in terms of days or commits), and I sometimes find it convenient.  If we have a consistent rule for us/us2, then this "old/" folder could be removed.

Benoît

[roger witte]

I have been unable to access US2.metamath.org for the past 24 hours.

Regards

Roger Witte

[David A. Wheeler]

More progress - us.metamath.org been updated from us2.metamath.org, which you can check by viewing:
http://us.metamath.org/mpeuni/mmrecent.html

There are still several problems, but I'm happy we're making progress.
Worse comes to worse, I *do* have access to the DNS registration account,
so we can completely change systems if we decide to do so.

--- David A. Wheeler

[Alexander van der Vekens]

Great, it works perfectly (as far as I have checked it). 

By the way, wasn't there oncy a German mirror site, was it? And I have looked at the Austrian mirror site - this seems not to be updated since October 2021. Does anybody now how the mirror sites are maintained?

[Mingli Yuan]

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?

Mingli

--
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 metamath+u...@googlegroups.com.
To view this discussion on the web visit https://groups.google.com/d/msgid/metamath/f51a5421-adba-4541-ab75-2f26c6432a9bn%40googlegroups.com.

[David A. Wheeler]

> On Jan 22, 2022, at 7:41 AM, Mingli Yuan <mingl...@gmail.com> 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

[ookami]

As for the German site: It exists as well, see http://de.metamath.org/mpeuni/mmrecent.html.  Note that it was last updated on 25-Oct-2021,  So this seems to be refreshed infrequently only.http://de.metamath.org/mpeuni/mmrecent.html

[Jim Kingdon]

On 1/23/22 1:44 PM, David A. Wheeler wrote:

> 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.

Sounds good to me. This is some approximation of what Norm had been
doing manually, and I'm all in favor of making it more automatic since
the interesting judgement calls happen before things get merged anyway.

[Alexander van der Vekens]

On Sunday, January 23, 2022 at 11:39:19 PM UTC+1 ookami wrote:

As for the German site: It exists as well, see http://de.metamath.org/mpeuni/mmrecent.html.  Note that it was last updated on 25-Oct-2021,  So this seems to be refreshed infrequently only.

But it is not contained/mentioned on the mirror page http://us.metamath.org/mm.html, and even not on http://de.metamath.org/mm.html. It should be added there.