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}'"} \ "${@}"