Broken links

[GinoGiotto]

Mentioned in #10

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).

In the mailing list https://groups.google.com/g/metamath/c/P0D4h2uIj2k Mario Carneiro wrote:

I'm afraid tirix will have to fix that himself, I don't know where the source or hosting for that site is. (Although, I think it would be quite possible to integrate those pages into the main site now.)

I think integrating your website into the main one is a good proposal since I do share the desire for a more modern appearance of the webpages. Of course it's up to you to decide its future (since you are the author). In case we would decide to go further, such decision would probably need to be discussed with a wider audience in the metamath mailing list, to collect some opinions and ideas. I personally like your website, it does need maintenance, but once it's done, it would be a nice upgrade for metamath.

[tirix]

I'll use this issue for a more generic discussion, even if it's not so much in the spirit of "one issue per problem" :-)

There are 3 directions to extend this project:

• up-to-date set.mm : the online version currently runs on an old version of set.mm. I would like to move to a newer version, and even pull the latest set.mm every night. This requires a bit of scripting, and also for STS, for the set.mmsts file to be updated regularly when new syntax is added to set.mm.
• polishing and features: Thanks a lot for your help there! There is more to do, and we can track them with different issues.
• overall architecture and content: Here I'm thinking for example about Lean's community pages as an example. They are a bit more modern, shows a clear table of contents. We could also have a slick home page, showing a few links to interesting resources (like explainer videos), biggest/most recent achievements (like acyclic graphs or Gödel models), and still have pointers for more detailed information.

[GinoGiotto]

• up-to-date set.mm : the online version currently runs on an old version of set.mm. I would like to move to a newer version, and even pull the latest set.mm every night. This requires a bit of scripting, and also for STS, for the set.mmsts file to be updated regularly when new syntax is added to set.mm.

Sounds awesome! I would personally appreciate this feature, and it would definitely encourage to check your website more often, since it would show the newest additions and revisions.

• overall architecture and content: Here I'm thinking for example about Lean's community pages as an example. They are a bit more modern, shows a clear table of contents. We could also have a slick home page, showing a few links to interesting resources (like explainer videos), biggest/most recent achievements (like acyclic graphs or Gödel models), and still have pointers for more detailed information.

A lean-like website looks pretty good! I think the main problem with the official metamath website is that it's too verbose. Lean has a much cleaner/clearer webpage which goes straight to the point. This is important for first time users, which don't know where to find the relevant stuff (I'm thinking about my own experience in September 2022, when I first discovered metamath). At that time I remember I was mainly interested in where are the theorems and where are the main programs (metamath.exe, metamath-knife ecc..), so from my perspective I would highlight the attention on that. A small introduction similar to Lean I think is good enough. The main purpose of the homepage is to catch the attention, and once that's achieved the user can be directed to the metamath-book for more in-depth information.

Switching to https instead of http would also be a nice improvement.

[tirix]

Switching to https instead of http would also be a nice improvement.

I did that little bit tonight, URLs like https://metamath.tirix.org/mpests/fprodefsum now work.

Agreeing with all the rest you wrote.