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 <https://github.com/tirix/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 <https://github.com/metamath/metamath-exe/issues/31#issuecomment-1006328448> 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 <http://metamath.tirix.org:3030/mpeascii/tgoldbachgt.html>" in the path, * the so-called "structured typesetting" (STS), with "mpests <http://metamath.tirix.org:3030/mpests/tgoldbachgt.html>" 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 <http://metamath.tirix.org:3030/mpests/sqr2irrlem.html>, * Scott's full-eta axiom for the surreal numbers <http://metamath.tirix.org:3030/mpests/noeta.html> (and more), * Alexander's shorter version of Huneke's proof <http://metamath.tirix.org:3030/mpests/frgr2wwlk1.html> , and sum of degrees of a finite pseudograph <http://metamath.tirix.org:3030/mpests/finsumvtxdg2size.html>, * Glauco's inferior limit of a countable set of sigma measurable function <http://metamath.tirix.org:3030/mpests/smfliminf.html>, * my last step of the Ternary Goldbach Conjecture <http://metamath.tirix.org:3030/mpests/tgoldbachgt.html> 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.
