A wrapper script for the metamath executable

35 views
Skip to first unread message

heiph...@wilsonb.com

unread,
Feb 4, 2020, 10:06:55 PM2/4/20
to meta...@googlegroups.com
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/

mm.sh
Reply all
Reply to author
Forward
0 new messages