> On Aug 30, 2022, at 10:45 AM, Benoit <[email protected]> wrote:
>
> Thanks David for this work. I have two down-to-earth questions:
>
> * When linking to a page in the metamath website (or when sending a link to
> someone), we should always use "https://us.metamath.org/..."; (that is,
> "https" and "us" as opposed to "http" and "us2", and no port indication like
> ":88" as is the case for us2). Correct ?
Correct!
The .mm files currently often refer to "http://us.metamath.org"; instead of
"https". I think we should create a PR to fix those links in the future.
> * When is the website updated after a PR is merged ? (e.g., "the following
> day at 6pm GMT", or "within the following 12 hours", or...) ? Or does it
> vary ? Maybe different pages have different refresh rates ?
The process to take all data & generate a "new version of the website"
currently takes 6.5 hours. I'm sure it could be sped up in the future
dramatically, but I think it's useful as-is.
When it runs, it loads the files (e.g., the databases) and then generates a new
version of the website. We can then sync it to update what's visible, which
will be basically instantaneous. So it's not at all set up to have different
pages updated at different refresh rates.
We can choose *when* it runs. I'm expecting to run it daily, as that is easily
understood. We could to it 2/day (that would double the CPU costs), or only
some days (but I think daily is easier to understand).
--- David A. Wheeler
--
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/3E45E621-993B-49AB-B381-51A12F12AF00%40dwheeler.com.
