On Mon, 4 May 2020 23:58:46 -0700 (PDT), savask <[email protected]> wrote: > 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.
We *definitely* don't want *unasked* changes no matter what. We should support those who want to just put everything in one directory and control it, just like now. I think that would be easy. But that isn't how most people expect software to work today. Typically software is installed in a "standard place". In Linux/Unix those are /usr/bin, /usr/local/bin, ~/bin, or ~/.local/bin. On Windows those are "C:\Program Files". You run an installer or select a package, and you're done. As far as "accumulate over time", that's a fair concern. The best solution might be, as B. Wilson suggests, to use the standard packaging conventions. Every modern system has a package manager that makes it easy to install AND REMOVE software so that it won't "accumulate over time'. > 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 - The goal is to make that even easier. > 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). There certainly is a standard directory for them. On Windows it is "%HOME%\My Documents" (shown as "Documents"). On Linux/Unix (GNOME and KDE) it is "$HOME/Documents". I'm trying to remember the MacOS one, I think it's "$HOME/Documents" there too (though MacOS uses /users instead of /home for home directories). You don't have to use the standard directory for documents, and you shouldn't have to use the standard directory here either. But most users don't want to *have* to configure the tools; they want a "reasonable default" and then they can change if they want to. > 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. Yuk. I don't want to become a version control program. I want the version control program to be the version control program. If you want to become a version control program, that's up to you :-). But we should not require people to have to constantly remember to do that. People are terrible at consistently doing that. When I start up mmj2, I want it to have a "reasonable default". If you want something different, excellent... but many people just want to get the job done. Every choice they *MUST* make is a mistake, though of course I don't want to *prevent* choices. > 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. By definition today you have to do something to tell metamath where the file is, because there's no default. The goal isn't to remove that ability; the goal is to create a reasonable default when you *DON'T* say where it is. A side annoyance: .mm is already a standard extension (Objective-C). I don't know if anyone does both Objective-C and Metamath development... :-). --- 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/E1jVyX2-0001da-U6%40rmmprod06.runbox.
