On Wed, 6 May 2020 00:45:22 -0700 (PDT), "'B. Wilson' via Metamath" <[email protected]> wrote: > Would it make sense to have "search path" variables for metamath and mmj2? > > The FHS describes /var/lib and /var/local/lib as places for "variable data" > associated with programs in /usr and /usr/local, respectively. Ostensibly, > the purpose of /var is so that /usr can be make read-only. In this respect, > it makes sense to me for the set.mm repo to be checked out in a directory > like /var/lib/metamath.
No, I think that's not the right analogy, for several reasons. First, the "set.mm" repo is basically a shared document that we are all editing; it is *not* a constant unchanging file. We're managing its versions with git. It is *far* simpler to dedicate different directories to different repos than to try to merge multiple repos into 1 directory. Second, set.mm is *NOT* the only database. There are other databases that are in different repos. Trying to use git to manage different repos merged into one directory is *awful*. Third, /var/lib is intended to provide a *single* view to all users of that system, but that wouldn't make sense. If you have a multi-user system (less common but it still happens), you would definitely NOT want a single unpacked set.mm file in /var/lib. You might copy a git repo there, but in a multi-user system the git working directory is almost *necessarily* in a home directory. > What about mmj2? I haven't tried out mmj2 yet, but would the above apply > there too? The problem is that mmj2 needs to know where the database is. It currently gets that information through a baroque pair of command line parameters and a file with commands. The "obvious" solution is to provide simple command line scripts & command files that assume it's in one place. If you don't like that placement, you can copy & edit those files to do whatever you want it to do. That seems like the easy way, at least to get started. -- 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/E1jWMrC-0005vQ-OV%40rmmprod06.runbox.
