Faint text + wff and class definitions don't work

[GinoGiotto]

I like your website @tirix , I found myself using it more than the original Metamath one. I only have two issues:

I find the main text hard to read. If I zoom in it seems to be black, but from far away it appears as a very faint grey, could you make it darker (or thicker) ?

All wff and class definitions that I visited don't appear, it always shows Could not format assertion. Unkown statement

[tirix]

I did a few changes this weekend and among others, I've made the text darker, and enabled the display of axioms and symbol definitions like ~wn.

The site is now accessible at http://metamath.tirix.org/mpeuni/wn.

[GinoGiotto]

Nice! The text looks better now and symbols definitions are working.

There are some other issues I noticed:

Many links from http://metamath.tirix.org/index.html seems to be broken. For example if I click http://metamath.tirix.org/mpeuni/mmset.html it gives a 404.

http://metamath.tirix.org/mpeuni/bm1.1 The hypothesis bm1.1.1 doesn't show. Is it because the non-freeness symbol is missing?

http://metamath.tirix.org/mpeuni/toc?ref=61 This webpage is empty, maybe it doesn't render tables?

http://metamath.tirix.org/mpeuni/ax-mp If I click on min or maj then it gives a 404. More generally this issue appears when I click on hypotheses. Are they not intended to be clickable?

[tirix]

There are some other issues I noticed

At first sight they are all different problems, maybe we could track each in a separated issue? Anyway let me try to answer:

http://metamath.tirix.org/mpeuni/bm1.1 The hypothesis bm1.1.1 doesn't show. Is it because the non-freeness symbol is missing?

I tried and it worked for me. Maybe you need to refresh the page? (or clear your cache?)

http://metamath.tirix.org/mpeuni/toc?ref=61 This webpage is empty, maybe it doesn't render tables?

It does not even display any "chapter comment" at all. That's a new feature to be added. With the last version of metamath-knife, it should be easy.

http://metamath.tirix.org/mpeuni/ax-mp If I click on min or maj then it gives a 404. More generally this issue appears when I click on hypotheses. Are they not intended to be clickable?

Good point. One solution is to make then not clickable, another would be to display the syntax breakdown for them. The first option seems to be much easier, and I don't see the interest of showing the syntax breakdown just for those and not for all proof steps.

Many links from http://metamath.tirix.org/index.html seems to be broken. For example if I click http://metamath.tirix.org/mpeuni/mmset.html it gives a 404.

Yes, that's a more generic point about the architecture. I'm not sure whether this should be a kind of mirror, with all pages from the original website, just an alternative way to display proof pages, or a completely different site about Metamath. Porting mmset.html maybe only makes sense in the first case. The project started with:

• the idea to build proof pages on the go as they are served,
• a will to have more modern looking pages (but that's so
• a desire to port "structured" typesetting to Rust ...and just because I could do it (and I found it fun).

[GinoGiotto]

At first sight they are all different problems, maybe we could track each in a separated issue?

Ok, I'm closing this issue since it's solved and open new ones to keep topics in order.