Proposed installation conventions so things will be easier to install

[David A. Wheeler]

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.

[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

[Jim Kingdon]

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.

[Norman Megill]

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

[David A. Wheeler]

On Mon, 4 May 2020 08:32:59 -0700 (PDT), Norman Megill <n...@alum.mit.edu> 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

[B. Wilson]

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:

[David A. Wheeler]

On Mon, 4 May 2020 18:41:16 -0700 (PDT), "'B. Wilson' via Metamath" <meta...@googlegroups.com> 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

[David A. Wheeler]

On Mon, 4 May 2020 18:41:16 -0700 (PDT), "'B. Wilson' via Metamath" <meta...@googlegroups.com> 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

[savask]

I just wanted to make a small comment, based on personal experience.

Back when I first tried metamath, I found it very convenient that it was shipped as a standalone executable. I don't really like programs which "clutter" the home directory or make some unasked changes to the file system (especially to "invisible" directories like .config), since these things tend to accumulate over time. In my opinion, one of the strongest sides of metamath is that it's very easy to set up and play with, essentially you just need to download one tarball and run the executable - all main databases are already at your disposal. It is as easy to remove without any traces being left, which is a plus side in my opinion (unless you want to make people stick to metamath no matter what, I guess :-) ). There's also a growing tendency to ship programs as standalone packages (like appimage), but I guess metamath tarball is already more or less a standalone package.

Same goes for set.mm and other databases - these are just input for metamath and mmj2, so I don't think there should be a standard place for these (I don't think there is a standard directory for .tex or .doc files). As for the hypothetical event of losing your set.mm progress by installing a new metamath version over it - that could be easily fixed by adding date to the set.mm filename used in metamath.tar.gz, as in set_05.05.20.mm. Personally, I have various versions of set.mm scattered all over the file system (for a good reason), so it would be unfortunate if I had to re-configure metamath to support that.

[Norman Megill]

-------- 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

[David A. Wheeler]

On Mon, 4 May 2020 23:58:46 -0700 (PDT), savask <sav...@yandex.ru> wrote:
> I just wanted to make a small comment, based on personal experience.
>
> Back when I first tried metamath, I found it very convenient that it was
> shipped as a standalone executable. I don't really like programs which
> "clutter" the home directory or make some unasked changes to the file
> system (especially to "invisible" directories like .config), since these
> things tend to accumulate over time.

We *definitely* don't want *unasked* changes no matter what.
We should support those who want to just put everything in one directory
and control it, just like now. I think that would be easy.

But that isn't how most people expect software to work today.
Typically software is installed in a "standard place".
In Linux/Unix those are /usr/bin, /usr/local/bin, ~/bin, or ~/.local/bin.
On Windows those are "C:\Program Files". You run an installer or
select a package, and you're done.

As far as "accumulate over time", that's a fair concern. The best solution
might be, as B. Wilson suggests, to use the standard packaging conventions.
Every modern system has a package manager that makes it easy to
install AND REMOVE software so that it won't "accumulate over time'.

> one of the strongest
> sides of metamath is that it's very easy to set up and play with,
> essentially you just need to download one tarball and run the executable -

The goal is to make that even easier.

