> 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/012EFD1C-2A34-4E4E-973F-52D408ECC42D%40dwheeler.com.
