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

-- 
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+unsubscr...@googlegroups.com.
To view this discussion on the web visit 
https://groups.google.com/d/msgid/metamath/537f32d7-ce74-4151-8992-6bb9c0018d59n%40googlegroups.com.

Reply via email to