Making progress on generating Metamath website without us2.metamath.org

[David A. Wheeler]

Good news, I'm making progress on generating the Metamath website
*without* us2.metamath.org. I'm not done yet, but progress is progress. Details below.

--- David A. Wheeler

=== DETAILS ===

Currently the metamath website is generated on the "us2.metamath.org" computer,
then sent (via rsync) to the us.metamath.org public website.
However, us2 is actually at Norm Megill's former home, and it's not fair
to ask his former partner to keep that computer running indefinitely.

I've been working to make it so the us.metamath.org computer (hosted on linode)
will *generate* the website as well as *serving* it on the web.
My plan is to re-run generation on a daily basis (as it is now), so
all merged changes will show up within about a day.

I've had trouble getting generation working at all. Norm wrote his scripts
for his specific computer, and though there are comments, they omit some things.
I made a number of fixes & changes to the script,
and then untarred a metamathsite.tar.gz file into the "metamcthsite" directory,
and it's finally starting to regenerate parts of the metamath site.
It's now generating 132264 filesystem objects (files + directories) in "metamathsite".

It's currently not correctly generating the PDFs using latex, even though latex is installed.
I don't know why; I'm going to have to debug that. Also,
I need to compare what it's generating vs. the real site, and fix any other problems.
I expect that there *will* problems, but I don't know what they'll be.

Still, before this weekend I hadn't managed to regenerate the website other than on us2,
so this is a big step forward. After everything works, I'm sure we can do things
to refine the scripts to be better/cleaner, but getting them working is the priority.

Currently regeneration takes about 6 hours (using the cheapest Linode
plan, which has only 1 relatively low-speed CPU). I estimate
doing daily regeneration will cost an added ~$3/month for CPU costs.
I'm *hoping* I won't need to also pay for more storage, but currently
93% of storage is being used, so that upgrade may be unavoidable.
I plan to just pay for those costs myself for now,
as well as the other costs (for hosting & DNS), though I may eventually
send around my virtual hat :-).

Daily regeneration has its negatives, but also its positives - it means the site
contents are displayed *quickly*, and it works for those who don't enable JavaScript.
Doing it all on a cloud system means that everything will keep working
even if someone dies/becomes incapacitated/etc.

[David A. Wheeler]

I *think* I've worked out the other problems in
having us.metamath.org generate the metamath website.
I'm going to re-run a test from scratch.

If it all works, then within the next few days I intend to *disable* the website
generation by us2.metamath.org, and switch over to using us.metamath.org
to both generate AND serve web pages. When I do that, I'll let everyone know.
At that point, please let me know if there's an unexpected problem.

I intend to keep the old us2.metamath.org on standby mode in case there's
a problem, so we can switch back to using it. Once we confirm that
the new system is working well, we can work on updating how the
mirrors get their information.

*Hopefully* this is one step closer to decommissioning Norm's old machine.

--- David A. Wheeler

[Benoit]

Thanks David for this work.  I have two down-to-earth questions:

* When linking to a page in the metamath website (or when sending a link to someone), we should always use "https://us.metamath.org/..." (that is, "https" and "us" as opposed to "http" and "us2", and no port indication like ":88" as is the case for us2).  Correct ?

* When is the website updated after a PR is merged ? (e.g., "the following day at 6pm GMT", or "within the following 12 hours", or...) ?  Or does it vary ?  Maybe different pages have different refresh rates ?

Thanks,

Benoît

[David A. Wheeler]

> On Aug 30, 2022, at 10:45 AM, Benoit <benoit...@gmail.com> wrote:
>
> Thanks David for this work. I have two down-to-earth questions:
>
> * When linking to a page in the metamath website (or when sending a link to someone), we should always use "https://us.metamath.org/..." (that is, "https" and "us" as opposed to "http" and "us2", and no port indication like ":88" as is the case for us2). Correct ?

Correct!

The .mm files currently often refer to "http://us.metamath.org" instead of "https". I think we should create a PR to fix those links in the future.

> * When is the website updated after a PR is merged ? (e.g., "the following day at 6pm GMT", or "within the following 12 hours", or...) ? Or does it vary ? Maybe different pages have different refresh rates ?

The process to take all data & generate a "new version of the website" currently takes 6.5 hours. I'm sure it could be sped up in the future dramatically, but I think it's useful as-is.

When it runs, it loads the files (e.g., the databases) and then generates a new version of the website. We can then sync it to update what's visible, which will be basically instantaneous. So it's not at all set up to have different pages updated at different refresh rates.

We can choose *when* it runs. I'm expecting to run it daily, as that is easily understood. We could to it 2/day (that would double the CPU costs), or only some days (but I think daily is easier to understand).

--- David A. Wheeler

[David A. Wheeler]

On Aug 30, 2022, at 11:02 AM, David A. Wheeler <dwhe...@dwheeler.com> wrote:
>
> We can choose *when* it runs. I'm expecting to run it daily, as that is easily understood. We could to it 2/day (that would double the CPU costs), or only some days (but I think daily is easier to understand).

