Currently, us2.metamath.org is not reachable anymore - is this intended? On Tuesday, August 30, 2022 at 8:55:52 PM UTC+2 David A. Wheeler wrote:
> > > On Aug 30, 2022, at 11:22 AM, Benoit <[email protected]> wrote: > > > > Thanks David. To clarify: I'm not pushing towards faster or more > frequent updates. Even if it's only every other day or less, I'd be fine. > What's important is that this information is known (maybe we could indicate > it on mmrecent.html or somewhere else). > > Good point. We can put it somewhere on the website (once we know what it > is :-) ). > > > So, if I understand, a refresh cannot be triggered by a merge on github: > the website script has to download the databases periodically in order to > check whether they were modified ? > > Correct. There are many things that influence the results of generation, > in particular, updating a database OR updating the metamath.exe tool OR the > underlying seed website OR the scripts used to create the website. > > It takes long enough to regenerate that it's better to generate > periodically, and NOT regenerate on each change. > > > (And then, I guess the regeneration happens only if a change is noticed > in the associated database ?). > > Actually, no, it currently just regenerates every day. > > I hope to add that optimization later. If someone else wants to do it, > GREAT! It would save a few pennies. However, currently my goal is make it > work *NOW*. We can optimize later. It's not *hard* really, but to truly > ensure that generation occurs when something HAS changed, you need to > ensure you capture all the possible cases. It's easier to just "always > regenerate periodically". > > Context: originally these were jury-rigged scripts that Norm only ran > every once in a while. For many years changes occurred only infrequently, > so that was fine. But the Metamath community has greatly grown since then, > and I do *not* want to have to have anyone figure out "when to update the > website". Periodic updates of whatever has been approved means one less > discussion/decision we need to make. If it's been accepted, then let's show > it. If we make a change/improvement later, then let's show that too. > > --- 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/6208f6df-7b40-4aef-86b9-e9ff3070529bn%40googlegroups.com.
