Draft mmj2 tutorial - feedback wanted!

[David A. Wheeler]

I've created a tutorial on using mmj2. It's basically just a video recording
of me walking through (most of) the tutorial included in mmj2.

The advantage of a video recording is that
people don't have to install anything to see the tutorial.

You can see it here:
https://www.youtube.com/watch?v=gAMf4tfoXjY

I'd love to hear feedback!

This is an *unlisted* URL, please don't post the URL everywhere.
I intend to make modifications (based on feedback) and officially post
the URL for the final version.

--- David A. Wheeler

[Marnix Klooster]

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+ 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 ''
  ]
  
• Video might explain a mmj2 version check (Help -> About mmj2).
  
• 0:35: "mmj2" is read as "mmg".
• 14:35: The video explains how the tutorial doesn't match the recent notation change in mmj2 step:hyps:ref-- instead of explaining that in the video, shouldn't the tutorial be fixed before publishing the final video?
• 21:43: Switched to 'reiteration.mmp' file name for Page401.mmp, which makes it a bit difficult to follow along if (like me) you only look at the mmj2 window title bar. :-)
• 23:36: Probably you should explicitly mention that you are skipping Page402.mmp and Page403.mmp, about 'only assertions in the Ref part of a step'?
• 26:13: Skipping Page 405.mmp without mention, presumably because the instructions are not correct (Edit/Undo doesn't do anything after just loading the page, of course).
• 30:04: The result of Page409.mmp is actually different from the starting point of Page410.mmp (d1/d2->1001/2001, and the leading exclamation marks are done).  That difference doesn't teem to matter.
• Side note, are those leading exclamation marks explained somewhere, either in the tutorial or in the video?  Couldn't find this.

Those were the nits I could find. :-)

Again, thanks for this effort!!

Groetjes,

 <><

Marnix

Op di 7 jan. 2020 om 23:43 schreef David A. Wheeler <dwhe...@dwheeler.com>:

--
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 metamath+u...@googlegroups.com.
To view this discussion on the web visit https://groups.google.com/d/msgid/metamath/E1ioxZJ-00009P-Iy%40rmmprod07.runbox.

--

Marnix Klooster
marnix....@gmail.com

[Jon P]

Hi David, very nice tutorial, I learned a lot of interesting things. 

Re the sound quality I think maybe you are a bit close to your mic, you are getting a bit of breathing coming through and popping on p sounds. However it isn't a big deal and wasn't particularly noticeable.

You say in some places, like in file 302, that things have changed since the tutorial was written and it is a bit outdated, such as it now needing more :'s. Do you think it is worth updating the tutorial files when you found these?

For me the most useful feature of mmj2 is putting an ! at the beginning of the line, this seems to magically fill in everything for me which is very nice. It seems this did not come up in the tutorial and it's the first thing I would tell people ha ha.

Overall very nice, thanks for making it. 

Jon

[Mario Carneiro]

I agree with Marnix that you should just pre-fix the tutorial pages rather than talking about how the tutorial is out of date in the video. Also, on page 303 you forgot to put "200,1000" in for step qed. (But it would be more impressive if you put a ! at the start, as in "!qed" with nothing else, and then it will figure out *both* the hyps and the ref. But that is a feature added after the tutorial was written.)

