Recommendations for metamath hosting?

[David A. Wheeler]

All:

Does anyone have recommendations for a better hosting site for the main site us.metamath.org and/or for the build/staging site us2.metamath.org? Personal experience (or close to it) preferred. Alternatively, warnings about “don’t do X” are also welcome. There are lots of hosting services, which makes selection more complicated :-).

Below is the background & requirements as I know them. In the end Norm decides, my goal is to give him a hand.

--- David A. Wheeler

===========

The “main” us.metamath.org site is currently hosted by site5.com. I’ve learned from Norm that his current term with them expires soon on 7/29/2021. Now would be a good time to plan a change, because the current hosting service has serious limitations. The current us.metamath.org hosting service doesn’t allow ssh or rsync, and it doesn’t make it easy to support TLS/HTTPS (it *might* be possible but it’s not trivial). Those would be highly desired. For example, ideally we could just enable Let’s Encrypt and have TLS/HTTPS support.

On the good side, the current hosting service doesn’t charge extra fees for extra network transfers. That’s important; everyone once in a while the site gets busy. Wherever it goes to should allow transfers without just shutting us off at N bytes.

It might be great to enable Cloudflare’s free tier, or some other inexpensive CDN service. That would make transfers faster & cause less load. We’d need a service that’d work with that.

I don’t think GitHub hosting would work. It’s a static site, but we have too much stuff :-). There are over 100K web pages generated from the *.mm files. I don’t have the numbers handy, but I believe the total site size exceeds the GitHub Pages maximum of 1GB https://docs.github.com/en/pages/getting-started-with-github-pages/about-github-pages

=============

The “build/staging” site us2.metamath.org is where the static files are currently rebuilt. That is currently at Norm’s house running Debian. There’s no rush to change it. However, eventually I’d like to see that somewhere outside a house, so that things can continue smoothly if something happens to his house or him. The site build on us2 takes around 4 to 5 hours, though I suspect that can be sped up without too much effort.

In all cases cost matters.

Any related suggestions (don’t do X) welcome!

[Mázsa Péter]

Digitalocean (autobackup enabled) + Serverpilot.io (for
auto-update/upgrade-security + auto-https). I use it for
wordpress-hosting (behind free cloudflare): foolproof + zero
maintenance. Don't do Google cloud: maintenance =/= (/) :) If you want
to try DO+SP I think they give 2 free months or so (as a referral
program), I'll check it. P.

On 6/12/21, David A. Wheeler <dwhe...@dwheeler.com> wrote:
> All:
>
> Does anyone have recommendations for a better hosting site for the main site
> us.metamath.org and/or for the build/staging site us2.metamath.org

> <http://us2.metamath.org/>? Personal experience (or close to it) preferred.

> Alternatively, warnings about “don’t do X” are also welcome. There are lots
> of hosting services, which makes selection more complicated :-).
>
> Below is the background & requirements as I know them. In the end Norm
> decides, my goal is to give him a hand.
>
> --- David A. Wheeler
>
> ===========
>

> The “main” us.metamath.org <http://us.metamath.org/> site is currently
> hosted by site5.com <http://site5.com/>. I’ve learned from Norm that his

> current term with them expires soon on 7/29/2021. Now would be a good time
> to plan a change, because the current hosting service has serious

> limitations. The current us.metamath.org <http://us.metamath.org/> hosting

> service doesn’t allow ssh or rsync, and it doesn’t make it easy to support
> TLS/HTTPS (it *might* be possible but it’s not trivial). Those would be
> highly desired. For example, ideally we could just enable Let’s Encrypt and
> have TLS/HTTPS support.
>
> On the good side, the current hosting service doesn’t charge extra fees for
> extra network transfers. That’s important; everyone once in a while the site
> gets busy. Wherever it goes to should allow transfers without just shutting
> us off at N bytes.
>
> It might be great to enable Cloudflare’s free tier, or some other
> inexpensive CDN service. That would make transfers faster & cause less load.
> We’d need a service that’d work with that.
>
> I don’t think GitHub hosting would work. It’s a static site, but we have too
> much stuff :-). There are over 100K web pages generated from the *.mm files.
> I don’t have the numbers handy, but I believe the total site size exceeds
> the GitHub Pages maximum of 1GB
> https://docs.github.com/en/pages/getting-started-with-github-pages/about-github-pages
> <https://docs.github.com/en/pages/getting-started-with-github-pages/about-github-pages>
>
> =============
>

> The “build/staging” site us2.metamath.org <http://us2.metamath.org/> is

