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 <king...@panix.com> 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 metamath+unsubscr...@googlegroups.com. > 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 metamath+unsubscr...@googlegroups.com. To view this discussion on the web visit https://groups.google.com/d/msgid/metamath/CAFXXJSt-BLb6Q4jfs3KUGtGPav5bhXYzVx9Ersf6BP9vhU1Xew%40mail.gmail.com.
