Hi, Il 07/05/20 15:52, Norman Megill ha scritto: > Set.mm is not a part of the programs. It is a file of data like a Word > or an Excel file. It should be kept in the current directory.
I tend to agree with this point of view: set.mm and any other Metamath database is just a file like any other document a user keeps in their home directory (the fact that it is under a git repository or not is an independent question: some users might want to use it, some might not). An application consuming or producing this file will ask the user to provide the path to such a file, defaulting to the CWD when no full path is provided. There is no need to implement a search path like $PATH for executables, to me. In case you are interested, here is how official Debian packages I am responsible for work; package "metamath" contains these files: /usr/bin/metamath /usr/share/doc/metamath/changelog.Debian.gz /usr/share/doc/metamath/copyright /usr/share/man/man1/metamath.1.gz The first is the executable, of course, in a standard $PATH directory. Then there are two documentation files that are mandatory per Debian policies, which respectively list the changelog of the Debian package and the licenses for all files included in the (source) Debian package. The last file is the manpage, which is distributed with the Metamath sources. As you can see, no databases here. For two reasons: first, Debian packages are compiled for something like 20 different architectures[1], therefore it is important not to put large architecture-independent files in them, otherwise they will be included 20 times in the Debian archive, wasting space. Architecture-independent files are to be put in architecture-independent packages, which are shared among different architectures. [1] See https://buildd.debian.org/status/package.php?p=metamath to see what happens to package metamath Second reason: a user might want to use the metamath program without dealing with the Metamath databases shared in set.mm. It is entirely legitimate. There is no need to install many megabytes worth of data is one simple executable is enough. For the same reason, the "metamath" package does not depend on, by merely suggests, installing the "metamath-examples" package. Third reason: Debian packages' expected lifetime is of many years. Once a distribution is released, its package are not touched except for important reasons, to minimize breakages for users who rely on the stability of that distribution. Therefore, both Metamath program and databases will not be updated anymore after the release, except unless very important bugs surface. For the program this is not a problem: except for new features, an old executable is as good as a new one. For databases it makes littler sense: if you want to participate to developing set.mm, it's ok to have an old Metamath executable in most cases, but it's probably not ok to have an old set.mm copy. You'd better download a recent copy (possibly using git) and work on that one. Therefore, I plan to include Metamath databases in Debian, but they will only be meant as examples, so that Debian users can test them if they install the package. Therefore they will be in a system-wide directory which is not writeable by users, like /usr/share/doc/metamath-examples. If users want to develop them, they'll have to copy them to their home directory and work there, or better download them freshly from the Internet. I am not sure this is useful in the context of this discussion, but in case it helps, good! Giovanni. -- Giovanni Mascellani <[email protected]> Postdoc researcher - Université Libre de Bruxelles -- 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/fefe5363-6739-4bdb-06f0-97d658e78d9f%40gmail.com.
signature.asc
Description: OpenPGP digital signature
