On Saturday, September 30, 2023 at 11:12:48 PM UTC+2 [email protected] wrote:
the other thing is that dealing with files hosted on set.mm repo is a bit of a mess because it is so jumbled and flat. We have to cherry pick which files go in mpegif, which are for ilegif and which are for nfegif. Putting things in folders will make the script a lot simpler, and would make me more supportive of just moving all the database-specific files into set.mm repo if that's what we want to do. I lean toward a rule like: * files associated with a given database go the metamath/set.mm repository (which could be renamed metamath/databases -- github manages repository aliases); * files which are more general and "website-wide" go to the metamath/website repository (which is the merging of the metamath/metamath-website-seed and metamath/metamath-website-scripts repositories). As for organizing the metamath/databases repository, I'm of course all for it, having opened https://github.com/metamath/set.mm/issues/1887 and https://github.com/metamath/set.mm/pull/3515. Benoît On Sat, Sep 30, 2023 at 5:08 PM Mario Carneiro <[email protected]> wrote: There is very little code involved in keeping a file somewhere else, there is just one cp line in the script. So I'm fine if we want to make an exception for certain files. But currently it's not clear that this is what is happening, and yet there is a lot of inconsistency, for example mmbiblio.raw.html is hosted on set.mm repo but IL's mmbiblio.raw.html is in the seed repo. Some kind of general rule for where to look for files would be appreciated, the simpler the better. On Sat, Sep 30, 2023 at 1:04 PM Jim Kingdon <[email protected]> wrote: On 9/30/23 04:27, Mario Carneiro wrote: Moreover, I am of the opinion that we should also move all the .html and .raw.html files from set.mm repo to the website repo, even though those files are more heavily trafficked than most other pages. When you want to add a new page, you need to modify the website repo anyway because otherwise it won't get copied correctly, and if it's living next to the scripts then it will be easy to maintain .raw.html and the necessary processing along with it. By comparison, there is very little "tandem update" work involved in an .html file versus the .mm file - they can generally be updated in any order, with the main issue being possible broken links if the mm file links to the html file or vice versa before the other has landed. I see the big issue as being the links from the html files to specific theorem names or math syntax. If the web pages now in the set.mm repo are moved, there would appear to be some kind of catch-22 in terms of which repository would have to be updated first and how we could build automated checks that the websites refer to valid syntax/theorems. In particular, mmil.raw.html changes very frequently and it is very much tied to updates to iset.mm and set.mm. Adding a new page is rarer, so I'm not sure that's a huge consideration (especially if we make the scripts better organized so we better understand where we need to add it). I'm not saying I'm implacably opposed to any change but I'd tread cautiously. On the whole I think the current organization has served us well (I mean, in terms of which web pages are maintained where, not all the details of how the scripts are written which hopefully we are already on the path to improving quite aside from moving web page files around). -- 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/c2fd9098-cd27-4557-f5f3-a5a4041c2461%40panix.com <https://groups.google.com/d/msgid/metamath/c2fd9098-cd27-4557-f5f3-a5a4041c2461%40panix.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/8667c6f4-e57f-4be4-aa0d-89f5ab64088an%40googlegroups.com.
