Proposal: Change mmj2's CLI

[David A. Wheeler]

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?

[Jim Kingdon]

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.

[Mario Carneiro]

> If FILENAME is omitted, guess that "set.mm" was meant unless the option --skipdatabase was provided.

I'm not a fan of this mode. I think I would prefer that there is no default, and skipping it just gives you the help text, in the same way that you can't call "gcc" with no arguments.

Also, rather than prepending LoadFile,DATABASE_NAME to the RunParms file (which will result in a malformed RunParms file if it's not accessed in this way), I would propose having variables in the RunParms file so that you can write

LoadFile,${INPUT_DATABASE_OR set.mm}

or something similar. It doesn't have to be a full blown feature, e.g. it might only work in LoadFile, but with this we can provide a suitable replacement. Actually, I think the easiest thing to add would be two new commands

LoadInputFile

LoadInputFile,set.mm

where the first one gives an error if there is no input and the second one loads set.mm if there is no input.

Similarly, the RunParms file can be used to set up the database search path, a la

AddSearchPath,.,../../set.mm

(we should look into improving RunParms syntax - the no spaces thing in particular might cause problems here - but that can wait until later.)

Mario

--
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+u...@googlegroups.com.
To view this discussion on the web visit https://groups.google.com/d/msgid/metamath/2219a4a3-fa56-b5c2-ee04-3be823b2b064%40panix.com.

[Norman Megill]

-------- Forwarded Message --------
Subject: Opening files
Date: Tue, 12 May 2020 10:41:14 +0200 (CEST)
From: fl
To: Megill Norman

 Hi Norm,

can you post this:

and what prevents from opening the file from a menu and switching between set mm and iset.mm from there.
--
FL

[Benoit]

I think the changes proposed by DAW, with Mario's remarks, would be a nice addition, adhering to standard practices and POSIX.

As for the call with no arguments, maybe the command

  $ mmj2

could simply prompt something like

  Name of the database to open:

As for FL's remark: being able to select the database from a menu would be nice indeed, but this would require a change in the mmj2 program, whereas DAW's proposal is to simply add a wrapper without changing mmj2 itself.

Benoît

[André L F S Bacci]

On Wed, May 13, 2020 at 11:18 AM Benoit <benoit...@gmail.com> wrote:

I think the changes proposed by DAW, with Mario's remarks, would be a nice addition, adhering to standard practices and POSIX.

As for the call with no arguments, maybe the command

  $ mmj2

could simply prompt something like

  Name of the database to open: 

A GUI prompt?

A command line prompt, waiting for input, is a bad practice. Command line programs are somewhat expected to act as "filters", not interactive programs.

To active a interactive mode, a specific parameter like --interactive should be indicated, to "exit" from a default, filter mode.

André

[Norman Megill]

-------- Forwarded Message --------
Subject: Widget
Date: Wed, 13 May 2020 12:57:06 +0200 (CEST)
From: fl
To: Megill Norman

 Hi Norm,

can you post this:

I insist. Why not opening the files using a widget accessed from the menu ? There are such standard widgets in every library. They are easy to plug.

--
FL

[Norman Megill]

-------- Forwarded Message --------
Subject: Widget again
Date: Thu, 14 May 2020 14:42:40 +0200 (CEST)
From: fl
To: Megill Norman

 Hi Norm,

could you post that:

I insist once again: why not adding a widget to open a file from the menu. Mmj2 has already been modified by Mario Carneiro and I see no reason why it couldn't be done once again.

--
FL

[heiph...@wilsonb.com]

This is a good point. It's probably a good idea to have different behaviour
depending on "interative" vs. "non-interactive" use.

Having a mandatory "--interacitev" option seems heavy-handed though. On Linux
at least, you can automatically detect "interactive" input by checking if
stdout is attached to a tty. This is pretty standard behaviour. For example,
compare the outputs of

$ ls # versus
$ ls | cat

They differ, with the latter ls acting like the '-1' option was passed, for
easier line-oriented parsing.

[David A. Wheeler]

FL:

> I insist once again: why not adding a widget to open a file from the menu.

Actually, mmj2's GUI *does* have a GUI widget to open a menu.
But the GUI is for loading & saving .mmp proof files, not the .mm database.

Perhaps part of what is confusing about mmj2 is that it
deals with *2* different kinds of files:
* .mmp proof files. This is the proof format it natively saves & loads, e.g.,
File/Load and File/Save use *THIS* format.
There currently isn't a command line option to load this; you can load one
indirectly via a script using ProofAsstStartupProofWorksheet
* .mm Metamath database files. It loads this database first, before
you can interact with .mmp files. It has no way to edit/save this database file.

Most programs don't have to deal with 2 different file formats, which
is perhaps part of what makes this so confusing.
Typically if there's a separate filetype, there'd be a
command line option to set it or a "distinguished argument position"
(usually the first one) to set it. E.g.:
gawk [OPTIONS] -f program-file [ -- ] file ...
gawk [ OPTIONS ] [ -- ] program-text file ...

So perhaps the mmj2 CLI should be tweaked so that the .mmp files
are the focus, at least when the GUI gets invoked. That has its
advantages: if you want to edit a .mmp file, just double-click on it.
In many ways that makes more sense, since only mmj2 can only edit
.mmp files - not .mm files.

With that in mind, maybe the mmj2 CLI should look more like this:

mmj2 [OPTIONS] [.mmp FILE]

-d METAMATH_DATABASE : Provides the path of the Metamath database.
Long option name: --database
-f SCRIPT_FILE : If present, run the script in file RUNTIME_SCRIPT
and exit on completion. This is just its current RunParams mechanism.
The script can run "RunProofAsstGUI" if it
wants to enter GUI mode as part of the script. Long name: --script-file

If "-f / --script-file" is not provided, mmj2 will:
1. load the METAMATH_DATABASE file as expressed with "-d".
The filename is a pathname to the right database.
If -d is not provided, it will use the last one it loaded,
and failing that will search in "obvious directories" to make this easy.
We can record "last one loaded" in a file somewhere in ~/.config or ~/.local.
2. If the .mmp FILE is stated & its path exists, it will load that.
If it doesn't exist, it will fail fast (mmj2 takes a long time to start!).
If no .mmp FILE is stated, a convenient default is loaded
(that way the user can see SOMETHING
and then load something else).

I didn't see any obvious option flag names to steal from here:
https://www.gnu.org/prep/standards/html_node/Option-Table.html

Thoughts?

--- David A. Wheeler

[Norman Megill]

-------- Forwarded Message --------
Subject: Libraries and text files
Date: Sat, 16 May 2020 14:32:08 +0200 (CEST)
From: fl
To: Megill Norman

 Hi Norm,

Can you post this:

Many softwares permit to open two kinds of files. Editors for instance. Especially Emacs. You can open libraries (well the received word is "load" ) and you can open text files. And both have their utility. Here  we are in the same case.

By the way if somebody could remove the header in the mmj2  files. Nobody uses it in my opinion. Since all that is under git, you might create a feature branch where the header is kept and remove it from the trunk. It would be possible to reintroduce the feature when it is complete and if it turns out it is useful.

--
FL