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/E1jYJWt-00007E-8U%40rmmprod06.runbox.
