Thierry, thanks so much!! I still intend to re-update the Metamath website, but other life events have been all-consuming. I'm hoping to get to it this weekend :-(.
--- David A. Wheeler > On Jan 11, 2022, at 10:48 PM, Thierry Arnoux <[email protected]> wrote: > > Hi all, > > Norm was manually updating the Metamath web pages and so they still stand at > their state of beginning of December. Some have expressed their wish to see > updated pages. > > I've written a short web server for Metamath web pages, metamath-web, and I'm > now running it on http://metamath.tirix.org:3030/mpests/tgoldbachgt.html. > > It serves the pages dynamically, meaning that it has parsed set.mm, and then > builds and serves the pages on the go as they are requested (I can't help > mentioning here Mario described that as super-cool in a recent comment ;) ). > > For now, it only serves set.mm pages. It would not be very hard to extend it > to e.g. iset.mm. > > There are only two renderers implemented until now: > > • the unformatted ASCII source file, which uses "mpeascii" in the path, > • the so-called "structured typesetting" (STS), with "mpests" in the > path. > I've not yet implemented a unicode renderer (as in "mpeuni") but this shall > be pretty straightforward once parsing the $t typesetting section of metamath > files is implemented. > > This is still very much experimental and incomplete, so of course it does not > compare with all the functionalities built in over the years in the > metamath-exe pages, but I wanted to already share it. Here are some features > which are still lacking, roughly in the order I'd like to add them: > > • only theorems are displayed, axioms and definitions are not (pages > are in error). I will put there the "syntax proof" as in the original web > pages, > • theorems hypotheses and final statement are not shown at the top of > the page, it's just the proof right now, so the final statement is at the > very bottom of the page, > • there is no navigation to the next/previous theorems in the database, > • there is no table of content, > • the embedded math in-line in comments between `` is not formatted, > • the $d distinct variables are not displayed, > • the "used by" list is not built. > To update the pages, I have to manually fetch the new set.mm version and > restart the server. This however is very lightweight and takes only a few > seconds, compared to the regeneration of a whole directory with 30000+ files. > I believe this can be automated. > > The server code is roughly 300 lines of code, plus another 200 for STS, so it > shall not be too hard for anyone to join its development - any help is > welcome! > > I hope this utility will help others discover some the latest theorems which > are not yet on the us2 server: > > • Jannik's shorter proof of the irrationality of the square root of 2, > • Scott's full-eta axiom for the surreal numbers (and more), > • Alexander's shorter version of Huneke's proof , and sum of degrees of > a finite pseudograph, > • Glauco's inferior limit of a countable set of sigma measurable > function, > • my last step of the Ternary Goldbach Conjecture > Sorry for those I missed! There is of course Jim's intuitionistic proof of > Bezout's theorem, I hope I can setup the server soon for iset.mm! > > BR, > _ > Thierry > > > > > -- > 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/8899df6a-4d70-d72a-585f-1131f7857075%40gmx.net. -- 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/9E07EBC1-1545-4E5B-8C86-475EE5053876%40dwheeler.com.
