A simple Metamath web server for Rust, displaying proofs in the most basic way.
View these Metamath pages in action here.
First, install rust if you don't have it yet on your system.
Clone this repository, and set.mm
or the database you want to work with:
git clone https://github.com/metamath/set.mm.git –-depth 1
git clone https://github.com/tirix/metamath-web.git
The following commands can then be used to launch the server:
cd metamath-web
cargo run ../set.mm/set.mm
Once the server is started, it will parse the metamath database. Wait until it displays the "Ready" message: it shall be a few seconds. You can then switch to a browser and visit for example http://localhost:3030/mpeascii/o2p2e4 or the table of content and start navigating. The port 3030 is the default, see usage for configuration of the server address and port.
Just hit CTRL+C to stop the server once you're done browsing!
Here are some features implemented, and some which are still lacking:
mpeascii
) - this is Metamath "source code"mpeuni
) - this is the symbol-by-symbol typesettingmpests
) - structured typesetting (sts
feature needed)-b
)It is possible to serve pages formatted using structured typesetting, by activating the sts
feature, and browsing pages in the mpests
path.
cargo run --features sts ../set.mm/set.mm