> 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.
On Thu, 7 May 2020 21:17:16 +0200, Giovanni Mascellani <[email protected]> wrote: > 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 Yes, that's key. A Metamath database is a file, like any other document, and *not* necessarily part of any particular executable. > (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). I don't think we should *require* git use, but whatever conventions are recommended through installation should make it easy to use a git repo. The current mmj2 default settings make it difficult to use a set.mm git repo separately from the metamath executable, because it encourages combining the metamath program and the Metamath database into one directory. > 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. This is a big difference between GUIs and CLIs. While the current directory *exists* in GUIs, users don't normally set it. Instead, users select specific files to work on, and then the program to use on that file. That file has a directory of course. Metamath.exe works well in this role, but mmj2 doesn't play nicely at all with this. mmj2 is a GUI that takes a very nonstandard set of CLI parameters. > In case you are interested, here is how official Debian packages I am > responsible for work; package "metamath" contains these files: (A nice, conventional organization for a package.) > As you can see, no databases here. Good! The mmj2 program is actually the weirder program here. Its installation & command line is very different from most programs. My plan is to provide, soon, simplified install instructions for the *current* mmj2 program as it exists. I then hope to think about ways to make mmj2 easier to use in typical circumstances. The key is that we should try to make it easy for new users to join the fun. --- 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/E1jWpED-0007u7-1u%40rmmprod06.runbox.
