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 <path>] [-g <repo>] [-r <database>] [-s <rcfile>]
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> Path directory containing metamath databases
-g <repo> URL of remote git repo from which to update databases
-r <database> Read <database> into metamath on startup
-s <rcfile> Submit commands in <rcfile> 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 "${mmdir}" -name '*.mm' -printf '%P\n'; exit;;
u) mm_update "${mmgit}" "${mmdir}"; exit $?;;
d) mmdir=${OPTARG};;
g) mmgit=${OPTARG};;
r) mmdb=${OPTARG};;
s) mmrc=${OPTARG};;
R) unset tput;;
T) unset rlwrap;;
:) error 1 "Expected argument: -${OPTARG}";;
*) error 1 "Unknown argument: -${OPTARG}";;
esac
done
shift $((OPTIND - 1))
if [ -n "${tput+x}" ]; then
width=$(tput cols)
height=$(tput lines)
fi
exec ${rlwrap+rlwrap --complete-filenames} \
metamath ${width+"set width ${width}"} \
${height+"set height $((height - 1))"} \
${mmrc+"submit '${mmrc}'"} \
${mmdb+"read '${mmdir}/${mmdb}'"} \
"${@}"
