mmj2 tutorial issues: can't start on Linux; chapter 5 is broken

[cwitty]

I wanted to run the tutorial, but there were several roadblocks in my way.

1) The instructions talk about Mac OS-X and Windows, but not Linux. Not a big problem; I just copied the command line out of mmj2PATutorial.bat and ran it by hand.

2) That command line uses the obsolete "-Xincgc" flag, so it doesn't work on the version of Java I have ("14-ea", from Debian openjdk-14-jdk 14~36-2). So I deleted the "-Xincgc" part from the command line and re-ran.

3) The command line references RunParmsPATutorial.txt , which has this line:

ProofAsstStartupProofWorksheet,PATutorial\Page101.mmp

That pathname doesn't work on Linux. So I copied PATutorial/Page101.mmp to PATutorial\Page101.mmp and re-ran.

4) I finally was able to get into the tutorial, and got through most of it. But when I got to chapter 5, I got an initially mystifying error when I followed instructions and pressed Control-U on Page501.mmp:

E-PA-0343 Theorem 95p1e96 Step qed: Invalid symbol in proof step formula. Input token = ; not found in Logical System Symbol Table. Proof Text input reader last position: Source Id: Proof Text Line: 28 Column: 12
 --------------------------------------------------------- 

I eventually figured out that this is because RunParmsPATutorial.txt loads setFirst100.mm, which doesn't have decimal notation (or real numbers, or set theory, or predicate calculus).

I can see a couple of possible fixes: either copy enough of the current set.mm into setFirst100.mm to get through the tutorial, or get rid of setFirst100.mm altogether and tell users they need to download the real set.mm. But the current situation, where following instructions gets a tutorial that breaks mysteriously at chapter 5, is very bad.

[digama0]

cc @david-a-wheeler , who added those pages to the tutorial

[david-a-wheeler]

Thanks so much for the report and fof some suggested fixes!! Yes, we need to fix this.

[david-a-wheeler]

Here's a PR that fixes most of that:

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

@digama0 - will you please merge #38? This builds on my previous fix to increase maximum memory, which I believe addressed your previous concerns with that.

We need to explain how to get the real set.mm. Updating README might not be a bad idea either :-).

[benjub]

@cwitty Does this work with the fix of #38 ? I'm also using Debian testing and I had to downgrade to JDK 8 (see https://groups.google.com/d/topic/metamath/WFoQTXy17lU/discussion). I'd be glad if it works with current Java.

@david-a-wheeler I don't know much about garbage collection, but what does removing -Xincgc entail ? I replaced it with -XX:+UseConcMarkSweepGC but not sure how performance compares.

[david-a-wheeler]

@benjub: Java has always had a garbage collector. The -Xincgc option was originally off by default; when the option was added, it enabled the incremental garbage collector, which reduces "the occasional long garbage-collection pauses during program execution." However, it's been on by default for many versions, and they've removed the option. I think it's absurd to remove a no-op, it makes it hard to support many Java versions simultaneously. But since newer versions don't accept it, and it's been a no-op for many years, it makes more sense to just remove calling the option. Fiddling with garbage collectors can bring you down a deep rabbit hole; I don't feel like jumping down that hole today :-).

[david-a-wheeler]

I always ran mmj2, even when doing the tutorial, so I never noticed the problems with mmj2PATutorial.bat.

[cwitty]

@benjub, after I commented out the body of checkVersion() in BatchMMJ2.java and recompiled (as described in #36) and removed -Xincgc from the command line, I was able to go through the tutorial with a current Debian testing openjdk-14-jdk (until I got to chapter 5, where I had to replace setFirst100.mm with the real set.mm).

I haven't tested it, but my expectation would be that any set of garbage collector parameters would work fine for mmj2. I agree with @david-a-wheeler that it's not worth my time fiddling with them. In other words: feel free to keep using -XX:+UseConcMarkSweepGC or to leave it off; I doubt if you'll notice a difference either way, unless you try doing careful benchmarks and statistics.

[benjub]

@cwitty Thanks. Using openjdk-8 and openjdk-11 (default-jdk) on Debian testing, mmj2 launches but has unexpected behavior which makes it unusable (described in the linked thread) which I cannot fix...

Edit:

$ java -version
openjdk version "11.0.7-ea" 2020-04-14
OpenJDK Runtime Environment (build 11.0.7-ea+9-post-Debian-1)
OpenJDK 64-Bit Server VM (build 11.0.7-ea+9-post-Debian-1, mixed mode, sharing)

Command line: java -Xms256M -Xmx512M -jar .....

[cwitty]

@benjub, it looks like your problem is that you can't compile mmj2 because of the missing JSON files? I just tested this, so here's a chunk of my "history" where I successfully cloned my existing repository, updated it with the JSON files, and compiled:

 1711  git clone ../mmj2
 1712  cd mmj2
 1713  git submodule init
 1714  git submodule update
 1715  ant

(You'd probably want to clone from github instead of "../mmj2". Also, if you're on openjdk-14-jdk, you'll need to coment out the body of checkVersion() to get a jar file you can use.)

The magic incantation:

git submodule init
git submodule update

is actually in mmj2's INSTALL.html, if you scroll far enough down past the instructions on installing the 2011 version of Java...

[benjub]

Thanks @cwitty. I'll give it a try when I have time. (I don't know if it's a mistake, but I don't use git for mmj2 since I don't plan on modifying it; I simply download it the old-fashioned way.)

[david-a-wheeler]

@benjub - okay, you have the lead. Please post a link here to your try. A few thoughts:

• Explain how to install mmj2, but also hint at a convention for installing at least set.mm (and probably metamath-exe as well). On Linux and MacOS at least the file "set.mm" should be a subdirectory of the home directory. It might be wise to do the same with mmj2 and metamath-exe, since then we don't have to have privileges for installs.
• We need to cover Linux, Windows, MacOS. I can help with the first two. I'd like to include Cygwin-on-Windows (perhaps use that as the Windows case); I know that works.
• Ideally we'd have both the "no-recompile" and "recompile" cases. No-recompile is easier, but the recompile version can get latest releases & allows you to modify the code if desired.

[benjub]

@david-a-wheeler Sorry if my words misled you. What I meant by "I'll give it a try when I have time" was "I'll give it a try next time I want / have time to use mmj2... which may not be too soon". When I try, I'll report it, but this may be in a while.

[david-a-wheeler]

@benjub - thanks for the clarification. In that case, I'll try to work up something.