mmj2 is difficult to install/compile/get running

cwitty commented 4 years ago

(The parts where I talk about "install" are basically an edited version of my comment on #38; the parts about "compile" are new.)

It's difficult to get mmj2 up and running, especially if you're starting from an "mmj2" Google search. My first result on Google was this repository, which is good news; but from there, the normal way to discover how to install the system -- the README.md that is displayed by Github -- is not terribly helpful. Near the top are links to QuickStart.html and README.html, but if you click on either of those you're greeted with a sea of   and HTML tags. Next is a "Quick Start CHEAT SHEET" that assumes you've already installed mmj2. After that is an Installation section that links to INSTALL.html -- another sea of   and HTML tags. (There's also a link for the "mmj2 Proof Assistant Tutorial" which takes you to the Github page for a .bat file; not terribly helpful, especially if you haven't managed to install mmj2 yet.)

If you do manage to install the system -- perhaps you found the 3-year-old release at https://github.com/digama0/mmj2/releases, or you managed to compile it for yourself -- now you need to get it to run. In particular, you need a copy of set.mm. The README.md doesn't say anything about downloading set.mm, or how to do so. QuickStart.html says to download set.mm from http://us2.metamath.org:8888/metamath/set.mm (and also says it's a 6MB download... a bit obsolete). INSTALL.html says to visit the download page of http::\www.metamath.org (note the very malformed URL) and download metamath.zip, which includes set.mm . So if you follow the links from the README, and you brave the raw HTML, you can find two different ways to download set.mm, either of which should work (although one of the ways uses Norm's home Internet bandwidth, which seems like a poor default).

Compiling it for yourself is also not easy, especially if you're not familiar with git and Java. Checking out the code is fairly easy, but then you need to use the obscure "git submodule" feature and type "git submodule init" and "git submodule fetch" before you can actually compile it. Then, the correct thing to do is to type "ant" to build it; but "ant" is not mentioned in README.md, QuickStart.html, or INSTALL.html; you just have to know that the presence of a "build.xml" file means you should type "ant".

I guess my suggestion would be to get rid of the current README.md, QuickStart.html, and INSTALL.html. Write a new README.md from scratch; make sure it has simple instructions that work. Remove the obsolete bits, like how to install Java 6.0 (as of 2011). Be sure to include where to download mmj2. (The current INSTALL.html does say to go to http://us2.metamath.org:8888/ocat/mmj2/ , which I guess is probably correct? But like I said, it's difficult to read the INSTALL.html. Before I found that in INSTALL.html, I found http://us.metamath.org/index.html#downloads , which is probably correct but looks wrong because it claims that http://us2.metamath.org:88/ocat/mmj2/mmj2.zip is "latest version, 2.4.1 26-Jan-2016"; and https://github.com/digama0/mmj2/releases, whose most recent artifact is from May 2017.) Include a section on compiling that has the "git submodule" and "ant" commands necessary.

Also, it's confusing to have old releases in https://github.com/digama0/mmj2/releases but not current releases. Maybe you could start doing github releases again? Or if you don't want to, maybe there's some way to mark the github releases as not the place to look? (I don't know what options github offers for managing that page.) Or I suppose you could consider actually deleting the old releases.

digama0 commented 4 years ago

I don't have the time to update the docs to this level. If you are willing to write a PR that rewrites the readme, great. It is literally ancient.

david-a-wheeler commented 4 years ago

I would be willing to help rewrite the teadme/install docs. This really is a problem for onboarding new folks, and it doesn't need to be.

@cwitty .. we could use your eyes. Those of us who got it working a while ago probably forgot some steps.

david-a-wheeler commented 4 years ago

We need to describe how to install/get running for Windows, Linux, MacOS. I'd like to make building optional, but to describe how to do that too.

We also need a convention for where to put things on Windows, Linux, MacOS,.

david-a-wheeler commented 4 years ago

The set.mm contribution instructions, not including tools, are here: https://github.com/metamath/set.mm/wiki/Getting-started-with-contributing

david-a-wheeler commented 4 years ago

Currently mmj2 doesn't work on Java 11. It does work on 8, which is an LTS, and officially 8 is supported through December 2020.

In the long term we need to get the code updated, but I think right now let's just focus on improving the documentation so people can easily use what we already have.

We'll need to explain how to set it up to run, including how to set up JDK 8 (if they just want to run it).

This can be a little tricky. E.g., on Ubuntu 18, you install the OpenJDK Java 8 with:

sudo apt install openjdk-8-jdk

but then you have to set the system default to Java 8 (yuk!) or run it with long incantations like this:

/usr/lib/jvm/java-8-openjdk-amd64/bin/java -Xms128M -Xmx1280M -jar "$HOME/mmj2/mmj2jar/mmj2.jar" "RunParms.txt" Y "$HOME/mmj2/mmj2jar/" "$HOME/set.mm/" ""

digama0 commented 4 years ago

Currently mmj2 doesn't work on Java 11.

Is this true of the develop branch version of mmj2? I thought the upgrade bugs were fixed, modulo some feature regression.

david-a-wheeler commented 4 years ago

I merely ran the compiled jars in the git repo. I will try to compile and test tomorrow.

david-a-wheeler commented 4 years ago

The upgrade bugs seem all fixed! Excellent!

I've created a new branch that rewrites the install (etc.) instructions. I ended up tweaking some other things to make the install easier/more sensible.

I am NOT done, but you can see my progress here:

https://github.com/david-a-wheeler/mmj2/tree/fixup

In particular, you can see the brand-new README.md and INSTALL.html - they are much simpler. The idea is to focus on helping people get started with a simple workable structure.

david-a-wheeler commented 4 years ago

Java version 8 will go out soon. Java 11 is the current LTS, and even Ubuntu 18 has it.

Should we start delivering a Java file for Java 11? Should we provide both? Should we try to provide a multi-release JAR file? (See: https://www.baeldung.com/java-multi-release-jar )

david-a-wheeler commented 4 years ago

Hopefully this will make things better:

https://github.com/digama0/mmj2/pull/42

david-a-wheeler commented 4 years ago

mmj2's CLI interface complicates things. Everyone seems to store their database, in particular, "set.mm" file in different places. There are several related problems:

Jar files, like mmj2.jar, can be directly executed. But it requires a bigger memory setting than many Java systems, so it'll fail when it tries to run. It also has an incredibly weird CLI convention. The usual convention is - or -- options flags, followed by no filename (in which case it starts without opening a main file) or a SINGLE filename (which is then opened and read). mmj2.jar totally fails to do that. What's worse, the filename isn't even provided on the command line - it's embedded within a file passed via the command line.
Scripts. The scripts don't follow the standard conventions either. They also have the problem of trying to find the .jar file. And eventually we have to find the metamath database to read.

We could make immj2's invocation more like all other programs, but doing that would require code changes (and change the CLI). Would that be acceptable?

digama0 commented 4 years ago

Yes of course. The CLI interface should be fixed, rather than passing this off to the user.

david-a-wheeler commented 4 years ago

Okay. The CLI for mmj2 is of potential more general interest, so I plan on posting my ideas to the metamath mailing list before doing anything.

david-a-wheeler commented 4 years ago

I've posted the idea of creating an mmj2 entry script that "works like a normal CLI". No complaints so far and one thumbs-up; we'll see if there are any other comments.

Since I do NOT plan to change the underlying mmj2.jar interface, existing scripts created by various people will generally just keep working. My hope is that no one will need to create another one :-).

I currently intend to focus on rewriting "mmj2.sh" as a more capable and portable shell script.

I then plan to use a tool to mostly convert it to a Windows .bat file, and fix up any remaining problems. https://github.com/daniel-sc/bash-shell-to-bat-converter is such a tool, and there's even an online bash to bat converter based on it! I don't expect the automated conversion to be perfect, but that should speed up the process.

billh0420 commented 3 years ago

I downloaded the repository into Eclipse IDE version 2020-12 (4.18.0). I found that selecting ProofAsstGUI.java as the main program that I could run it as a Java application without using the jar file. I am doing this because I want to set break points and possibly make changes. The install documentation didn't make it clear what java file to make as the starting point.

What are people using as their IDE? After making changes and compiling, are they running the jar or ProofAsstGUI.java?

digama0 commented 3 years ago

Generally, the workflow is to compile the jar and then use one of the batch files / scripts in mmj2jar appropriate for your system, which will run the jar file and pass the appropriate command line args to it. You can ProofAsstGUI.java directly, which I sometimes do for debugging purposes, but you have to put in the command line arguments as part of the run configuration in eclipse. You can copy them from any of those launch scripts, adjusting the paths as necessary.

digama0 / mmj2

mmj2 is difficult to install/compile/get running #39