Re: [Metamath] Proposed installation conventions so things will be easier to install (FL)
> 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 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 metamath+unsubscr...@googlegroups.com. To view this discussion on the web visit https://groups.google.com/d/msgid/metamath/E1jWpED-0007u7-1u%40rmmprod06.runbox.
Re: [Metamath] Proposed installation conventions so things will be easier to install
On Thu, May 7, 2020 at 12:19 PM Giovanni Mascellani wrote: > > Il 06/05/20 18:40, David A. Wheeler ha scritto: > > So "\Documents and Settings" was sort-of like /home. > > This was HIDEOUS for programs and users, because > > "Documents and Settings" is absurdly long AND has spaces in it, > > which is pain for Windows shell similar to the pain of Unix shell. > > Not to mention the fact that "Documents and Settings" was localized in > non-English installations of Windows (just like "Program Files"); and of > course there was plenty of software unaware of that, so that you had > programs trying to access your files in the wrong position, or > installing programs in the wrong position. I understand that was part of the point, to make programs that didn't check the appropriate settings break early and often, so if a program couldn't handle custom document folders with spaces and odd characters in them, the program would clearly be wrong, not the user. Shell is frequently a security disaster, since real files have spaces, quotes and other characters in them, and most Unixes permit anything but / and \0, so if shell can't handle that, you shouldn't use shell. -- The standard is written in English . If you have trouble understanding a particular section, read it again and again and again . . . Sit up straight. Eat your vegetables. Do not mumble. -- _Pascal_, ISO 7185 (1991) -- 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 metamath+unsubscr...@googlegroups.com. To view this discussion on the web visit https://groups.google.com/d/msgid/metamath/CAMZ%3Dzj6cqGF5A0chx2nn9FQvo5Ryr0LCeEF8bQxjgZgjXkgkUw%40mail.gmail.com.
Re: [Metamath] Proposed installation conventions so things will be easier to install
Il 06/05/20 18:40, David A. Wheeler ha scritto: > So "\Documents and Settings" was sort-of like /home. > This was HIDEOUS for programs and users, because > "Documents and Settings" is absurdly long AND has spaces in it, > which is pain for Windows shell similar to the pain of Unix shell. Not to mention the fact that "Documents and Settings" was localized in non-English installations of Windows (just like "Program Files"); and of course there was plenty of software unaware of that, so that you had programs trying to access your files in the wrong position, or installing programs in the wrong position. Giovanni. -- Giovanni Mascellani 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 metamath+unsubscr...@googlegroups.com. To view this discussion on the web visit https://groups.google.com/d/msgid/metamath/d6f3f70f-619f-3978-49d9-04cc8c5e47e4%40gmail.com. signature.asc Description: OpenPGP digital signature
Re: [Metamath] Proposed installation conventions so things will be easier to install (FL)
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 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 metamath+unsubscr...@googlegroups.com. 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
Re: [Metamath] Proposed installation conventions so things will be easier to install (FL)
Forwarded Message Subject: Git Date: Thu, 7 May 2020 11:45:59 +0200 (CEST) From: fl To: Megill Norman Hi Norm, Can you post this: providing only communication through git is not a good Idea. Git should be reserved forp who wants to modify the programs (Metamath or mmj2). 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. And the end user doesn't want to have his/her working directory polluated with git stuff. -- FL -- 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 metamath+unsubscr...@googlegroups.com. To view this discussion on the web visit https://groups.google.com/d/msgid/metamath/cb4dfbcb-e51b-4ffc-9503-52cf9c743937%40googlegroups.com.
Re: [Metamath] Proposed installation conventions so things will be easier to install
On Tuesday, May 5, 2020 at 12:00:28 AM UTC-4, David A. Wheeler wrote: > > > We could continue to post Metamath-exe with a precompiled binary > and have people store it in C:\metamath. That's not how software > is usually installed on Windows, and it's clunky, but it *works*. There are many Windows programs, especially small utilities, that consist of the .exe file only. For example, one that I use frequently for temperature and other system monitoring is called speccy.exe, and it runs as a standalone program. It doesn't matter what directory you put the file in - you double-click on it, and it runs. It does not mess with the registry or require an installer/uninstaller or put tons of files scattered throughout the system or anything else. To uninstall it, you just delete it. (OK, if you change a configuration setting from inside the program, it does create a file called speccy.ini in the same directory as the program, but that's the only thing it touches on your system.) I can put it on a thumb drive and use it immediately on a different computer with no installation, running it directly from the thumb drive. Simple and beautiful. I like programs like that. As for metamath.exe, no one has ever complained that its "installation" on Windows is clunky or awkward, nor has anyone asked for a Windows setup.exe type installer and uninstaller. It is no different from speccy.exe in that regard. The directory C:\metamath is just a suggestion; it can go anywhere. I can put the two files metamath.exe and set.mm on a thumb drive, and I'm ready to start using the program immediately on any Windows computer. So I'm wondering if creating an installer package for metamath.exe on Windows is something there is an actual demand for. If not, it seems like a lot of work with little benefit, in addition to future work of keeping it all maintained. mmj2 may be a different story, since its installation is less trivial, and it might benefit from being released for Windows as a setup.exe file. Norm -- 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 metamath+unsubscr...@googlegroups.com. To view this discussion on the web visit https://groups.google.com/d/msgid/metamath/6c9f9626-d9ca-4e26-9e2c-28affa14071c%40googlegroups.com.
Re: [Metamath] Proposed installation conventions so things will be easier to install
On Wed, 6 May 2020 00:45:22 -0700 (PDT), "'B. Wilson' via Metamath" wrote: > There also seems to be some tension about installation expectations. Some > people like the fact that metamath Just Works by downloading and extracting > an archive to wherever. Others, like myself, seem to prefer that metamath > Just Works by installing it like any other program on your platform. > > Upstream build and distribution burden notwithstanding, it seems like both > of these installation methods are mutually compatible. Agreed. It shouldn't be any harder than it is currently to download a zipfile/tarball, do compiling/configuration, and run. Ideally easier. But it's very rare for people to install software that way any more. Software is usually installed today as packages unless you plan to modify the program. I think you have a good point that we should be following *current* packaging standards. We'd have to do some more work on the software to truly follow them, but it would make it easier for new users. It might be best to think about what it would look like in the end. Users could simply use their browser, click on "install Metamath-exe" and "install mmj2", and the respective software would be fully installed. They can separately download a database, e.g., "set.mm". They can then use their list of applications (e.g., "Start" Menu) to run the program, which would be able to easily load whatever database they'd like. Here are the kind of changes needed for that: * Metamath-exe: Its autoconfig files already meet the requirements for POSIX; we just need to document how to install it with them. We'd also need to add a .desktop file for POSIX, but that's trivial. Ideally someone would directly create packages for systems like Debian, Ubuntu, Fedora, and then either get the packages into their repos *OR* create a Metamath repo. Metamath doesn't provide a Windows installer; it might not be too hard to use NSIS to create a .msi installer. * mmj2: It doesn't currently meet POSIX install standards. I can autoconfiscate it to do that. It needs a .desktop file (easy).Its instructions need an update. Packaging it for Windows might be trickier, but as long as we require installing Java *separately* it wouldn't be too bad. --- 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 metamath+unsubscr...@googlegroups.com. To view this discussion on the web visit https://groups.google.com/d/msgid/metamath/E1jWNX2-00014v-Uh%40rmmprod06.runbox.
Re: [Metamath] Proposed installation conventions so things will be easier to install
On Wed, 6 May 2020 00:45:22 -0700 (PDT), "'B. Wilson' via Metamath" wrote: > Would it make sense to have "search path" variables for metamath and mmj2? It could. All Metamath tools (at least Metamath & mmj2) would have to be modified to support it, and that's a minor pain. But once done things would "just work" even when people make a few different decisions, and that's an advantage. Here's a try: "METAMATHDB_PATH", if present, is a list of directories to be searched when a Metamath database is to be loaded and the database name does not include a directory separator. This modified name is from then on considered its name (e.g., if it is saved, then it saved to that location unless a different location is specified). The list uses the OS's standard format (; separated for Windows, : for everything else). On POSIX systems, the default value of METAMATHDB_PATH is: .:$HOME/set.mm:$HOME/metamath:/usr/var/metamath On Windows systems, the default value of METAMATHDB_PATH is: .;%USERPROFILE%\set.mm;%USERPROFILE%\metamath;%HOMEDRIVE%\set.mm;%HOMEDRIVE%\metamath;%SystemDrive%\Users\Public\metamath I'm not sure what a reasonable "global" value on Windows would be, so I used \Users\Public\metamath Note that in Windows, both "/" and "\" are directory separators. --- 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 metamath+unsubscr...@googlegroups.com. To view this discussion on the web visit https://groups.google.com/d/msgid/metamath/E1jWNL0-0008Uy-Fe%40rmmprod06.runbox.
Re: [Metamath] Proposed installation conventions so things will be easier to install
> My eyes are certainly Linux-tinted, but is there some sort of analogue to
> the above for Windows?
Sort of. Please sit back, the story is long, below.
I've lived through all this history: I've used Unix & Linux of many flavors,
and I've also used CP/M & MS-DOS 1.0 on & Windows on.
--- David A. Wheeler
===
Windows does have environment variables, the PATH environment variable,
and a notion equivalent to Linux's "home directory".
You can see various environment variable values here:
https://en.wikipedia.org/wiki/Environment_variable#Default_values
https://docs.microsoft.com/en-us/windows/win32/shell/knownfolderid?redirectedfrom=MSDN
Let's assume we can ignore Windows XP, and focus on Vista & later.
In that case, the environment variable USERPROFILE is more-or-less
the same as Unix HOME.
(Beware: HOMEPATH isn't quite the same, because it omits the HOMEDRIVE,
and if the home directory is remote there *is* no HOMEDRIVE).
You can see this joyousness here:
https://github.com/mitchellh/go-homedir/issues/23
So in Windows command shell you can refer to USERPATH as %USERPATH%
(just like $HOME is Unix/Linux shell).
HOWEVER, there's also history to be considered, especially
CP/M -> Quick-n-Dirty DOS -> MS-DOS -> Windows.
MS-DOS 1.0 didn't have directories, just drive letters,
so people *had* to store things in the "root" of the drive.
MS-DOS 2.0 added directories, and later Windows added home directories.
However, Windows, up through and including Windows XP, had the
equivalent of home directories in:
\Documents and Settings\{username}
So "\Documents and Settings" was sort-of like /home.
This was HIDEOUS for programs and users, because
"Documents and Settings" is absurdly long AND has spaces in it,
which is pain for Windows shell similar to the pain of Unix shell.
So people often continued to store directories (at least) at the top,
e.g, C:\metamath.
More recent Windows now uses "\Users\{username}" instead of
"\Documents and Settings\{username}" but the damage is done;
many users don't use their home directory much (!).
There's a general convention in Windows that you'll
install software using an installer that will place executables
so that you don't have to manipulate the PATH.
That's true for other systems too, but creating such installers
is more work on Windows. It's possible, though.
There are other differences, e.g.:
* Windows line ending is conventionally CRLF, vs POSIX's LF
* Windows directory separator is "\". However the file system *DOES* accept "/"
as a directory separator, so you can often use "/" and it just works. One
problem: Command line commands often use "/" as the option prefix (instead of
"-"), but this is inconsistent.
* PATH is ;-separated, not :-separated, but otherwise works the same way.
Windows is really a mess. They've tried to walk back some of the mistakes
(e.g., the new "Users" directory). But screw-ups like drive letters and using
"\" as the directory separator are hard to fully undo.
--
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 metamath+unsubscr...@googlegroups.com.
To view this discussion on the web visit
https://groups.google.com/d/msgid/metamath/E1jWN6D-0007AM-3e%40rmmprod06.runbox.
Re: [Metamath] Proposed installation conventions so things will be easier to install
On Wed, 6 May 2020 00:45:22 -0700 (PDT), "'B. Wilson' via Metamath" 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 metamath+unsubscr...@googlegroups.com. To view this discussion on the web visit https://groups.google.com/d/msgid/metamath/E1jWMrC-0005vQ-OV%40rmmprod06.runbox.
Re: [Metamath] Proposed installation conventions so things will be easier to install
Here are some brainstorming questions and thoughts: 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. What about mmj2? I haven't tried out mmj2 yet, but would the above apply there too? My eyes are certainly Linux-tinted, but is there some sort of analogue to the above for Windows? There also seems to be some tension about installation expectations. Some people like the fact that metamath Just Works by downloading and extracting an archive to wherever. Others, like myself, seem to prefer that metamath Just Works by installing it like any other program on your platform. Upstream build and distribution burden notwithstanding, it seems like both of these installation methods are mutually compatible. 2020年5月6日水曜日 5時25分48秒 UTC+9 Norman Megill: > > Forwarded Message > Subject: Current problem > Date: Tue, 5 May 2020 20:19:24 +0200 (CEST) > From: fl > To: Megill Norman > > Hi Norm, > > Can you post this. > > I don't know how you do, but my own version of mmj2 has no problems to > find set.mm in the current directory. > > -- > FL > > On Tuesday, May 5, 2020 at 10:44:18 AM UTC-4, David A. Wheeler wrote: >> >> FL: >> > For me it's not "/usr/bin" it's "/usr/local/bin" >> >> That's true for many people. Metamath-exe actually already supports this, >> just use "make install" with autoconf (as always that's the default). >> If you want /usr/bin (as is common for packages installed with a >> package manager), use "PREFIX=/usr/bin make install" >> >> ... >> >> > and set.mm is not a library it's a file of data. >> > You have to be able to browse it and modify it with an editor. >> >> Agreed. >> >> > And the applications must look for it in the current directory "." not >> in $HOME. >> >> The bigger problem is mmj2. >> GUIs don't really have the concept of "current directory", and mmj2 >> needs to know where its current database is. >> >> --- 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 metamath+unsubscr...@googlegroups.com. To view this discussion on the web visit https://groups.google.com/d/msgid/metamath/1f36efa8-a57f-4186-ab97-176fa92b31a5%40googlegroups.com.
Re: [Metamath] Proposed installation conventions so things will be easier to install
Forwarded Message Subject: Current problem Date: Tue, 5 May 2020 20:19:24 +0200 (CEST) From: fl To: Megill Norman Hi Norm, Can you post this. I don't know how you do, but my own version of mmj2 has no problems to find set.mm in the current directory. -- FL On Tuesday, May 5, 2020 at 10:44:18 AM UTC-4, David A. Wheeler wrote: > > FL: > > For me it's not "/usr/bin" it's "/usr/local/bin" > > That's true for many people. Metamath-exe actually already supports this, > just use "make install" with autoconf (as always that's the default). > If you want /usr/bin (as is common for packages installed with a > package manager), use "PREFIX=/usr/bin make install" > > ... > > > and set.mm is not a library it's a file of data. > > You have to be able to browse it and modify it with an editor. > > Agreed. > > > And the applications must look for it in the current directory "." not > in $HOME. > > The bigger problem is mmj2. > GUIs don't really have the concept of "current directory", and mmj2 > needs to know where its current database is. > > --- 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 metamath+unsubscr...@googlegroups.com. To view this discussion on the web visit https://groups.google.com/d/msgid/metamath/7f91a511-acb0-4cac-952a-9d11a31df858%40googlegroups.com.
Re: [Metamath] Proposed installation conventions so things will be easier to install
On Tue, 5 May 2020 08:00:35 -0700, David Starner wrote: > It'd be a lot easier to handle set.mm if it were more standard to have > set.mm as a constant and editing being done to separate .mm files. I don't think so. Which version of set.mm would be constant? --- 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 metamath+unsubscr...@googlegroups.com. To view this discussion on the web visit https://groups.google.com/d/msgid/metamath/E1jW122-0005F4-Og%40rmmprod06.runbox.
Re: [Metamath] Proposed installation conventions so things will be easier to install
It'd be a lot easier to handle set.mm if it were more standard to have set.mm as a constant and editing being done to separate .mm files. -- The standard is written in English . If you have trouble understanding a particular section, read it again and again and again . . . Sit up straight. Eat your vegetables. Do not mumble. -- _Pascal_, ISO 7185 (1991) -- 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 metamath+unsubscr...@googlegroups.com. To view this discussion on the web visit https://groups.google.com/d/msgid/metamath/CAMZ%3Dzj6B-apMopvq3pGcFKJozb4eCpYrrw5WHDYVXttv0T-5Vg%40mail.gmail.com.
Re: [Metamath] Proposed installation conventions so things will be easier to install
FL: > For me it's not "/usr/bin" it's "/usr/local/bin" That's true for many people. Metamath-exe actually already supports this, just use "make install" with autoconf (as always that's the default). If you want /usr/bin (as is common for packages installed with a package manager), use "PREFIX=/usr/bin make install" ... > and set.mm is not a library it's a file of data. > You have to be able to browse it and modify it with an editor. Agreed. > And the applications must look for it in the current directory "." not in > $HOME. The bigger problem is mmj2. GUIs don't really have the concept of "current directory", and mmj2 needs to know where its current database is. --- 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 metamath+unsubscr...@googlegroups.com. To view this discussion on the web visit https://groups.google.com/d/msgid/metamath/E1jVynv-0003up-Hy%40rmmprod06.runbox.
Re: [Metamath] Proposed installation conventions so things will be easier to install
Forwarded Message Subject: Directories Date: Tue, 5 May 2020 11:36:00 +0200 (CEST) From: fl To: Megill Norman Hi Norm, Can you post this. For me it's not "/usr/bin" it's "/usr/local/bin" and set.mm is not a library it's a file of data. You have to be able to browse it and modify it with an editor. And the applications must look for it in the current directory "." not in $HOME. -- FL -- 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 metamath+unsubscr...@googlegroups.com. To view this discussion on the web visit https://groups.google.com/d/msgid/metamath/1eeb2a86-46f5-464c-a7fe-2fcddff2213a%40googlegroups.com.
Re: [Metamath] Proposed installation conventions so things will be easier to install
On Mon, 4 May 2020 18:41:16 -0700 (PDT), "'B. Wilson' via Metamath" wrote: ... Your post does *not* discuss what to do with Windows. We need to decide how to help people install Metamath on Windows, since that's a common platform. We could continue to post Metamath-exe with a precompiled binary and have people store it in C:\metamath. That's not how software is usually installed on Windows, and it's clunky, but it *works*. Proper installation really requires at least manipulating the PATH. If we wanted something better for Windows, then providing an installable package seems like the right way to go. There seem to multiple approaches: * Microsoft pitches its "store" today, so you create an "App Package Upload File (.msixupload or .appxupload). That seems to require paying $$$ for certificates and such (did I misread something?) * An alternative is to create an App Bundle (.msixbundle or .appxbundle) installation file. That seems to require the use of Visual Studio. But again, it seems to require getting a certificate, and it looks like that costs $$$ and we're not a company. https://docs.microsoft.com/en-us/windows/msix/package/packaging-uwp-apps * An old-school approach would be to create an .msi file. Working out the process for doing that would be a pain, but the WiX toolset will create .msi files that can "just be installed": https://wixtoolset.org/ A competitor to WiX is NSIS: https://nsis.sourceforge.io/Main_Page It might be useful to use Visual Studio to compile Metamath for Windows; it looks like it can be freely used for OSS development: https://visualstudio.microsoft.com Comments welcome! --- 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 metamath+unsubscr...@googlegroups.com. To view this discussion on the web visit https://groups.google.com/d/msgid/metamath/E1jVoks-00045p-H0%40rmmprod06.runbox.
Re: [Metamath] Proposed installation conventions so things will be easier to install
On Mon, 4 May 2020 18:41:16 -0700 (PDT), "'B. Wilson' via Metamath" 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 metamath+unsubscr...@googlegroups.com. To view this discussion on the web visit https://groups.google.com/d/msgid/metamath/E1jVoGn-fx-0g%40rmmprod06.runbox.
Re: [Metamath] Proposed installation conventions so things will be easier to install
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. Programs which do this are not common, play badly with
packaging tools, and are generally considered bad citizens from a system
administrator perspective. Instead, how about following the Filesystem
Hierarchy Standard, instead?
http://www.pathname.com/fhs/pub/fhs-2.3.html
Something like the following conventions would make metamath play along
well with the rest of the system:
/usr/bin for metamath-exe, mmj2 etc.
/var/lib/metamath for set.mm and any other databases
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. Metamath-exe, as an autotools build automatically
supports this. This would make a *local* installation look like
$HOME/.local/usr/bin contains metamath-exe, mmj2 etc.
$HOME/.local/var/lib/metamath contains set.mm etc.
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, which means that it
has a better chance of working in home directories that have locked-down
executable permissions.
Locally, I have a wrapper script around metamath that follows the above,
letting one easily list, read, and update databases. For reference, I will
attach it.
The above is just a rough sketch of my ideas, so if anything is unclear,
please poke and prod with abandon. Looking forward to where this discussion
goes!
Cheers,
2020年5月4日月曜日 2時16分07秒 UTC+9 David A. Wheeler:
>
> I want to clarify a key point in my earlier post,
> "[Metamath] Proposed installation conventions so things will be easier to
> install".
>
> To make it easier to install mmj2 and other tools, I want to change the
> conventions
> so that "set.mm" is by default stored in its *own* directory
> (I recommend ~/set.mm for non-Windows, C:\set.mm for Windows).
> Separating code from data, when they're not updated at the same time,
> makes
> updates & many other operations much simpler.
>
> If you really want to, you can continue to do things the old way. I just
> want to change
> the instructions & scripts so this is the *default*.
>
> --- 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 metamath+unsubscr...@googlegroups.com.
To view this discussion on the web visit
https://groups.google.com/d/msgid/metamath/53534b3c-caa7-4512-b95f-390bcf825832%40googlegroups.com.
#!/usr/bin/env sh
METAMATH_DIR=${METAMATH_DIR-${HOME}/.local/var/lib/metamath}
METAMATH_GIT=${METAMATH_GIT-https://github.com/metamath/set.mm}
METAMATH_RC=${METAMATH_RC-${HOME}/.metamathrc}
command -v rlwrap >/dev/null && rlwrap=enabled
command -v tput >/dev/null && tput=enabled
show_usage() {
>&2 cat <<-USAGE
Usage: mm [-hlu] [-d ] [-g ] [-r ] [-s ]
Wrapper around the metamath executable, setting up the metamath
environment for easy use. The following options also provide convenient
management of metamath databases.
OPTIONS
-h Display this help message
-l List available databases
-u Update databases from METAMATH_GIT into METAMATH_DIR
-d Path directory containing metamath databases
-g URL of remote git repo from which to update databases
-r Read into metamath on startup
-s Submit commands in to metamath on startup
-R Disable readline support with rlwrap
-T Disable automatic height and width setting from tput
ENVIRONMENT VARIABLES
METAMATH_DIR=${METAMATH_DIR}
Path of directory containing metamath databases
METAMATH_GIT=${METAMATH_GIT}
URL from which to update the databases git repository
METAMATH_RC=${METAMATH_RC}
Path to file containing metamath commands
USAGE
}
error() {
errno=${1}
msg=${2}
>&2 echo "${msg}"
show_usage
exit "${errno}"
}
mm_update() {
url=${1}
dir=${2}
command -v git >/dev/null || return 1
[ -d "${dir}" ] || mkdir -vp "${dir}"
if [ -d "${dir}/.git" ]; then
git -C "${dir}" pull
else
git clone "${url}" "${dir}"
fi
}
mmdir=${METAMATH_DIR}
mmgit=${METAMATH_GIT}
[ -r "${METAMATH_RC}" ] && mmrc=${METAMATH_RC}
while getopts ':hluRTd:g:r:s:' opt "${@}"; do
case "${opt}" in
h) show_usage; exit 0;;
l) find "$
Re: [Metamath] Proposed installation conventions so things will be easier to install
On Mon, 4 May 2020 08:32:59 -0700 (PDT), Norman Megill wrote: > While I'm not sure of the best way to go forward, let me explain why set.mm > and the metamath program are currently in the same directory. ... > Putting both into one directory allows an unsophisticated Windows user to > click on metamath.exe and type "read set.mm". This goes back to the days > before the Metamath site existed, when the only access to set.mm was via > the program, so it was important to make getting started as simple and > quick as possible for such users. I think this makes historical sense, but now that set.mm and metamath-exe are being routinely updated on GitHub I think that structure has outlived its usefulness. The *easiest* way to keep up-to-date with set.mm is to pull from GitHub, which means that set.mm should be in its own directory. If set.mm & metamath-exe are in the same directory, it's easy to stomp on each other, potentially losing work in progress. If someone really wants put them in one directory, that's fine, but that shouldn't be the default install; that's something you should configure yourself because you want to do that & you know what you're doing. There are many ways to deal with paths. It's not *that* complex, and there are only really two cases: POSIX (the standard) and "Windows". All the POSIX systems basically work the same way (Linux, Unix, MacOS, cygwin). I think it's better to update the instructions so that people deal with paths (or whatever) only during install, and then everything 'just works". There are many ways to do this, but trying to merge data into a single directory, when they're updated at different times, is becoming an obstacle. Package managers can do that just fine, but we don't need to write a package manager just for Metamath :-). --- 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 metamath+unsubscr...@googlegroups.com. To view this discussion on the web visit https://groups.google.com/d/msgid/metamath/E1jVdvr-0007Ri-FN%40rmmprod06.runbox.
Re: [Metamath] Proposed installation conventions so things will be easier to install
While I'm not sure of the best way to go forward, let me explain why set.mm and the metamath program are currently in the same directory. A significant number of people are completely unfamiliar with command line interfaces on Windows and don't know how to specify directory paths. Even worse, there are multiple ways to specify directory paths depending on the platform, the compiler, and (on Windows) whether or not you are using Cygwin. While the program directory can be added to the Windows "Path", it involves going into advanced system settings to alter the Path environmental variable (an awkward and dangerous edit with the crude editing facility provided). Putting both into one directory allows an unsophisticated Windows user to click on metamath.exe and type "read set.mm". This goes back to the days before the Metamath site existed, when the only access to set.mm was via the program, so it was important to make getting started as simple and quick as possible for such users. Norm On Sunday, May 3, 2020 at 1:16:07 PM UTC-4, David A. Wheeler wrote: > > I want to clarify a key point in my earlier post, > "[Metamath] Proposed installation conventions so things will be easier to > install". > > To make it easier to install mmj2 and other tools, I want to change the > conventions > so that "set.mm" is by default stored in its *own* directory > (I recommend ~/set.mm for non-Windows, C:\set.mm for Windows). > Separating code from data, when they're not updated at the same time, > makes > updates & many other operations much simpler. > > If you really want to, you can continue to do things the old way. I just > want to change > the instructions & scripts so this is the *default*. > > --- 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 metamath+unsubscr...@googlegroups.com. To view this discussion on the web visit https://groups.google.com/d/msgid/metamath/f8d3d98a-a7f2-4a28-b186-2114be645aa9%40googlegroups.com.
Re: [Metamath] Proposed installation conventions so things will be easier to install
This looks reasonable. I'm not completely sure I follow which pieces are
recommendations which people can follow or not, and which pieces are
default places for scripts to look (which people can also not follow,
since there will be ways to override defaults). But I'm sure this will
be clear as this is turned into pull requests. And the particular
defaults suggested below seem as good as any.
Generally the idea that you can install metamath, set.mm, and mmj2, and
there are default or suggested ways for them to find each other, makes
sense to me. Even for me, who is capable of messing around with a PATH
and editing a config file, found it to be a bit of a speed bump in
getting started. So anything we can do to make this easier is great.
On 5/2/20 3:43 PM, David A. Wheeler wrote:
We need to make it easier for new Metamath users to join the fun.
Typical Metamath users have multiple things installed. I think they should be able to
install things wherever they want, *but* we should have some conventions so that things
"just work" on a simple install by default.
Here are some thoughts about how to do this; comments welcome.
--- David A. Wheeler
First, overall:
1. People should be able to put things wherever they want; the point here is to
just set some *defaults* in config files etc. so that if you don't care, things
will automatically work together.
2. We should try to follow the local system conventions, supporting at least
Windows (including with and without Cygwin), Linux (Ubuntu/Debian/Fedora at
least), and MacOS.
3. Precompiled packages should be available, especially on systems where
compilers are harder to set up (Windows), but it should be relatively easy to
set up things with source code.
4. Different components must start in different directories, so that you can upgrade one
without stomping on another. In particular, the current "set.mm" should be in a
directory *separate* from metamath-exe and mmj2.
5. I'm focusing on the set.mm database, metamath-exe, and mmj2 for starters, but
there are other Metamath tools & I'm sure their users would like things to be
simpler too!
So let me start with a proposal for Linux systems, using its conventions ("~"
is the user home directory):
* Install set.mm in "~/set.mm". This is already what happens if you are in your home
directory and do the usual git install command from GitHub: "git install
https://github.com/metamath/set.mm.git";.
* Install the metamath-exe (C) source code in "~/metamath". This is already what
happens if you are in your home directory and follow the metamath-exe instructions at
http://us.metamath.org/#downloads . You can compile it & leave its executable there. You
can do a local user install to your home directory $HOME (e.g., $HOME/bin/metamath), a local
system install to the usual directory /usr/local/ (e.g., /usr/local/bin/metamath), or a
*system package* for metamath, to the usual directory /usr (e.g., /usr/bin/metamath for the
exectuable) - the autoconf file in Metamath already supports all of that as usual.
* Install mmj2 source code in "~/mmj2". It should also be installable with all
the usual conventions.
Programs can increase the likelihood of finding a working metamath-exe executable by
doing PATH="$PATH:$HOME/metamath" and then calling metamath. That way, if the
metamath executable wanted by the user is on the PATH, that will be used... but if one
isn't in the PATH, then ~/metamath is checked out automatically.
On Windows the convention seems to be to install metamath-exe into "c:\metamath". That's unusual, and I worry
that some systems that forbid that (since it's outside the user home directory). But if that is to continue, then I'd
suggest "c:\set.mm" for the set.mm database (as copied from git) and "c:\mmj2" for mmj2's source
distribution. A similar trick applies for programs trying run metamath; set PATH="%PATH%;c:\metamath" and
then give it a try. If people want to use the home directory as the default instead, that's great. Many Windows users
depend on a package installer, but that's a more work to set up.
MacOS: Not sure what to say here. It might not be hard to set up something with
brew, at least for metamath-exe.
--
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 metamath+unsubscr...@googlegroups.com.
To view this discussion on the web visit
https://groups.google.com/d/msgid/metamath/542220e9-2c4e-1565-87c4-172aba9f2dc7%40panix.com.
Re: [Metamath] Proposed installation conventions so things will be easier to install
I want to clarify a key point in my earlier post, "[Metamath] Proposed installation conventions so things will be easier to install". To make it easier to install mmj2 and other tools, I want to change the conventions so that "set.mm" is by default stored in its *own* directory (I recommend ~/set.mm for non-Windows, C:\set.mm for Windows). Separating code from data, when they're not updated at the same time, makes updates & many other operations much simpler. If you really want to, you can continue to do things the old way. I just want to change the instructions & scripts so this is the *default*. --- 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 metamath+unsubscr...@googlegroups.com. To view this discussion on the web visit https://groups.google.com/d/msgid/metamath/E1jVIDl-0007Un-Pi%40rmmprod06.runbox.
[Metamath] Proposed installation conventions so things will be easier to install
We need to make it easier for new Metamath users to join the fun.
Typical Metamath users have multiple things installed. I think they should be
able to install things wherever they want, *but* we should have some
conventions so that things "just work" on a simple install by default.
Here are some thoughts about how to do this; comments welcome.
--- David A. Wheeler
First, overall:
1. People should be able to put things wherever they want; the point here is to
just set some *defaults* in config files etc. so that if you don't care, things
will automatically work together.
2. We should try to follow the local system conventions, supporting at least
Windows (including with and without Cygwin), Linux (Ubuntu/Debian/Fedora at
least), and MacOS.
3. Precompiled packages should be available, especially on systems where
compilers are harder to set up (Windows), but it should be relatively easy to
set up things with source code.
4. Different components must start in different directories, so that you can
upgrade one without stomping on another. In particular, the current "set.mm"
should be in a directory *separate* from metamath-exe and mmj2.
5. I'm focusing on the set.mm database, metamath-exe, and mmj2 for starters,
but there are other Metamath tools & I'm sure their users would like things to
be simpler too!
So let me start with a proposal for Linux systems, using its conventions ("~"
is the user home directory):
* Install set.mm in "~/set.mm". This is already what happens if you are in your
home directory and do the usual git install command from GitHub: "git install
https://github.com/metamath/set.mm.git";.
* Install the metamath-exe (C) source code in "~/metamath". This is already
what happens if you are in your home directory and follow the metamath-exe
instructions at http://us.metamath.org/#downloads . You can compile it & leave
its executable there. You can do a local user install to your home directory
$HOME (e.g., $HOME/bin/metamath), a local system install to the usual directory
/usr/local/ (e.g., /usr/local/bin/metamath), or a *system package* for
metamath, to the usual directory /usr (e.g., /usr/bin/metamath for the
exectuable) - the autoconf file in Metamath already supports all of that as
usual.
* Install mmj2 source code in "~/mmj2". It should also be installable with all
the usual conventions.
Programs can increase the likelihood of finding a working metamath-exe
executable by doing PATH="$PATH:$HOME/metamath" and then calling metamath. That
way, if the metamath executable wanted by the user is on the PATH, that will be
used... but if one isn't in the PATH, then ~/metamath is checked out
automatically.
On Windows the convention seems to be to install metamath-exe into
"c:\metamath". That's unusual, and I worry that some systems that forbid that
(since it's outside the user home directory). But if that is to continue, then
I'd suggest "c:\set.mm" for the set.mm database (as copied from git) and
"c:\mmj2" for mmj2's source distribution. A similar trick applies for programs
trying run metamath; set PATH="%PATH%;c:\metamath" and then give it a try. If
people want to use the home directory as the default instead, that's great.
Many Windows users depend on a package installer, but that's a more work to set
up.
MacOS: Not sure what to say here. It might not be hard to set up something with
brew, at least for metamath-exe.
--
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 metamath+unsubscr...@googlegroups.com.
To view this discussion on the web visit
https://groups.google.com/d/msgid/metamath/E1jV0rF-0006nT-CW%40rmmprod06.runbox.
