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 [email protected].
To view this discussion on the web visit
https://groups.google.com/d/msgid/metamath/542220e9-2c4e-1565-87c4-172aba9f2dc7%40panix.com.
