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
<http://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 <http://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
<http://metamath.tirix.org:3030/mpests/tgoldbachgt.html>.
It serves the pages dynamically, meaning that it has
parsed set.mm <http://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 <http://set.mm> pages.
It would not be very hard to extend it to e.g.
iset.mm <http://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 <http://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 <http://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
<https://groups.google.com/d/msgid/metamath/ad7e9314-b275-40bf-a858-a1bb8b6fda85n%40googlegroups.com?utm_medium=email&utm_source=footer>.
