This is something I would just like to share. Please let me know if you find
this helpful.
Attached is a wrapper script around the metamath executable that provides the
following:
- Automatic setting of height and width from terminal (if tput is found),
- Automatic execution with rlwrap (again, if rlwrap is detected),
- Convenience flags for listing, reading, and updating databases, and
- Support for an RC file, loaded at startup.
Currently, it seems many (most?) users simply run metamath directly from the
metamath directory. The above script makes it convenient to have the files
installed in more conventional locations.
For example, the metamath/metamath-exe repository will install the following:
- Metamath executable installed to /usr/bin/metamath and
- Metamath man page at /usr/shar/man/man1/metamath.1,
which is in nice accordance with Filesystem Hierarchy Standard[0]. On my
system, this is augmented with the following:
- The attached script installed to /usr/bin/mm,
- The metamath/set.mm repository checked out in /var/lib/metamath, and
- Metamath book installed to /usr/share/doc/metamath/metamath.pdf.
The wrapper script makes in convenient, IMHO, to work with the above. Here is a
taste of usage:
$ mm -h # Shows usage information
$ mm -r set.mm # Starts metamath and reads /var/lib/metamath/set.mm
$ sudo mm -u # Performs a git pull (or git clone) into /var/lib/metamath
As usual, there are environment variables to override the defaults (e.g. if you
want a different path than /var/lib/metamath). Also, every "feature" provided
by the script can be toggled or set with a switch, so for example:
$ mm -RT <arg1> <arg2> ... <argn>
is equivalent to a simply calling metamath without the wrapper (see the help
text for details).
The script is straight POSIX shell and passes shellcheck[1], so it should be
relatively portable and solid. That said, bug reports and suggestions are
certainly welcome!
If this turns out to be useful to others, I will also consider writing an
rlwrap filter that provides intelligent completion.
Cheers!
[0]:https://refspecs.linuxfoundation.org/FHS_3.0/fhs/index.html
[1]:https://www.shellcheck.net/
--
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/3S9MMN9H6NIV1.3I7URSHL4GLK6%40wilsonb.com.
#!/usr/bin/env sh
set -o errexit -o nounset -o noclobber
METAMATH_DIR=${METAMATH_DIR-/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 repository 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}'"} \
"${@}"
