> On Feb 27, 2023, at 5:27 PM, Thierry Arnoux <[email protected]> wrote:
>
> And since we're there, I'd also like to recall this other live site:
>
> http://metamath.tirix.org:3030/mpests/toc
>
> All pages are rendered dynamically, there are 3 modes:
>
> - ASCII - http://metamath.tirix.org:3030/mpeascii/areacirc
> - Unicode - http://metamath.tirix.org:3030/mpeuni/areacirc
> - MathML - http://metamath.tirix.org:3030/mpests/areacirc
>
> Source code here. https://github.com/tirix/metamath-web
That *is* nice. The MathML in particular is nice.
Is there a list of Metamath database view generation tools? I can think of:
- https://github.com/digama0/mm-web-rs
- https://github.com/tirix/metamath-web
I know there are others. At least, there was one that let you expand/contract
proof steps, which one was that?
So clearly we should talk about options to completely replace the current
process. Obviously we *could* replacing pre-generation with generating them
dynamically;
alternatively we run these other tools as pre-generators.
I really *do* want it to be possible to view the key results without
client-side JavaScript,
but this code & Mario's can clearly meet that need. In the case of tirix's code,
just view ASCII and/or Unicode and you're fine.
I do have a few specific comments on tirix's tool. They're all fixable of
course:
1. I can't read most of the text because most of the text has low contrast.
That includes description, step numbers, hyp refs, ref blue boxes, text
expressions in mpascii, & navigators. Can you please change its CSS to have
strong text contrast? It should be readable by color-blind people on a phone in
sunlight. Creating strong text contrast *important" but also *easy* - it's just
some CSS tweaks.
2. The text just runs off to the right, instead of going over multiple lines,
making long ones unreadable. That's important but easy for the non-MathML case
(just a little CSS), though I don't know how hard that is for MathML/MathJax.
3. I think it's important we support existing URLs. That's easy with
pregeneration, just rename to taste. If this is dynamically generated, that
would require some changes to support the .html endings *and* support returning
static pages.
4. This one omits many of the capabilities of the metamath-exe generator, e.g.,
compare with <https://us.metamath.org/mpeuni/areacirc.html>. That includes:
Distinct variable group: 𝑥,𝑦,𝑅
Allowed substitution hints: 𝑆(𝑥,𝑦)
Colors of variables (off, setvar, class) ... this one isn't as important to
me & would be a lot of work, so I'm not fussy there.
Syntax hints (with links to them)
List of axioms used (with links)
List of definitions used (with links)
List of theorems that reference it (with links)
--- David A. Wheeler
--
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 [email protected].
To view this discussion on the web visit
https://groups.google.com/d/msgid/metamath/508D4E31-7626-4F3F-A0DA-F78E5B2FAFF1%40dwheeler.com.
