mm-web-rs server support

[Mario Carneiro]

Hi All,

I just wanted to share some metamath-knife progress: The https://github.com/digama0/mm-web-rs experimental metamath web site clone is now able to draw complete theorem pages, including the step list, forward references and axioms used, comment markup, dummy variable and allowed substitution hints, basically everything visible on the page, all powered by the metamath-knife API. Furthermore, as a result of the switch to a rust backend it is now quite simple to add a web server, so now you can run "mm-web-rs server" and it will serve pages like http://localhost:8080/mpeuni/pnt.html as you would expect from a static server.

Mario

[Thierry Arnoux]

Hi there,

Just to clarify, this second server is different from the 'metamath-web' I was mentioning two weeks ago in another post, and which provides the pages at http://metamath.tirix.org:3030/.

This shows how easy it is now to write a small server which when using the metamath-knife library as a starting point!

The functionalities covered are slightly different, but both can be completed fairly easily. I think Mario put an emphasis on reproducing the same functionality as Norm's original pages, while I took some liberties with the formatting, and added the "structured typesetting" as a display option.

Mario, there's another project I'd like to start based on metamath-knife, that would be an LSP server similar to what you've been doing for MM0, which would allow to turn Visual Studio into a tool for viewing and editing not just Metamath source files, but maybe also Metamath proof files - that would certainly be a lofty goal! What I have is really just the scaffolding, but I'll start to share it here.

Could we join forces for that one? Is anyone else interested?

_
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 metamath+u...@googlegroups.com.
To view this discussion on the web visit https://groups.google.com/d/msgid/metamath/CAFXXJStpvP5oC7QvwxroZbEdZHEfcSzAB4e2EVf7Coo-S0XZgw%40mail.gmail.com.

[Mario Carneiro]

mm-web-rs now supports generation of the auxiliary pages: mmtheorems.html, mmrecent.html, mmtheoremsall.html, mmdefinitions.html, and mmascii.html, which was the last remaining piece to completely replace metamath-exe web site generation functionality. The next step is to add it to the website build (under an experimental subfolder) so that regular users can play with it and find differences with the original.

[Mario Carneiro]

It requires some changes to the mmrecent.html CSS, so for now a copy is hosted at https://github.com/digama0/mm-web-rs/blob/master/mmrecent.raw.html . The pages generated by mm-web-rs are significantly different under the hood, making use of modern HTML5, although it's still dressed up in the web 1.0 clothing of the original website. Once we've confirmed that the site isn't missing anything critical, I want to update the site design a bit (and possibly finally ditch the GIF pages!). I'm working on this in my spare time between my other projects though, so progress will probably be slow. Feel free to run https://github.com/digama0/mm-web-rs locally before the beta version goes live.