Thanks Thierry, this looks great ! Both "ascii" and "mathml/mathjax" are useful (the latter may lure more people to metamath), and I hope "unicode" will be available soon. Actually, for metamath.org, I have been thinking for some time that gif support could be deprecated and replaced with "ascii".
Where you mention the navigation links next/previous, it would also be nice to have links to toggle between the three versions (ascii, unicode, mathml/mathjax) of the currently displayed theorem (and maybe also a link to the corresponding metamath.org page). Concerning your ~tgoldbachgt : it looks like the conclusion should be Step 127: no need to go to the more complicated Step 135, which does not bring anything. (?) Benoît On Wednesday, January 12, 2022 at 7:40:55 PM UTC+1 Glauco wrote: > Great job, Thierry. > > Il giorno mercoledì 12 gennaio 2022 alle 04:48:37 UTC+1 Thierry Arnoux ha > scritto: > >> 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/ad7e9314-b275-40bf-a858-a1bb8b6fda85n%40googlegroups.com.
