Should eliminate the GIF directories & just use Unicode?
78 views
Skip to first unread message
David A. Wheeler
Jan 2, 2023, 10:42:35 AM1/2/23
to Metamath Mailing List
Should eliminate the GIF directories & just use Unicode? That is, for example,
redirect all uses of <https://us.metamath.org/mpegif/> to
<https://us.metamath.org/mpeuni/> ?
I welcome comments/thoughts. A few notes are below.
--- David A. Wheeler
===
The Metamath project has, for many years, generated HTML pages with embedded GIF images.
For a very long time this was the only practical way for most people to read the results.
However, today practically all web browsing systems support Unicode.
We switched to Unicode as the default years ago. Many
people's fonts didn't cover math symbols, but when we posted web fonts (my fault :-) )
that problem was basically solved.
At this point I think the primary reason to keep GIF directories is to make copying text easier:
https://us.metamath.org/mpeuni/mmset.html#textonly
That's a perfectly valid use case, as long as people are actually doing it.
I don't know how many people find that useful.
Generating everything twice takes time, but that's not a big deal.
It does create more opportunities for error & complicates our scripts.
The big advantage of eliminating the GIF generation would be to save disk space.
Because we generate everything twice, we use about double the disk space.
Anyone can see our current disk space status by viewing this page:
https://us.metamath.org/status.txt
The main drive /dev/sda has 26G, with 1.3G available (95% used).
We can pay for more space, but there's a jump in price.
We should be fine for a long time as long as we keep log files limited in size,
but any error in its configuration can cause problems (as illustrated recently).
There may be other issues I'm not aware of.
redirect all uses of <https://us.metamath.org/mpegif/> to
<https://us.metamath.org/mpeuni/> ?
I welcome comments/thoughts. A few notes are below.
--- David A. Wheeler
===
The Metamath project has, for many years, generated HTML pages with embedded GIF images.
For a very long time this was the only practical way for most people to read the results.
However, today practically all web browsing systems support Unicode.
We switched to Unicode as the default years ago. Many
people's fonts didn't cover math symbols, but when we posted web fonts (my fault :-) )
that problem was basically solved.
At this point I think the primary reason to keep GIF directories is to make copying text easier:
https://us.metamath.org/mpeuni/mmset.html#textonly
That's a perfectly valid use case, as long as people are actually doing it.
I don't know how many people find that useful.
Generating everything twice takes time, but that's not a big deal.
It does create more opportunities for error & complicates our scripts.
The big advantage of eliminating the GIF generation would be to save disk space.
Because we generate everything twice, we use about double the disk space.
Anyone can see our current disk space status by viewing this page:
https://us.metamath.org/status.txt
The main drive /dev/sda has 26G, with 1.3G available (95% used).
We can pay for more space, but there's a jump in price.
We should be fine for a long time as long as we keep log files limited in size,
but any error in its configuration can cause problems (as illustrated recently).
There may be other issues I'm not aware of.
Samiro Discher
Jan 2, 2023, 10:49:11 AM1/2/23
to Metamath
Another issue that immediately comes to my mind is that in such case one shouldn't invalidate old hyperlinks,
e.g. https://us.metamath.org/mpegif/id.html should be redirected to https://us.metamath.org/mpeuni/id.html
in case the
mpegif pages are removed.
Glauco
Jan 2, 2023, 2:47:05 PM1/2/23
to Metamath
The gif version has a useful feature: when you hover on a symbol, the ascii string for the symbol is shown.
Would it be possible to have the same behavior in the Unicode version?
Benoit
Jan 2, 2023, 3:49:51 PM1/2/23
to Metamath
I think that we should drop the GIF directories, to lighten maintenance, and that we should in place add an ascii version, https://us.metamath.org/mpeascii/, so that the feature mentioned by Glauco stay (and be even better).
The ascii pages should not be hard to generate: in the metamath.c function generating the unicode pages (generated by the command MM> SHOW STATEMENT */HTML), there should be a line saying:
"for token in statement {fetch the htmldef of the token and display it}"
which should be changed to:
"display statement".
That is, it displays precisely the statements as displayed on the command line of MM> , maybe with the added color code, maybe with italic if it's the same font, but nothing more.
David A. Wheeler
Jan 2, 2023, 4:53:29 PM1/2/23
to Metamath Mailing List
> On Jan 2, 2023, at 2:47 PM, Glauco <glaform...@gmail.com> wrote:
>
> The gif version has a useful feature: when you hover on a symbol, the ascii string for the symbol is shown.
>
> Would it be possible to have the same behavior in the Unicode version?
https://www.w3.org/TR/2016/REC-html51-20161101/dom.html#the-title-attribute
If we create a span and use a "title" element we could do the same thing.
I tried out both Firefox and Chrome (on MacOS) and after having for just a moment I saw the tooltip.
My demo HTML is below, in case anyone else wants to try the experiment.
--- David A. Wheeler
=======
<html>
<body>
<p>
This is a tooltip demo for althtmldef "->" as " → ";
<p>
A<span title="->"> → </span>B.
</body>
</html>
Mario Carneiro
Jan 2, 2023, 9:01:23 PM1/2/23
to meta...@googlegroups.com
I think it's not worth it to have ascii symbols in title attributes on every character. This will unnecessarily blow up the page size quite considerably. I think Benoit's suggestion of an all-ascii version of the pages is better - I think this is already implemented in one of the alternate verifiers, and it seems like a better overall approach if the purpose is to get expressions which can be copy-pasted into e.g. an mmj2 worksheet or an .mm file compared to a bunch of tiny tooltips.
--
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/FF0A4BFB-8BAC-4482-83ED-E409B453552F%40dwheeler.com.
Jim Kingdon
Jan 2, 2023, 11:25:10 PM1/2/23
to meta...@googlegroups.com
There are a lot of ideas on this thread which might be worth
doing, but the redirect from mpegif to mpeuni is the only which is
in my mind a (likely) prerequisite for retiring mpegif. Most of
the others we could do later if we find we wish we had them.
--
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/4d0b2379-fff3-4712-b43f-2a1ba194c13en%40googlegroups.com.
Mario Carneiro
Jan 2, 2023, 11:26:32 PM1/2/23
to meta...@googlegroups.com
I don't think the redirect would be that difficult, it is a one time apache configuration thing, possibly plus updates to the mirrors.
To view this discussion on the web visit https://groups.google.com/d/msgid/metamath/f420e0ce-f888-e26a-c8fc-32ed56a3c78d%40panix.com.
David A. Wheeler
Jan 3, 2023, 11:14:04 AM1/3/23
to Metamath Mailing List
> On Jan 2, 2023, at 11:26 PM, Mario Carneiro <di....@gmail.com> wrote:
>
> I don't think the redirect would be that difficult, it is a one time apache configuration thing, possibly plus updates to the mirrors.
but the basic principle is the same. We would just need to edit this file on GitHub:
https://raw.githubusercontent.com/metamath/metamath-website-scripts/main/us.metamath.org
A quick intro to nginx rewrite rules is here: <https://www.nginx.com/blog/creating-nginx-rewrite-rules/>
So we'd add a line like this:
rewrite ^/(...)gif/$ /$1uni last;
Then on the main website we'd log in and run "git pull; ./build-system.sh" to do the update.
The mirrors would have to do their own config changes, we don't really control that. Hopefully it wouldn't matter much.
--- David A. Wheeler
Reply all
Reply to author
Forward
0 new messages