Quick clarification: I intend to set a specific time for the website regeneration to start every day. Say, 2am Eastern Time. The regeneration would download the current versions of the databases, run to completion, and then update the website all at once. So the website update would currently occur about 6.5 hours after the regeneration begins.

--- David A. Wheeler

[Benoit]

Thanks David.  To clarify: I'm not pushing towards faster or more frequent updates.  Even if it's only every other day or less, I'd be fine.  What's important is that this information is known (maybe we could indicate it on mmrecent.html or somewhere else).  So, if I understand, a refresh cannot be triggered by a merge on github: the website script has to download the databases periodically in order to check whether they were modified ? (And then, I guess the regeneration happens only if a change is noticed in the associated database ?).

Benoît

[David A. Wheeler]

> On Aug 30, 2022, at 11:22 AM, Benoit <benoit...@gmail.com> wrote:
>
> Thanks David. To clarify: I'm not pushing towards faster or more frequent updates. Even if it's only every other day or less, I'd be fine. What's important is that this information is known (maybe we could indicate it on mmrecent.html or somewhere else).

Good point. We can put it somewhere on the website (once we know what it is :-) ).

> So, if I understand, a refresh cannot be triggered by a merge on github: the website script has to download the databases periodically in order to check whether they were modified ?

Correct. There are many things that influence the results of generation, in particular, updating a database OR updating the metamath.exe tool OR the underlying seed website OR the scripts used to create the website.

It takes long enough to regenerate that it's better to generate periodically, and NOT regenerate on each change.

> (And then, I guess the regeneration happens only if a change is noticed in the associated database ?).

Actually, no, it currently just regenerates every day.

I hope to add that optimization later. If someone else wants to do it, GREAT! It would save a few pennies. However, currently my goal is make it work *NOW*. We can optimize later. It's not *hard* really, but to truly ensure that generation occurs when something HAS changed, you need to ensure you capture all the possible cases. It's easier to just "always regenerate periodically".

Context: originally these were jury-rigged scripts that Norm only ran every once in a while. For many years changes occurred only infrequently, so that was fine. But the Metamath community has greatly grown since then, and I do *not* want to have to have anyone figure out "when to update the website". Periodic updates of whatever has been approved means one less discussion/decision we need to make. If it's been accepted, then let's show it. If we make a change/improvement later, then let's show that too.

--- David A. Wheeler

[Alexander van der Vekens]

Currently, us2.metamath.org is not reachable anymore - is this intended?

[David A. Wheeler]

> On Sep 6, 2022, at 12:51 AM, 'Alexander van der Vekens' via Metamath <meta...@googlegroups.com> wrote:
>
> Currently, us2.metamath.org is not reachable anymore - is this intended?

I recommend normally using us.metamath.org (main site), not us2.metamath.org (Norm's old computer).

As far as I can tell, us.metamath.org is working normally. If it *ever* goes down for
a nontrivial amount of time, let me know.

Unfortunately mirrors are currently running off rsync.metamath.org, and that's really us2.metamath.org
instead of us.metamath.org. I intend to eventually move rsync to refer to us.metamath.org, but
we're having trouble with a DNS transfer and that is temporarily halting things.

I'll ask Susan's partner to reboot Norm's old computer, that may help.

--- David A. Wheeler

[David A. Wheeler]

Note: I'm automatically notified via email
if us.metamath.org ever goes down for more than 5 minutes.
That said, I might miss the alert, or perhaps the monitoring system might fail to
notify me, so if it's down for a while it's fine to let me know.

Hopefully us.metamath.org going down will be a rare occurrence:
* The us.metamath.org site is hosted by
Linode, who generally have a good reputation, so the virtual machine should
generally keep running.
* The web server (nginx) is generally pretty reliable, and
is auto-restarted if it crashes.
* The system automatically installs security updates,
which will hopefully update the system faster than attackers exploit known vulnerabilities.
* I've taken some hardening steps to make the system harder to take down.
* We're simply serving static HTML pages and many server functions are
intentionally disabled, which hardens it further.

Nothing is unbreakable, but I'm trying to increase the likelihood that
the system will just keep running.

--- David A. Wheeler

[Benoit]

Now that "us" is favored over "us2" and that there is no longer the notion that "us2" is fresher than "us", we should also "decouple" both sites by removing some hyperlinks between them (e.g., us.metamath.org currently has a link to "http://us2.metamath.org:88/mpeuni/mmrecent.html" for "Recent proofs" near the top of the page, and a few other instances).

Benoît

[David A. Wheeler]

> On Sep 8, 2022, at 4:57 PM, Benoit <benoit...@gmail.com> wrote:
>
> Now that "us" is favored over "us2" and that there is no longer the notion that "us2" is fresher than "us", we should also "decouple" both sites by removing some hyperlinks between them (e.g., us.metamath.org currently has a link to "http://us2.metamath.org:88/mpeuni/mmrecent.html" for "Recent proofs" near the top of the page, and a few other instances).

Agreed. I've hesitated because I wanted to make sure that the site kept working day-by-day.

Has anyone had any problems with us.metamath.org?

--- David A. Wheeler