I've implemented a subset of the Metamath web site by way of downloading a .mm
file and processing it on the client side.
Code:
https://github.com/sorear/smm-webui
[The README there should be fairly up to date, just beware that it requires
downloading ~100MB of dependencies and I have no idea if it works on Windows]
Prebuilt version:
https://smm.divshot.io
[Is there a better choice for this? github pages does not support custom
routes so I went looking for an alternative, and there are surprisingly few
players in this space it seems.]
Features: Most of them should be fairly discoverable. Two that aren't:
1. Layout of the theorem list switches significantly at 768 CSS pixels width.
The breakpoint may not be optimal.
2. Click on a subexpression to reveal grouping.
Non-Features (things it doesn't do yet):
1. Comment markup parsing
2. Meaningful proof display
Things which surely need work:
1. The bottom copy is something I just made up, and is speaking for people I
don't actually have authority to speak for. Wording tweaks accepted.
2. The ?go= / ?node= thing sucks, but it was the simplest thing that I knew how
to make work. I've been thinking of ways to do better, no firm ideas yet.
3. I need to figure out how to do automated testing for this; it's worked quite
well for the smm core but is not used in smm-webui yet.
It _seems_ to work in Chrome 43, Safari 6, Firefox 38, Firefox 39, and IE 10,
although there are a couple styling issues in the last oen (there's a
superfluous margin on the top of the page and alignment is broken in the inline
outline nav).
Some other thoughts:
1. Since it downloads a .mm file and then works with that, the bandwidth
behavior is significantly different from a metamath mirror: ~250kb of code,
then 9.2 MB of
set.mm (with transparent gzip compression), then nothing
thereafter. If you want to run a mirror and not rely on free CDNs that could
decide to quit at any time, the bandwidth usage will probably be higher for
brief visitors and lower for long visits...
2. Especially if they switch math mode halfway through, because there's only
one version of the database.
3. Working from .mm files means we can provide editing options later. Details
TBD.
4. I've started down the path of extending .mm file syntax for this. See:
https://github.com/sorear/smm-webui/blob/master/public/assets/set-config.mm
--
Questions? Comments? Thoughts?
-sorear