> 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
On Mon, May 11, 2020 at 7:58 PM Jim Kingdon <[email protected]> wrote:
> 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
> .
>
--
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/CAFXXJSuxpT8nx6rKUOEUf-SxJ27RFrRQYJp2G%3Dsy22yQemCr%2BA%40mail.gmail.com.
