On Wed, Jan 8, 2020 at 6:31 AM Marnix Klooster <[email protected]> wrote:
> Hi David, > > Thanks for this, I think it will indeed help some people to get the > feeling of a hands-on experience by just watching a video. > > Some remarks: > > - Video should probably point to a download link, and some very brief > installation instructions (that is the hard part in my experience, at least > on Linux. :-) ), probably by referring to the video's description. > [Java 8 seems to be the max version per the post-2.5.3 fix for java 9+ > > <https://github.com/digama0/mmj2/commit/468e629743e09eb3f3ec5d2801a23dcd2666dfec> > and a quick test with OpenJDK 11, and probably the min version as well. > Linux Java 8 command line needs to be something like > cd /the/directory/where/you/unpacked/mmj2/mmj2jar > java -Xincgc -Xms128M -Xmx512M -jar mmj2.jar RunParms.txt Y '' > /the/directory/having/set.mm '' > ] > > MMJ2 works on java 9+ (post fix), but undo only works one character at a time; it's only that one feature (chunked undo) that was broken by the update. > > - Side note, are those leading exclamation marks explained somewhere, > either in the tutorial or in the video? Couldn't find this. > > They were added after the tutorial was written, and it seems David stuck to the script so these didn't get a mention. A ! before a step enables mmj2's more advanced unification features; they are opt in because they can sometimes be too aggressive but they are added by default on new derive steps (unless you change your RunParms settings). mmj2 will generally be able to finish the step if you provide: * Only the ref (will create the statement and derive steps) * The ref and hyps (will create the statement) * Only the statement and use ! (if the hypotheses are available somewhere in the document) This means that you can basically delete the entire right side of a proof worksheet (the statements) and it will regenerate the proof (i.e. inferred syntax steps), or the entire left side of the worksheet, giving only statements, and it will find refs and link everything together. Mario -- You received this message because you are subscribed to the Google Groups "Metamath" group. To unsubscribe from this group and stop receiving emails from it, send an email to [email protected]. To view this discussion on the web visit https://groups.google.com/d/msgid/metamath/CAFXXJSsCU0pyQ1XAECtLvesuT9Oz-hAEupr0jRvbNRA6CYQCJQ%40mail.gmail.com.
