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:

• [x] support for 3 typesettings:
  • [x] ASCII (mpeascii) - this is Metamath "source code"
  • [x] Unicode (mpeuni) - this is the symbol-by-symbol typesetting
  • [x] STS (mpests) - structured typesetting (sts feature needed)
• [x] display axioms and definitions' syntax proof
• [x] links to other theorems in comments
• [x] links to bibliographic references (see command line option -b)
• [ ] in-line math in comments
• [x] summary of the theorems (hypotheses and statement) before the proof
• [x] navigation to next/previous theorem in the database
• [x] navigation between the different typesettings
• [x] table of content
• [ ] distinct variables
• [ ] list of uses

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

• metamath-knife for parsing metamath file and obtaining proofs,
• handlebars for templating,
• warp for the web server.
• nom for parsing the STS definition file.