Main metamath website generates its own web pages - needs a little slimming

[David A. Wheeler]

Progress! We're one step closer to not using us2.metamath.org.

The main metamath website, "metamath.org / us.metamath.org",
now *generates* its own web pages as well as serving them. So it
*no longer* pulls files from Norm's computer us2.metamath.org.

Please let me/us know of any problems you find.
This *should* be a silent change, that is, there shouldn't be anything to notice.
But of course, I'm doing things in stages in case there *is* a problem.
Eventually we'll want the mirrors to stop using us2.metamath.org too,
but that's a different step.

Currently I've set website regeneration to occur daily at 4am UTC.
That time is arbitrary and can be changed.

The site is currently at 98% disk use, which is WAY too much & begging
for problems. I'd like to fix that quickly.
There are a few mega-large files we create in "downloads/",
and I don't think we need ALL of them:
276136805 Aug 30 09:52 metamathsite.zip
273985535 Aug 30 09:51 metamathsite.tar.gz
269798481 Aug 30 09:51 metamathsite.tar.bz2
268443892 Aug 30 09:47 mpeuni.zip
206535792 Aug 30 09:45 mpeuni.tar.gz
98907939 Aug 30 09:43 mpeuni.tar.bz2

Can we drop the '.tar.gz' files in these cases?
I think the .tar.bz2 and .zip formats should be plenty.

Also, we might also want to remove some metamath.exe
stuff & point people to GitHub, e.g., removing:
downloads/metamath.zip
downloads/metamath.tar.gz
downloads/metamath.tar.bz2

--- David A. Wheeler

[Jim Kingdon]

On 8/30/22 16:18, David A. Wheeler wrote:

> Progress! We're one step closer to not using us2.metamath.org.

Thank you again for all your work on this. Also send my thanks to Norm's
partner who has been providing space and power for us2 during this
transitional time.

> Can we drop the '.tar.gz' files in these cases?
> I think the .tar.bz2 and .zip formats should be plenty.

OK with me.

> Also, we might also want to remove some metamath.exe
> stuff & point people to GitHub, e.g., removing:
> downloads/metamath.zip
> downloads/metamath.tar.gz
> downloads/metamath.tar.bz2

I suppose I could imagine a world in which github becomes less available
or wants money for this. But it seems unlikely for the near to medium
term, so I suppose we might as well if having them on the linode is
causing any problems.