> Same goes for set.mm and other databases - these are just input for
> metamath and mmj2, so I don't think there should be a standard place for
> these (I don't think there is a standard directory for .tex or .doc files).

There certainly is a standard directory for them.
On Windows it is "%HOME%\My Documents" (shown as "Documents").
On Linux/Unix (GNOME and KDE) it is "$HOME/Documents".
I'm trying to remember the MacOS one, I think it's "$HOME/Documents" there too
(though MacOS uses /users instead of /home for home directories).

You don't have to use the standard directory for documents, and you
shouldn't have to use the standard directory here either.
But most users don't want to *have* to configure the tools; they want
a "reasonable default" and then they can change if they want to.

> As for the hypothetical event of losing your set.mm progress by installing
> a new metamath version over it - that could be easily fixed by adding date
> to the set.mm filename used in metamath.tar.gz, as in set_05.05.20.mm.

Yuk. I don't want to become a version control program.
I want the version control program to be the version control program.

If you want to become a version control program, that's up to you :-).
But we should not require people to have to constantly remember to do that.
People are terrible at consistently doing that.

When I start up mmj2, I want it to have a "reasonable default".
If you want something different, excellent... but many people just want
to get the job done. Every choice they *MUST* make is a mistake,
though of course I don't want to *prevent* choices.

> Personally, I have various versions of set.mm scattered all over the file
> system (for a good reason), so it would be unfortunate if I had to
> re-configure metamath to support that.

By definition today you have to do something to tell metamath
where the file is, because there's no default.
The goal isn't to remove that ability; the goal is to create a reasonable
default when you *DON'T* say where it is.

A side annoyance: .mm is already a standard extension (Objective-C).
I don't know if anyone does both Objective-C and Metamath development... :-).

--- David A. Wheeler

[David A. Wheeler]

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

[David Starner]

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)

[David A. Wheeler]

On Tue, 5 May 2020 08:00:35 -0700, David Starner <prosf...@gmail.com> 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

[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

[B. Wilson]

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:

[David A. Wheeler]

On Wed, 6 May 2020 00:45:22 -0700 (PDT), "'B. Wilson' via Metamath" <meta...@googlegroups.com> 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

[David A. Wheeler]

> 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.

[David A. Wheeler]

On Wed, 6 May 2020 00:45:22 -0700 (PDT), "'B. Wilson' via Metamath" <meta...@googlegroups.com> 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

[David A. Wheeler]

On Wed, 6 May 2020 00:45:22 -0700 (PDT), "'B. Wilson' via Metamath" <meta...@googlegroups.com> 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

[Norman Megill]

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

[Norman Megill]

-------- 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

[Giovanni Mascellani]

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 <g.masc...@gmail.com>
Postdoc researcher - Université Libre de Bruxelles

[Giovanni Mascellani]

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.

[David Starner]

On Thu, May 7, 2020 at 12:19 PM Giovanni Mascellani
<g.masc...@gmail.com> 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.

[David A. Wheeler]

> 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 <g.masc...@gmail.com> 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

[Dirk-Anton Broersen]

Here’s my form of trisecrting an angle,

 

Notice the small little circles are related to the bisected circles. I think on surface area. If this is untrue, please let me notice. It seems untrue. If you know that a surface area circle combined to a square differce from thesame circumference length differce from the square. It might makes you doubt. What I’m saying is that the surface area is important to those circles.

 

 

 

With friendly regards,

 

Dirk-Anton Broersen

 

Verzonden vanuit Mail voor Windows 10

 

 

[Jim Kingdon]

I assume this is in reference to item 8 on http://us.metamath.org/mm_100.html . In case the rules of that game aren't clear, https://en.m.wikipedia.org/wiki/Angle_trisection seems to cover it (especially the link to Straightedge and compass construction).

I assume the next step on that one would be formalizing straightedge and compass construction. Is this some subset of the Tarski axioms or is it more complicated than that? Not that I'm likely to change gears from trying to prove that the square root of two is irrational in iset.mm, but I suppose who knows what might eventually catch my fancy?

[Dirk-Anton Broersen]

Yes, what I believe is that the small circles actually have to touch the bi-bisected lines. This is a trisection. But not in 3 thesame angels. The middle angle is a little bigger than the 2 outside. What I asked myself is if the twoo (samesized) circles are (of course according to it's ratio) like double or triple sized. Wich differs in areal size or circumference length. If you compare a circle to a square and you try to square the circle, than the surface area gives a different square than if you square the circumference. 

Square root of 2 is irrational, but it's constructible. I don't know if I get anything you say.

I created the trisection myself.

With friendly regards,

Dirk-Anton Broersen

Verzonden vanuit Outlook Mobile

---

Van: Jim Kingdon <kin...@panix.com>
Verstuurd: zondag 10 mei 2020 22:44
Aan: meta...@googlegroups.com; Dirk-Anton Broersen; meta...@googlegroups.com
Onderwerp: Re: [Metamath] Trisecting an angle