search

digama0 / mmj2

mmj2 GUI Proof Assistant for the Metamath project
GNU General Public License v2.0
72 stars 24 forks source link

Fixup #42

Closed david-a-wheeler closed 4 years ago

david-a-wheeler commented 4 years ago

I've tried to make a number of improvements to the install & getting started instructions, without changing how mmj2 works.

I removed the bogus version check; that should help it run on Debian.

I installed a precompiled Java 11 .jar file. At this point I think Java 11 is more common; Java 8 users can compile it themselves using the provided instructions.

Things could be improved further, but I think this is an overall improvement.

david-a-wheeler commented 4 years ago

Based on the mailing list comments I created a new "mmj2" front-end script that will work on all but Windows (I'll have to write a .bat file equivalent).

This means you can use a single command to choose the database and/or starting .mmp file, and if you don't give it that information, it'll figure something out. For many people it'll just "work out of the box", and if not, in most cases you'll only have to tell it once where to find the database.

Usage:

    mmj2 [ -f RUNCOMMANDS ] [ -d METAMATH_DATABASE_FILE ] [ FILE ]
    - If FILE is a .mmp file, open that .mmp file when starting out.
    - If FiLE is a .mm file, open that database and use a "default" .mmp file.
    If METAMATH_DATABASE_FILE isn't provided, it makes an effort to find it,
    and records its location in ~/.config/mmj2/default_database for next time.

If this is reasonable, I'll modify the documentation to match.

Since I'm not modifying the underlying jar file interface, everyone with RunParams files can continue to use them unchanged.

Thoughts?

david-a-wheeler commented 4 years ago

Okay, I think I've resolved all the comments.

The biggest annoyance was rewriting the shell script as a .bat script. Batch scripts are a horror that no one should have to deal with!

david-a-wheeler commented 4 years ago

So are we ready to make it much easier for people to install & use mmj2?

david-a-wheeler commented 4 years ago

Are we ready to merge? As far as I know all issues have been addressed. This one is much easier to install and used.

Since it wasn't merged yet, I tweaked the .bat file. But I'd like to get this merged in - one less problem for people to get started with Metamath!

david-a-wheeler commented 4 years ago

@digama0 - I think all issues have been resolved, let me know if there's anything that must be resolved before merging.