search

digama0 / mmj2

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

mmj2 is still difficult to install #72

Open BTernaryTau opened 11 months ago

BTernaryTau commented 11 months ago

Since #39 mentioned wanting details about the current onboarding experience, I figured I should write up mine. This was all done on a Windows 11 machine with Java 17 (I read that Java 11 or newer was recommended and so decided to stick with Java 17). Note that I didn't start documenting everything right away, so some details may be incorrect.

I began by cloning the repository and installing the precompiled mmj2. I navigated to mmj2.bat and clicked on it, only to have a command prompt window appear and disappear with an unreadable error. I switched to running mmj2.bat from the command line, where I could see that the error was "Error: No MM database found". I navigated to the doc folder and found mmj2CommandLineArguments.html, which mentioned RunParms.txt. I edited this file so that LoadFile pointed to the location of my local copy of set.mm, and ran mmj2.bat again only to get the same error. After this, I went back to mmj2CommandLineArguments, which says that

The actual Windows command line from mmj2.bat is: java -Xincgc -Xms128M -Xmx256M -jar mmj2.jar RunParms.txt Y "" c:\metamath ""

Through trial and error I got to the command java -Xms128M -Xmx1024M -jar mmj2.jar RunParms.txt Y instead, which avoided all the garbage collection/memory errors. However, it gave me a new error:

mmj.pa.MMJException: E-UT-1502 You attempted to use a macro, but the default Macro language 'js' does not exist. Use 'MacroLanguage,xxx' with one of the following installed languages:

I did some digging until I found readme.js in the macros folder, which mentioned that Nashorn is used for the scripts. I did some googling and found that Nashorn used to be included with the JDK, but isn't included with Java 17. I downloaded Nashorn and ASM as external JARs, and rooted around through the class files to find that mmj.util.BatchMMJ2 was the main class. I thus ended up with java -Xms128M -Xmx1024M -cp "C:\Path\To\External JARs\*;mmj2.jar" mmj.util.BatchMMJ2 RunParms.txt Y as the command I use to run mmj2.

tirix commented 11 months ago

Thank you, that's very precious feedback! Install.md should be updated to reflect this.