This part of the web page is in git at
https://github.com/metamath/set.mm/blob/develop/mmset.raw.html#L468 so
you can update it yourself via the normal pull request mechanism (can't
remember whether you have been submitting pull requests, but if not
there are lots of details at
https://github.com/metamath/set.mm/blob/develop/CONTRIBUTING.md and the
pages linked from there).
On 7/25/22 04:19, Jon P wrote:
Sounds like really nice progress David, very impressive, hope the
covid is light and passes off quickly for you :)
As a tiny thing I noticed on the front page it it says "Constructs
mathematics from scratch, starting from ZFC set theory axioms. Over
23,000 proofs."
Whereas maybe there are about 43k proofs now?
On Sunday, July 24, 2022 at 11:59:24 PM UTC+1 David A. Wheeler wrote:
All:
I've made some improvements to the us.metamath.org
<http://us.metamath.org> website infrastructure.
Details, including upcoming plans, are below. Comments welcome!
--- David A. Wheeler
====================
The most obvious change is that while you can continue to use the
old "http:"
URLs, all such requests are immediately upgraded to secure
"https:" requests.
Once you're using http requests, all relative requests continue to
use https.
The TLS (security) certificates used by https are provided
by Let's Encrypt, and they are automatically updated.
I've made some other improvements (mostly to security); all should
be invisible:
* We now use Debian 11 not Debian 10 (this upgrade improved
security & performance somewhat)
* The system now *automatically* downloads & installs security
updates, so any vulnerabilities
publicly found will be quickly addressed without waiting for me or
anyone else.
* We now have a simple intrusion prevention system enabled
(fail2ban - it's primarily there
to counter simplistic mass attacks).
* I've enabled a basic firewall to make life slightly harder on
attackers by ensuring that
only specific identified services are visible.
* I've slightly hardened the kernel configuration against attack
(e.g., by enabling source address verification & ignoring source
routing)
* I've slightly hardened the web server (nginx) against attack
(e.g., by only allowing the HTTP requests GET, HEAD, and OPTIONS).
There's always some additional security hardening you can do, but
I'm hoping that
these steps will be adequate to keep the site relatively secure.
I've made a larger but subtler change by switching to an
"Infrastructure as Code" approach.
That is, the *entire* server is defined by a set of scripts here:
https://github.com/metamath/metamath-website-scripts
We can at any time destroy the current virtual server & recreate
it automatically
with those scripts. This eliminates the "I wonder how this server
is configured" mystery,
and more importantly, it means we can always rebuild the server
from scratch whenever we want
(making the server like cattle instead of like a pet). Anyone can
review those scripts and
propose improvements, which if accepted will improve the system.
Currently us.metamath.org <http://us.metamath.org> is just the web
server. I plan to eventually *also* make it
the system that regenerates the website, 1/day. That is taking
longer to implement.
For one, I got COVID-19 this week, so I've been asleep most of
this week instead of
being useful :-(. Another is that Norm set up us2.metamath.org
<http://us2.metamath.org> the way he wanted over
a long period of time, so it's taking me quite some time to figure
out how to redo it.
He assumed that storage space was unlimited, but while we *can*
get lots of storage, it
costs more money; I would rather not keep unused extra copies that
would cost more money.
The cheapest linode plan has enough space for the website & 1 copy
being generated, not several.
The scripts were also just very complicated, which I think made
sense to him
because he built it over time. However, since we're transitioning
to a different
system anyway, I want to have a much less complicated system that
we can maintain it into the future.
I think the result will be much simpler & cleaner, but it's taking
me a while to figure out
what Norm's scripts did so I can extract just the parts we need.
Once the us.metamath.org <http://us.metamath.org> site can
regenerate the webpages, we can have the other mirrors sync
from *that* system instead (us instead of us2).
I think it'd be good to continue to support mirrors, we've
been doing it for a long time & I see no reason to stop.
However, I think the mirrors should be copying from a site that is
*not*
depending on anyone's basement :-).
I'm not sure how that sync'ing should take place. Currently it
uses rsync, which isn't secured;
we *could* continue to support that but I think it's a lousy idea
today.
The easy answer would be rsync+ssh, which would be fine and works
basically
identically to rsync except it adds encryption. If someone wants
an alternative
approach, we could probably support alternatives. That said, first
we need
to generate data worth synchronizing :-).
--
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 [email protected].
To view this discussion on the web visit
https://groups.google.com/d/msgid/metamath/fc16b33d-e226-4e6e-99ef-db668f4db491n%40googlegroups.com
<https://groups.google.com/d/msgid/metamath/fc16b33d-e226-4e6e-99ef-db668f4db491n%40googlegroups.com?utm_medium=email&utm_source=footer>.
--
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 [email protected].
To view this discussion on the web visit
https://groups.google.com/d/msgid/metamath/5516dd3d-2e9b-bddf-aa91-3e1959b48217%40panix.com.
