Sounds good to me. Glad to see this getting some attention - I have
figured out the status quo of wrangling RunParms.txst stuff and the
like, but it is harder than it has to be to switch between set.mm and
iset.mm, for example.
On 5/11/20 6:16 PM, David A. Wheeler wrote:
I've been working on getting it easier to get started with the mmj2 tool.
Part of the problem with mmj2 is that it has a very baroque, nonstandard command line
interface (CLI). This is one reason why I was seeking a "standard" location for
set.mm, because unlike most programs, the current mmj2 CLI doesn't let you pass a path to
the database as its first non-option parameter (!). This is in contrast to metamath-exe;
if you pass metamath-exe a single filename, it'll automatically load it (and that is a
GOOD thing)
All these nonstandard interfaces makes mmj2 a pain to get started to use. Which
is unfortunate, it has several nice capabilities once it gets going.
I'd like to change how mmj2 is invoked. Below is the current situation, a brief
discussion how programs *normally* work (which is completely different), and how I'd like
to make mmj2 work more like a "normal" program instead. This would make it
easy, for example, to put your set.mm database in any location you want without having to
edit weird files.
Comments welcome. This is in support of
<https://github.com/digama0/mmj2/issues/39> but I wanted to make sure other
people could comment ahead-of-time.
--- David A. Wheeler
=============================
The current situation is complicated. The main mmj2 program is mmj2.jar, a .jar (Java)
file. In theory you can run it directly if Java is properly installed, but in practice
you often can't; you often need to pass Java some options involving memory. The mmj2.jar
file also has incredibly weird calling convention involving a collection of arguments in
a specific order, combined with a separate mmj2 script file (such as
"RunParms.txt") that has to be edited for different databases (e.g., it sets
the name of the database to be loaded, as well as what to do afterwards).
There's an attempt to simplify this by providing some higher-level scripts that call it. E.g.,
mmj2.bat and MacMMJ2.command. However, way these higher-level scripts are called is *completely*
nonstandard. For example, there's no trivial way to say "mmj2 SET_MM_PATHNAME" and have
it just work, even though that's how programs normally work (!). In practice, you have to
edit/reprogram the top-level script and another mmj2 script (like RunParms.txt), instead of having
things "just work" out of the box.
All of this is unrelated to how programs *normally* run. In particular, most
programs can be invoked using this form:
PROGRAMNAME [OPTIONS] [FILENAME]
- FILENAME, where present, is the path to the file that will be opened and
read. This is how GUI shells (like Windows Explorer) invoke programs when you
right-click on a file to be processed. If FILENAME is absent it tries to do
some reasonable default behavior for that program (often bringing up a selector
for the file)
- OPTIONS are "-" followed by 1+ single-letter options, or "--LONG_NAME_OPTION", each followed by a parameter if
that option needs one. Historically Windows used "/" instead of "-", but many programs on Windows use
"-" today & it's simpler if we have a single convention for all platforms.
I want to make the mmj2 CLI "normal". I think we can go a long way just a modified
POSIX script & .bat file, without even modifying the Java, so I want to start there.
In particular, "mmj2 FILENAME" would open the database named FILENAME (e.g., ./set.mm
will load that file). If the filename has no directory separators and isn't in the current
directory, look for the FILENAME in "obvious places" (a search path) - this is meant to
make your life easy in case your current directory is unexpected.
If FILENAME is omitted, guess that "set.mm" was meant unless the option
--skipdatabase was provided.
We need some options. These would include:
--mmj2script FILENAME : Use FILENAME as the mmj2 RunParams file instead of the
"default"
--skipdatabase : Skip prepending the RunParams file with
"LoadFile,DATABASE_NAME" (which loads the database)
--worksheet FILENAME : Load this specific file - uses
ProofAsstStartupProofWorksheet
--tutorial : Run the tutorial (let it use set.mm!)
I'm sure other options would be useful, and more will be revealed if I implement
this, but that should give the idea. I'd implement this twice, once in shell (for
all but Windows) & once in .bat (for Windows).
Thoughts?
--
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/2219a4a3-fa56-b5c2-ee04-3be823b2b064%40panix.com.