> where the static files are currently rebuilt. That is currently at Norm’s
> house running Debian. There’s no rush to change it. However, eventually I’d
> like to see that somewhere outside a house, so that things can continue
> smoothly if something happens to his house or him. The site build on us2
> takes around 4 to 5 hours, though I suspect that can be sped up without too
> much effort.
>
> In all cases cost matters.
>
> Any related suggestions (don’t do X) welcome!
>

> --
> 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/0B9C1D56-C042-41FE-BEE1-A3D0B7E94A26%40dwheeler.com.
>

[Cris Perdue]

If you are prepared to upload the static files for the site, I think https://netlify.com/ would be worth a look. I have three or four small public sites with them, and have only good things to say about them.  Convenience, performance, and reliability have been very good from my point of view, and TLS is basically automatic.

Pricing is at https://www.netlify.com/pricing/.  Scroll down just a little to see details.  The metamath site is quite large, but I don't see any limitations on site size.  The "free" plan includes 100GB per month at no charge.  I don't know if you ever get busier than that.

I would recommend using their command line tool to deploy.  It appears to have smarts about not uploading files that have not changed, but I have no idea how effective that would be for Metamath. It definitely has abilities to let you preview a new version of a site before switching it to public status.

Their service does include a CDN.

What they do not provide is any kind of shell access.  They support builds, but not arbitrary executables, so you would need to build elsewhere and upload to Netlify (using their command line tool).

I'm glad to provide more info or help if you think it might be useful.

Best regards,

Cris

--

[Norman Megill]

On Saturday, June 12, 2021 at 11:57:47 AM UTC-4 David A. Wheeler wrote:

All:

Does anyone have recommendations for a better hosting site for the main site us.metamath.org and/or for the build/staging site us2.metamath.org? Personal experience (or close to it) preferred. Alternatively, warnings about “don’t do X” are also welcome. There are lots of hosting services, which makes selection more complicated :-).

Below is the background & requirements as I know them. In the end Norm decides, my goal is to give him a hand.

--- David A. Wheeler

===========

The “main” us.metamath.org site is currently hosted by site5.com. I’ve learned from Norm that his current term with them expires soon on 7/29/2021. Now would be a good time to plan a change, because the current hosting service has serious limitations.

site5.com is also increasing the price by 20% starting 7/29, which is another reason not to renew it. This pushes it to about $10/mo (if I pay for 3 years in advance), up from $4/mo a few years ago.

In the past, us.metamath.org reliably used only volunteer mirrors for many years until 2008, when I felt a little uncomfortable that I had no backup if they all disappeared. At that time I couldn't use my home server as a backup because the ISP blocked port 80 without an expensive "business account". So site5.com was basically a cheaper way to get port 80.

My current home ISP doesn't block port 80, so my house (us2.metamath.org) is now also available as a backup, and the original reason for site5.com is no longer there.

Currently there are two volunteer mirrors, at.metamath.org and cn.metamath.org. (de.metamath.org currently points to at.metamath.org for historical reasons; I may remove it.) Both have been very reliable for the past few years, and I've used both of them for us.metamath.org when the need arose.

us.metamath.org requires about 10GB disk and maybe 100 to 200GB/mo transfers. I think 1TB/mo would provide a comfortable margin. Here are some services people have mentioned:

Linode - 25GB disk space, 1TB/mo transfer for $5/mo

digitalocean - 25GB disk, 1TB/mo transfer for $5/mo.  The associated serverpilot.io seems to be needed for https (not clear to me) for another $5/mo

netify.com - the free plan provides 100GB/mo transfer and $20/mo each extra 100GB/mo, which is a problem. The next higher plan is $19/mo with 400GB/mo transfer. I couldn't find their disk space allowance.

I may set up a Linode account for us.metamath.org and see how it goes.

 

The current us.metamath.org hosting service doesn’t allow ssh or rsync, and it doesn’t make it easy to support TLS/HTTPS (it *might* be possible but it’s not trivial). Those would be highly desired. For example, ideally we could just enable Let’s Encrypt and have TLS/HTTPS support.

If us.metamath.org is changed to use https, it means that it can't be switched to volunteer mirrors as a backup unless they also agree to set up https and maintain certificates. I have little https experience and don't know what it involves.

 

On the good side, the current hosting service doesn’t charge extra fees for extra network transfers. That’s important; everyone once in a while the site gets busy. Wherever it goes to should allow transfers without just shutting us off at N bytes.

It might be great to enable Cloudflare’s free tier, or some other inexpensive CDN service. That would make transfers faster & cause less load. We’d need a service that’d work with that.

