On Mon, 4 May 2020 18:41:16 -0700 (PDT), "'B. Wilson' via Metamath" <[email protected]> wrote: > Thank you for starting this discussion. As a package manager, I certainly > empathsize strongly with efforts to make the current installation more > standards-compliant. In that vein, I would recommend against defaulting to > $HOME installations. ... Instead, how about following the Filesystem > Hierarchy Standard, instead?
We certainly could! I was suggesting to slightly regularize what people were *already* doing in the Metamath community, in the hopes that it would make regularizing easier for existing users. Using the more general FHS standards instead would require more changes to what current Metamath users are doing. But FHS *is* what everyone (except Windows) does, so using the standards might make it a lot easier for *new* users to join the fun. Metamath-exe already supports all of this. I wrote its autoconf files, and of course autoconf already supports all this (PREFIX, DESTDIR, etc.). We could just tweak its install instructions. Ideally metamath-exe would come with a pregenerated "config" file, but I'll have to talk Norm Megill into doing that :-), and the current process *does* work. > Similarly, by using the convention of a PREFIX variable at installation, > one could install these tools in your local home directory by setting > PREFIX=$HOME/.local. To be fair, FHS does *not* include "$HOME/.local". Many people, including me, have used "$HOME/bin" and friends for this purpose. I think that the PREFIX="$HOME" convention is far older. But you're right that the PREFIX="$HOME/.local" convention has been growing in popularity, e.g., it's in the systemd file hierarchy page: https://www.freedesktop.org/software/systemd/man/file-hierarchy.html One argument *for* the use of $HOME/.local/bin over $HOME/bin is that this way your home directory doesn't get cluttered up with "non-working data" directories like "$HOME/bin/". Historically $HOME/bin had more support, but it looks like $HOME/local has increased in its use over the years. > It's not uncommon for PATH to already contain $HOME/.local/bin, so in many > cases a local installation would Just Work, without requiring a > metamath-specific entry. At worst, instructing users to add this entry > simply instructs them to follow existing conventions... Fair enough. This would be a bigger change, but I'm game for doing that instead when installing metamath-exe and mmj2 on non-Windows systems. Maybe others here will be willing to make changes, or at least be willing to accept that the defaults are different, if it helps people join. Of course, if people *package* the executables, then they would go in the usual place. Brew puts binaries in /usr/local/bin, native system package managers would put in them in /usr/bin. Which is all straightforward, since these are the standard ways to do things. There are some issues: * What about Windows? * Where does set.mm get stored? I think it still ends up in $HOME/set.mm by default, because that is *not* a system-shared resource - that's a version-controlled set of files that you're working on & need to edit. * Where do mmj2 .mmp files get stored? * How can we make it easy for mmj2 to find its built-in tutorial? * I'm not sure what the conventions are for Java .jar files, but I'm sure there is one. The mmj2 project already has a comment that installing mmj2 is too hard. If we could make it really easy to install & update things, that would be great. --- 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/E1jVoGn-0000fx-0g%40rmmprod06.runbox.
