search

digama0 / mmj2

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

Fix tutorial #38

Closed david-a-wheeler closed 4 years ago

david-a-wheeler commented 4 years ago

I normally just run "mmj2" so I didn't notice the problem.

digama0 commented 4 years ago

@cwitty, does this solve your problem?

cwitty commented 4 years ago

Well, I solved my own problem; so the real question is "does this solve the problem for the next person to try it". And I'd say it depends on the level of technical competence and dedication of this hypothetical person; but maybe not.

1) The README still doesn't mention Linux.

2) The .bat files don't have -Xincgc any more; good. (But I notice that the OSX .command files still do.)

3) The bad path separator (backslash instead of slash) is fixed.

4) Now, running the tutorial fails immediately with a dialog box "mmj.mmio.MMIOException: A-IO-0105 Step Loadfile: Load() file not found." The README.md doesn't say anything about downloading set.mm, or how to do so. The README does refer to QuickStart.html, which does say to download set.mm from http://us2.metamath.org:8888/metamath/set.mm (and also says it's a 6MB download... a bit obsolete). The README also refers to INSTALL.html, which 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, 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). But following the links from the README is not easy. A Google search for mmj2 brings me to https://github.com/digama0/mmj2 , so the README.md is nicely visible and reasonably formatted there, in the standard Github fashion. Clicking on the links to QuickStart.html or INSTALL.html from that copy of README.md bring you to the Github source-code-formatted raw HTML files, which are offputting and difficult to read (probably difficult enough that a lot of people would give up there).

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.)

I seem to have expanded the scope of my initial request greatly, and probably a comment on a pull request is not the best place to do so. Let me know if you'd like me to turn this into a separate issue; or feel free to do so yourself.

david-a-wheeler commented 4 years ago

@digama0 - I think we should merge this pull request now. It's better than it used to be, and it solves the immediate problem @cwitty was having.

@cwitty - Yes, PLEASE create a separate issue. Re-post your comment about the README and INSTALL in a new issue, though of course if you want to modify it, do that. We need to modify the instructions - and probably some code - to make installations easy & painless on Linux, MacOS, and Windows. Onboarding is currently a pain, and it needs to be made easy.