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/629e88fb-7336-4fa8-93de-59d2d96866afn%40googlegroups.com.
