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 [email protected].
To view this discussion on the web visit
https://groups.google.com/d/msgid/metamath/E1jV0rF-0006nT-CW%40rmmprod06.runbox.
