I just wanted to make a small comment, based on personal experience. Back when I first tried metamath, I found it very convenient that it was shipped as a standalone executable. I don't really like programs which "clutter" the home directory or make some unasked changes to the file system (especially to "invisible" directories like .config), since these things tend to accumulate over time. In my opinion, one of the strongest sides of metamath is that it's very easy to set up and play with, essentially you just need to download one tarball and run the executable - all main databases are already at your disposal. It is as easy to remove without any traces being left, which is a plus side in my opinion (unless you want to make people stick to metamath no matter what, I guess :-) ). There's also a growing tendency to ship programs as standalone packages (like appimage), but I guess metamath tarball is already more or less a standalone package.
Same goes for set.mm and other databases - these are just input for metamath and mmj2, so I don't think there should be a standard place for these (I don't think there is a standard directory for .tex or .doc files). As for the hypothetical event of losing your set.mm progress by installing a new metamath version over it - that could be easily fixed by adding date to the set.mm filename used in metamath.tar.gz, as in set_05.05.20.mm. Personally, I have various versions of set.mm scattered all over the file system (for a good reason), so it would be unfortunate if I had to re-configure metamath to support that. -- 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/ab0f8732-d0ed-464a-a5c1-8bfea9a3fca4%40googlegroups.com.
