Metamath site down?

[Cris Perdue]

The us.metamath.org website appears to be down.

-Cris

[Mario Carneiro]

It was restarted 3 minutes ago, hopefully it should be back up automatically within at most a few hours.

On Fri, Nov 14, 2025 at 5:32 AM Cris Perdue <cr...@perdues.com> wrote:

The us.metamath.org website appears to be down.

-Cris

--
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 visit https://groups.google.com/d/msgid/metamath/CAOoe%3DWK9PmANsb6PTKRtnf6uJEjuOQbGFPeo2mOM2ugtN5Z0JA%40mail.gmail.com.

[Mario Carneiro]

Apparently it didn't come back automatically, the script https://github.com/metamath/metamath-website-scripts/blob/main/build-system.sh needs work I guess. I rebooted it manually and the site is back up.

[Falcon Dai]

Oh no. I am happy to help. So the current site is hosted on linode (per some of the comments in the linked file)? I wonder if it is worthwhile to migrate it to GitHub hosting. It it is free to host a static site and quite performant in my experience (not to mention that it saves efforts to configure and maintain servers).

[Mario Carneiro]

It's hosted on linode, yes. It's not entirely a static site, since it needs to be rebuilt periodically, but conceivably that could be done with GHA. (I also have some ideas to move more of the generation to server-side on request time to decrease the time and especially storage cost of regeneration.) Feel free to play with it, all of the sources to build the site are freely available at https://github.com/metamath/metamath-website-scripts and https://github.com/metamath/metamath-website-seed .

To view this discussion visit https://groups.google.com/d/msgid/metamath/a545e75b-3b3f-4419-a77a-127ca041e89en%40googlegroups.com.

[samiro.d...@rwth-aachen.de]

"It was restarted 3 minutes ago"

Wow, this finally fixed '?' references in PDF files (example) which should've been fixed in June 2024. (archive from August 2025)
It seems that nobody bothered to rebuild it since then, despite my comment in the pull request over one year ago.

[David A. Wheeler]

> On Nov 14, 2025, at 3:05 PM, Falcon Dai <m...@falcondai.com> wrote:
>
> Oh no. I am happy to help. So the current site is hosted on linode (per some of the comments in the linked file)? I wonder if it is worthwhile to migrate it to GitHub hosting. It it is free to host a static site and quite performant in my experience (not to mention that it saves efforts to configure and maintain servers).

I looked into that (my personal website is hosted on GitHub).

The website is regenerated daily. This is a *good* thing, because serving static pages to many systems is efficient, and all websites are now being hit by constant downloads (organizations are constantly re-downloading the Internet to feed to machine learning training processes). Regenerating the website takes more time than GitHub Actions will provide for free. Using linode means there's a fixed known price (that I pay each month).

--- David A. Wheeler

[Mario Carneiro]

On Mon, Nov 17, 2025 at 11:08 AM samiro.d...@rwth-aachen.de <samiro....@rwth-aachen.de> wrote:

"It was restarted 3 minutes ago"

Wow, this finally fixed '?' references in PDF files (example) which should've been fixed in June 2024. (archive from August 2025)
It seems that nobody bothered to rebuild it since then, despite my comment in the pull request over one year ago.

I think this is because while metamath-website-seed is re-pulled every day as part of the site rebuild, metamath-website-scripts is only re-pulled when the linode machine is rebooted, which has basically happened only once(?), just now, since we started using this workflow after Norm passed in 2021. So we've been using an old script since then... Ideally the daily script would also replace itself with the latest script from metamath-website-scripts to avoid this issue.

On Mon, Nov 17, 2025 at 5:15 PM 'David A. Wheeler' via Metamath <meta...@googlegroups.com> wrote: 

Regenerating the website takes more time than GitHub Actions will provide for free.

I think this is not necessarily the case. The mm-web-rs website generator is way way faster than metamath-exe, I expect the full website generation to take 5 minutes or less if we actually use it.

On Mon, Nov 17, 2025 at 5:15 PM 'David A. Wheeler' via Metamath <meta...@googlegroups.com> wrote:

The website is regenerated daily. This is a *good* thing, because serving static pages to many systems is efficient, and all websites are now being hit by constant downloads (organizations are constantly re-downloading the Internet to feed to machine learning training processes).

This is true though; the web has changed significantly since I started thinking about this plan since AI bots are continuously harassing webmasters globally. But I think this is not anything that can't be solved with a caching layer, which we would have regardless (indeed we already have one as part of our nginx deployment). This is only an improvement in total processing power if it's not the case that the entire website (every single page) is requested every 24 hours. Right now it's possible that the entire site is being downloaded every day, but if we add things that make the site theoretically infinite then this won't be the case anymore. It comes down to a question of how big the cache is vs how much it costs to generate a page. I think it's difficult to know for sure without trying it.

[Jim Kingdon]

On 11/19/25 02:14, Mario Carneiro wrote:

I think this is because while metamath-website-seed is re-pulled every day as part of the site rebuild, metamath-website-scripts is only re-pulled when the linode machine is rebooted, which has basically happened only once(?), just now, since we started using this workflow after Norm passed in 2021. So we've been using an old script since then... Ideally the daily script would also replace itself with the latest script from metamath-website-scripts to avoid this issue.

Oooh, nice discovery. I think this might explain some of the strange symptoms where we've tried to fix things and it hasn't been clear (at least to me) why some things were and were not happening (sorry I don't have details top of mind, this was probably a year or more ago).

[llesyna]

I am not sure this is related, but I have not been able to load the "Visualization version" link to theorems created in 2024 or later, and possibly earlier as well. One example is the theorem norcom. I get a "404 File not found" error message. I like the "Visualization version" as it provides the capability to copy and paste formulas directly into mmj2.

[Mario Carneiro]

The visualization version pages are hosted externally by expln, which means they are liable to get out of sync with the main website since they aren't on the same update schedule. I think we should move the page generation for these to metamath.org .

--

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 visit https://groups.google.com/d/msgid/metamath/10f3ea21-fa9b-4c30-a356-b6c6f8c28fe5n%40googlegroups.com.