I don’t think GitHub hosting would work. It’s a static site, but we have too much stuff :-). There are over 100K web pages generated from the *.mm files. I don’t have the numbers handy, but I believe the total site size exceeds the GitHub Pages maximum of 1GB https://docs.github.com/en/pages/getting-started-with-github-pages/about-github-pages

=============

The “build/staging” site us2.metamath.org is where the static files are currently rebuilt. That is currently at Norm’s house running Debian. There’s no rush to change it. However, eventually I’d like to see that somewhere outside a house, so that things can continue smoothly if something happens to his house or him. The site build on us2 takes around 4 to 5 hours, though I suspect that can be sped up without too much effort.

Well, I don't think the code itself can be sped up much easily, almost certainly not. say,  an order of magnitude. It averages about 100ms per page (on a 10-year-old i5-2500 CPU), which I don't see as unreasonable. I am aware of some bottlenecks generating very large proofs that I plan to address eventually, but even with that, the overall time might only decrease 10% or 20%.

It can be sped up several times by splitting the job onto multiple cores if we really need to do that.

It can also be sped up a factor of 2 if we eliminate the gif image versions of the pages. I've brought this up in the past, and someone said they found the gif pages useful because copy/paste produces the actual set.mm ascii expressions. So I left them in because there's essentially no extra cost in doing so.

Of course speedup is always welcome, but I don't see an urgent need to speed up the site build, as long as it completes in say under 24 hrs.  For urgent special cases, I have a script that will add specific new or modified proofs more or less instantly.

If we move us2 to a paid server to do site builds, it would need around 100GB of disk space (around 60-70GB currently but allowing for growth), which is much more than the inexpensive plans provide. It's hard to compete with "free" (at my house). :)

BTW the site build is essentially done with the script "install.sh" provided with the Metamath download and can be used by anyone to recreate the site on their local machine. The actual build script, called "build-metamath-site", is heavily customized for the us2 server; it calls "install.sh" and also creates buffer and backup directories, so that the site gets completely built before it is exposed on the live site, and so that I can instantly switch to a previous site version if something went wrong.

BTW2 David has the passwords to all accounts (us, us2, DNS) if something happens to me.

Norm

[Cris Perdue]

For what it's worth, I see that Netlify has an official form for requesting an "Open Source" account,

at: https://opensource-form.netlify.com/.

Note: I write this without prejudice against other options, e.g. DigitalOcean with free Cloudflare.  It's just that I have no experience with them.

It asks for the following information:

Project Name

Associated email

Open source license used

Link to code of conduct

Link to our service on your main page

Is there anything else you would like us to know?

I would expect that the account would be free, or at least free up to some limits, if approved, but that is only a guess.

If I were requesting such an account, I would want them to know that the total size of files in the site is (apparently) somewhat over 1GB and that it sometimes needs more than 100GB transfer per month. They don't list "public domain" as a license, so that would need a mention, and surely something about the subject matter and goals of the project, extremely brief and untechnical; also something about the longstanding nature of the project.

"Code of conduct" probably translates to Metamath info for contributors.

(One way to check disk usage would be to do "du -sh" at the shell prompt at the root of the website directory tree.)

--

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/537f32d7-ce74-4151-8992-6bb9c0018d59n%40googlegroups.com.

[Norman Megill]

Thanks, Cris.  I applied for an  an Open Source Account via the link you provided.  We'll see what happens.

Norm

[Norman Megill]

I got the response, " Open Source plans are only applicable for team already having a website on Netlify."  Looking over their description more carefully, it seems that the only advantage of an Open Source plan is "unlimited free team members" but otherwise you pay full price.

Norm

[heiph...@wilsonb.com]

FWIW, I can also vouch for DitialOcean and Linode VMs. Both are hosts that my
employer makes liberal use of, and it sounds like our egress data distribution
is similar to that of us.metamath.org.

> >>> <https://groups.google.com/d/msgid/metamath/537f32d7-ce74-4151-8992-6bb9c0018d59n%40googlegroups.com?utm_medium=email&utm_source=footer>
> >>> .
> >>>
> >>

[Ashok Khanna]

I would recommend Google Compute Engine - a bit of extra setup but you will get a lot more flexibility down the road and hopefully not too expensive either

I wasn't a big fan of Amazon's offering at the lower cost tiers, but your experience may vary. Happy to contribute to any hosting costs by the way.

--

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/0B9C1D56-C042-41FE-BEE1-A3D0B7E94A26%40dwheeler.com.