The transition from page 404 to 405 is incorrect, because the derive steps now have a different format, namely !d1:: rather than 1000:?: . Again this is a place where the tutorial should be fixed rather than talking around it. In addition, I would recommend using "!step::" for incomplete steps rather than "step:?:", as the bang will cause it to try to passively justify it on every unify (meaning that unrelated steps can sometimes get proven while you are working on something else), and the ? is no longer necessary to indicate "incomplete hyps" and will interfere with unification (as indicated, it doesn't try to unify these steps). I would have completely removed the "?" but it breaks a lot of backward compatibility. It is currently only useful for the "step search": if you double click on "step:: |- foo" then it will search only for proofs of |- foo with no assumptions, and if you double click "step:?: |- foo" it will search for proofs of foo with possibly additional hypotheses.

On page 411, it might be worth mentioning that you can also write "#" instead of "#1" and it will search for any matching step. If you use this form it will only search previous steps, but the #1 form will also work if it is a forward reference, and it will check that you aren't creating a cycle and reorder all the steps so that references are topologically sorted.

--
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 metamath+u...@googlegroups.com.

To view this discussion on the web visit https://groups.google.com/d/msgid/metamath/175830c6-3ad4-4460-a2a2-da743f902220%40googlegroups.com.

[Mario Carneiro]

On Wed, Jan 8, 2020 at 6:31 AM Marnix Klooster <marnix....@gmail.com> 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+ 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

[Jim Kingdon]

At 0:35 you say m-m-g instead of m-m-j-two.

At 6:16 you hesitate about how to pronounce the turnstile. I guess bar-dash is probably a better pronounciation than, say, turnstile (because "implies", for example is a lot more familiar than "turnstile"). So maybe there's not even a need to change anything (even the hesitation is sort of a "maybe you haven't seen this one before" cue).

At 9:03 you say "ph" instead of "ps".

Generally, I like this. The video should make it noticeably easier to learn mmj2. I learned two new things watching it (not because I'd never been through the tutorial, just that I'd never revisited it.

[Jim Kingdon]

On 1/8/20 5:01 AM, Mario Carneiro wrote:

> I would have completely removed the "?" but it breaks a lot of
> backward compatibility. It is currently only useful for the "step
> search": if you double click on "step:: |- foo" then it will search
> only for proofs of |- foo with no assumptions, and if you double click
> "step:?: |- foo" it will search for proofs of foo with possibly
> additional hypotheses.

The ? is still useful in telling mmj2 which hypotheses to fill in. For
example, if I have a step 500 and I want to say

510:500:syl2anc

and have mmj2 fill in the other two hypotheses. Before typing control-U
I can modify that to be:

510:?,?,500:syl2anc

or

510:500,?,?:syl2anc

before writing unify.

I just tried this with mmj2 2.5.3 as of 23-Sep-2019 (as reported in the
About box).

[David A. Wheeler]

On Wed, 8 Jan 2020 03:44:46 -0800 (PST), Jon P <drjonp...@gmail.com> wrote:
> Re the sound quality I think maybe you are a bit close to your mic, you are
> getting a bit of breathing coming through and popping on p sounds. However
> it isn't a big deal and wasn't particularly noticeable.

I don't really have a better option.
The "default" microphone level was hard to hear, so I had to
increase the volume using ffmpeg's "loudnorm" in a postproduction step.
I have another microphone, but it recently stopped working :-(.

> You say in some places, like in file 302, that things have changed since
> the tutorial was written and it is a bit outdated, such as it now needing
> more :'s. Do you think it is worth updating the tutorial files when you
> found these?

It'd be great to update the tutorial files.

However, my intent for this video is to "walk through" the mmj2
tutorial as it is provided by mmj2. So Mario would need to be willing
to accept or make changes to the tutorial within mmj2
and then cut a new release.

Mario: are you willing?

I'll also probably need some help updating those tutorial files.
I skipped a few tutorial pages because I couldn't get them to work
(admittedly I didn't try hard, making the video at all was an effort).

> For me the most useful feature of mmj2 is putting an ! at the beginning of
> the line, this seems to magically fill in everything for me which is very
> nice. It seems this did not come up in the tutorial and it's the first
> thing I would tell people ha ha.

Would you or someone else be willing to create another .mmp page
that explains it?

I know mmj2 has some other nifty features
(like search) that also aren't explained in the mmj2 tutorial; it might be
good to add a few more pages to do that.

> Overall very nice, thanks for making it.

Thanks! Though I don't think we're done yet :-).

As an aside: it was harder to do this than expected.
Youtube no longer has a useful built-in video editor :-(.
I created the video as a bunch of small sections (using snagIt),
so that I could re-record anything that needed redoing.
When I tried to concatenate them with ffmpeg, the sound and video
immediately got out of sync (because the fragment sound & video
weren't of identical length), and I couldn't find a way to fix that in
ffmpeg. MP4Box managed to do it nicely (though it can only combine
up to 20 fragments, so I had to do it in stages). I then used ffmpeg to
fix the microphone volume. I just mention all this to warn anyone
who's trying to create video - it seems to *always* be a pain :-).

--- David A. Wheeler

[Jim Kingdon]

Thanks for doing this, David!

Although there are a lot of nice-to-haves in terms of updating and otherwise improving the tutorial, and hopefully some of these will happen, even without them I think this would be better than nothing.

As for editing video, sorry to hear it isn't as easy as one would think. I note that the internet is full of questions like "Is there any video editing software that combines the functionality of Audacity w/ video?"

Sound quality is another nice-to-have in terms of experimenting with microphones, software and even the room where one records, but at least for me it was "good enough" in the sense of not being distracting.

[Jim Kingdon]

>> - Video should probably point to a download link, and some very
>brief
>> installation instructions

I'd be reluctant to include this in a video because (a) video isn't a great medium, you'd be pausing it while you follow them, as opposed to text where you just open instructions in another window, and (b) this sort of thing tends to change a lot (either mmj2 changes, or operating systems and Java change), and videos are hard to update.

[Mario Carneiro]

I think you can just write

510:,,500:syl2anc

or

510:500,,:syl2anc

for that.

--
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 metamath+u...@googlegroups.com.

To view this discussion on the web visit https://groups.google.com/d/msgid/metamath/6ca7f932-4475-3dcc-d66b-d42c2296a63c%40panix.com.

[Mario Carneiro]

On Wed, Jan 8, 2020 at 11:02 AM David A. Wheeler <dwhe...@dwheeler.com> wrote:

It'd be great to update the tutorial files.

However, my intent for this video is to "walk through" the mmj2
tutorial as it is provided by mmj2. So Mario would need to be willing
to accept or make changes to the tutorial within mmj2
and then cut a new release.

Mario: are you willing?

Absolutely. I don't have time to write a new tutorial myself right now, but checking that your changes are correct is comparatively easy, and it doesn't affect the build at all so I don't see any reason not to merge anything you send me right away.

I'll also probably need some help updating those tutorial files.
I skipped a few tutorial pages because I couldn't get them to work
(admittedly I didn't try hard, making the video at all was an effort).

By the way, I don't know if this is deliberate, but you stuck pretty close to the tutorial text, which made it a bit staid. You should inject your own opinions on what's being described or restate things in your own words if you can, as it will make it sound more natural. But this isn't really a specific complaint, just something to keep in mind if you re-record any of the segments.

Mario

[David A. Wheeler]

>On Wed, Jan 8, 2020 at 11:02 AM David A. Wheeler
><dwhe...@dwheeler.com>
>wrote:

>> Mario: are you willing?

>Absolutely.

Great! Sounds like a plan. I will probably need to redo the tutorial after we fix things up.

>By the way, I don't know if this is deliberate, but you stuck pretty
>close
>to the tutorial text, which made it a bit staid.

100% intentional. It's a lot of extra work to come up with my own script. Simply reading the text is pretty justifiable since I'm basically just going through the tutorial. It also means that if someone has trouble understanding something I say they can look at the text posted.

I did exactly that in the video to create a function in mmj2, and while I think that was quite successful, it was also a lot of work.

--- David A.Wheeler