HomePage RecentChanges

metamath program discussion

NOTE: to update this wiki your Username must be "whitelisted" by Aaron. For the purposes of discussion about Metamath or mmj2 I authorize you to use Username "ocat" – but in your update text please input some identifier (pseudonym, whatever) so that we know who is saying what. Thx. ocat 23-Nov-2007


While the current rage in Metamath software is mmj2, now and then proposals come up for tweaking the stodgy original metamath program. I added this page to discuss them.

Tooltips on Metamath web pages

Based on a suggestion by Reinder Verlinde, I added tooltips for mouseovers on proof step hyperlinks, for example steps 2 and 3 of a1i. This adds about 4% to the size of an average page.

It is also possible to add these tooltips to other hyperlinks, with a corresponding increase in page size. I invite discussion of where people might find tooltips the most useful. – norm 20 Nov 2007

Compressed webpages

Nearly all browsers can handle compressed files, so why not shrink the metamath html files: Compressed_HTML_makes_your_pages_zippy? That would be especially useful with the .gif's. And you could add tooltip flyovers to all assertion labels on each page. Or not :-) --ocat
P.S. Thinking about this option, it come to mind that you could just run a utility to create a .gz version of each file output by Metamath.exe – that would probably speed up download times for the web pages by 75% and reduce transmission costs. So this makes sense as a standalone enhancement, regardless of the tooltip flyovers. --ocat
This is a good suggestion. As an experiment, I gzipped all the mpegif/mpeuni .html pages except mmrecent.html on the us2 server. Maybe this is adequate - I didn't relish futzing around with htaccess etc. It seems to work, and maybe apache does this automatically already, not sure. Maybe some apache expert could enlighten me. It does seem that if you request a .html it automatically opens .html.gz if the .html isn't there. I'm not sure what the impact on the volunteer mirrors might be - I've tried to have static-only pages and keep server-side software issues away from them, in case they use Windows IIS or whatever. – norm 21 Nov 2007
Mozilla automatically un-zips web pages with suffix ".gz". It appears to be picking the ".gz" suffix file automatically -- but I cannot be absolutely sure. Perhaps post a Note or News item on US2 about the topic. --ocat 21 Nov 2007

It looks like IE6 also works with only the .html.gz on the server (no uncompressed .html). It surprises me that it would handle the gzip format, since that is an "open source" thing (e.g. PNG alpha transparency doesn't work in IE6 after years of user complaints). So: is Apache actually sending the compressed page to IE6, or is Apache decoding it on the fly to send to IE6 if IE6 tells it can't handle it?

Another experiment: if only the .html.gz is present on the server, wget retrieves the gzipped version for both .html and .html.gz specified in the URL. If both the .html and the .html.gz versions are on the server, wget retrieves the uncompressed .html version with a .html URL, and the compressed .html.gz version with a .html.gz URL.

Lynx also works even if only the .html.gz is on the server. – norm 21 Nov 2007

IMHO, it seems to me that what you should do, assuming that the mirror sites are black boxes and that you are not in communication with the mirror site operators, is to optimize your webserver while sending the mirror sites exactly what they get today. That means, I think, creating ".gz" versions of all of your webpages – regular and us2 -- and updating your .htaccess file as described in the above article. It is preferable to do this than to rely on what appears to be undocumented functionality in the server and browsers. Regarding the mirror sites, when you update your website to create the download deltas, you would first delete all of the ".gz"s, update your webpages, create the deltas, and then recreate the ".gz"s. The .htaccess you use on your server need not match the mirror sites' settings – they run their system however they please. However, if they did wish to optimize their services similarly it would be trivial for them to create their own ".gz" files. --ocat 21 NOV 2007