> Maybe you can let me know exactly what files you'd like to see in it. Thank you for engaging so openly.
Personally, my preferences align mostly with FL's. As a Linux user, the default
expectation I have for a source tarball (in this case metamath-program.zip) is
that I can do
$ ./configure && make install
and it Just Works (modulo concerns about external dependencies). To get this
working we just need to patch Makefile.am like this:
*** a/Makefile.am 2019-12-17 15:32:41.797498961 +0900
--- b/Makefile.am 2019-12-17 15:33:22.713276422 +0900
*************** metamath_SOURCES = \
*** 36,49 ****
mmwtex.c \
$(noinst_HEADERS)
- dist_pkgdata_DATA = \
- big-unifier.mm \
- demo0.mm \
- miu.mm \
- peano.mm \
- ql.mm \
- set.mm
-
EXTRA_DIST = \
LICENS@
followed by running
$ autoreconf -i
That should produce a source bundle that builds "as normal." If we really want
to make things look like bog standard *nix sysops, then I second FL's
suggestions:
1. Remove the metemath.exe executable,
2. Provide as a tar.bz2 instead of a zip, and
3. Include the Metamath book TeX source.
The only hanging thread is how to acquire the databases. The easiest solution
here is probably to just leave this detail to the package maintainers and/or
users. It might be nice to include a README in the tarball, explaining what the
source includes and what it does not.
On my own machine, I just clone the set.mm repo locally, set the environment
variable METAMATH_DIR pointing there, and then a wrapper shell function
provides easy loading of databases, automatic sizing, rlwrap, etc:
mm() {(
usage=$(cat <<-USAGE
Usage: mm [-hl] [-d <database>] [-r <rcfile>] [<args>]
OPTIONS
-d <database> Load <database>
-r <rcfile> Submit <rcfile> commands on startup, defaults to ~/.metamathrc
-l List available databases
-h Display this help message
USAGE
)
while getopts ':d:r:hl' opt "${@}"; do
case "${opt}" in
d) db="${OPTARG}";;
r) rc="${OPTARG}";;
l) find "${METAMATH_DIR}" -name '*.mm'; exit;;
h) >&2 echo "${usage}"; return 0;;
:) error "Expected argument: -${OPTARG}" "${usage}"
return 1;;
*) error "Unknown argument: -${OPTARG}" "${usage}"
return 1;;
esac
done
shift $((OPTIND - 1))
rc="${rc:-${HOME}/.metamathrc}"
[ -r "${rc}" ] || unset rc
rlwrap --complete-filenames \
metamath "set width $COLUMNS" \
"set height $((LINES - 1))" \
${rc+"submit '${rc}'"} \
${db+"read '${METAMATH_DIR}/${db}'"} \
"${@}"
)}
The only missing piece that I currently want is a nice rlwrap perl script that
provides context-aware completion. Otherwise, I find the metamath executable
itself quite ergonomic!
Norman Megill <[email protected]> wrote:
> On Monday, December 16, 2019 at 8:34:02 AM UTC-5, heiphohmia at wilsonb.com
> wrote:
> >
> > > And why not a special Linux source distribution...
> >
> > The URL that Norm shared pretty much ticks all the boxes you outline. The
> > only
> > substantive difference being that the metamath.exe is not excluded.
> >
>
> I could take it out if that is preferable. I left it in in case a Windows
> user (who typically has no C compiler) wanted to download just the program
> and sources, although there is also a direct link to metamath.exe on the
> home page so it isn't really necessary.
>
> Maybe you can let me know exactly what files you'd like to see in it.
>
>
> >
> > The source uses GNU autotools, so the standard build procedure Just Works
> > if
> > you first generate the necessary files with
> >
> > $ autoreconf -i
> >
> > I do find it curious that the advice for *nix builds is to directly call
> > gcc.
> > Perhaps the build instructions could be updated to this:
> >
> > $ autoreconf -i && configure && make
> >
> >
> I could add this as an alternate build method, but these are
> Linux/Unix-specific and may not be available on all systems. The program is
> very portable and purposely calls no external libraries or does anything
> that isn't strictly part of ANSI C, with the only exception AFAIK that it
> doesn't support the EBCDIC character set.
>
> (Personally I mostly use lcc during development because it compiles much
> faster than gcc, and occasionally use gcc for its better error messages and
> faster run time. Also, autotools is painfully slow, issues screenfuls of
> messages I have to scroll through to find a real error, and clutters up the
> directory with dozens of unwanted files, making development annoying and
> inefficient. Am I doing something wrong, and how do most people deal with
> this?)
>
> I just tried to run autoreconf -i && configure && make, and it doesn't work
> with metamath-programs.zip because it presupposes the databases are there.
> I'm not really that confident with autotools, and it would be best if
> someone else adjusts them.
>
> Norm
>
> --
> 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/8c5bd45d-5b88-4507-a2ba-0d89d154c0d8%40googlegroups.com.
--
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/5df87da8.c5Sa%2BUSFHZrCQdpS%25heiphohmia%40wilsonb.com.
sig.asc
Description: application/pgp-encrypted
