> On Jan 17, 2022, at 10:36 PM, Jim Kingdon <[email protected]> wrote: > > Thank you for putting in the time and effort. I knew that Norm's planning for > this was nonzero but I'm not surprised that it didn't go as smoothly as hoped > especially the first time. > > Let us know if there is anything we can help with (and if you just want > encouragement and patience, I can do that too!).
Encouragement & patience is definitely appreciated! I have notes from Norm on how to do things, but it turns out that actually trying to follow his directions reveals some... omissions :-). My current goal is to have the existing us2.metamath.org system periodically download the GitHub set.mm repo (and eventually the GitHub metamath-exe repo), regenerate the website, and then upload that to metamath.org... while using the existing scripts & setup to the extent possible (so we can quickly get things back to normal). I've successfully run Norm's "rebuilder" script on us2.metamath.org using old (unchanged) data. There's no *visible* result from that, but it's a key first step that shows that we at least have all the pieces working. It turns out that Norm's "rebuilder" script requires data to be in specific places that aren't the same as the repos we use. I think he copied files as they changed into specific locations by hand, and those locations are presumed by later scripts. I'm reviewing the scripts & current setup to figure out how to automate things with his setup. Hopefully by this morning the us2.metamath.org will have an updated set of theorems from set.mm. I've downloaded the latest files set.mm & mmset.raw.html from the GitHub "set.mm" repo (develop branch) & I'm rebuilding the website tonight. Norm said it normally takes about 4-5 hours. If that works, I'll upload that updated data set to us.metamath.org, and begin expanding the set of data that is automatically downloaded from GitHub and used to generate the site. E.g., other .html files, other databases such as iset.mm, and so on. Once regeneration is fully automated, I'll set up a cron job automatically update the website on certain days of the week. In the longer term I'm sure there are ways to make the generation process better, and I'd like to do that. The current scripts are a mess (I'm sure Norm would agree :-) ). But since I don't currently know which parts are necessary workarounds & which are obsolete complications, that should wait until later. --- 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/431642E1-8BC1-424D-A55F-957F5524CA40%40dwheeler.com.
