That's awesome! I'd love to help and I've got some time off coming up. Where can I grab the source code to give it a whirl?
> On Jan 12, 2022, at 11:32 AM, David A. Wheeler <[email protected]> wrote: > > 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. -- 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/171DE9D7-126F-4E69-AA67-905BABD2A492%40gmail.com.
