Explain bottom-up dialogue (please review)

[david-a-wheeler]

This modifies the guide to explain the bottom-up dialogue. This was created through experimentation so I'm not sure I got it right. Please review and provide suggestions!

[david-a-wheeler]

I don't understand where the output of the "log level" goes. If you could explain that'd be great.

I don't know exactly what the statement selection does. Are these permitted or required?

[expln]

David, I will provide explanations, but later. I would like to concentrate on releasing the next version of mm-lamp. It will include proof explorer, loading existing proofs into the editor and long touch. However, the last two items are under question. If they require longer time than I expect I will exclude them. Thanks for submitting this PR!

[expln]

When you select log level, then a "show proof tree" button appears in the results of the bottom-up prover. Then you can explore the proof tree and see what the prover found. This is the purpose of this option.

You may find a brief explanation of the bottom-up prover settings here at 11:15 https://drive.google.com/file/d/1haJff_AN1M6HZGrWXsgqzrxq-Di84gmZ/view?t=675

And particularly explanation of logging levels here at 13:31 https://drive.google.com/file/d/1haJff_AN1M6HZGrWXsgqzrxq-Di84gmZ/view?t=811

I can provide more detailed explanation, but as I wrote above - a bit later.

[expln]

I don't know exactly what the statement selection does. Are these permitted or required?

statement selection means "permitted". Not selected - forbidden. There is no required option. But unchecking "allow new statements" will partially emulate "required".

[david-a-wheeler]

statement selection means "permitted". Not selected - forbidden. There is no required option. But unchecking "allow new statements" will partially emulate "required".

AHH! Okay, that makes sense. That combination allows the user to do something similar to what mmj2 users can do (specify and label and/or the statements that must be used).

[david-a-wheeler]

David, I will provide explanations, but later. I would like to concentrate on releasing the next version of mm-lamp.

Sounds wonderful!

I will modify this PR using the feedback you've already given me & by looking at the referenced video. You can then review at your convenience.

[david-a-wheeler]

At some point can you provide a copy of the images used in the bottom-up prover explanation? Those images would probably be helpful in the documentation.

[expln]

Sure, images are here https://drive.google.com/file/d/1kno1E4hYLZtZRsQ1KY88cLJxwv9Ir1f4/view?usp=sharing

I guess in a long term perspective there may be collected many different screenshots in this guide. This may increase the size of the repo significantly. And, to be honest, I am not very excited about this:) The first solution which came to my mind was to separate the code and the documentation, i.e. to create a separate repo for the guide. Then I continued evolving this thought and I think I came up with a better idea. We started with something like "let's advise newcomers to start with metamath-lamp, but there is no documentation for it, so let's create documentation". What if we change it to "let's advise newcomers to start with 'Introduction to Metamath for beginners' guide, which uses metamath-lamp, but it is not completely dedicated to it"?

It seems to me this approach solves issues related to newness and some incompatibility of metamath-lamp with conventions and approaches used in the official Metamath databases. What we have currently is a guide for metamath-lamp, but what Metamath community really needs, as for me, is a guide dedicated to Metamath in the first place, and it may use metamath-lamp as a convenient tool (but not restricted by it).

To be precise, what I am proposing: 1) Creating a new repo for "Introduction to Metamath for beginners" (this is just an example name for the guide). You will be the owner of the repo. 2) You will be composing this guide in the most beneficial for Metamath way explaining different approaches to prove theorems using metamath-lamp. 3) I will continue providing all the required info to understand how to use metamath-lamp; working on issues to make it more compatible with Metamath commonly used practices and conventions. 4) I will put a link from the metamath-lamp repo and app to this new guide as a recommendation of how to get more familiar with metamath-lamp. 5) Eventually, I will create a separate documentation for metamath-lamp with many of technical details (but it will not replace the links to the new guide).

What do you think?

[david-a-wheeler]

This really should be a new issue, but since it's here I'll reply :-).

I guess in a long term perspective there may be collected many different screenshots in this guide. This may increase the size of the repo significantly. And, to be honest, I am not very excited about this:) The first solution which came to my mind was to separate the code and the documentation, i.e. to create a separate repo for the guide.

I don't see a problem with repo size. If we were using 8-bit computers I'd obsess over it, but modern storage capacities and network speeds make that basically irrelevant.

It's obviously possible to have separate code & documentation repos. A problem with this approach is that this separation often leads to skew, that is, the documentation and code increasingly diverge because code changes don't naturally lead to documentation.

On the other hand, a separate repo would indeed focus each repo. If it's to be a new repo, I suggest creating the doc repo as a fork to maintain git history. i could move the repo into the "metamath" GitHub organization so the document can live on beyond any one person. In fact, I'd suggest that. Maybe call it "lamp-guide"? The big advantage of putting it in the Metamath org is that if someone dies, it's easy to continue. Of course, please don't die soon on us :-).

I think there is a need for documentation specific to metamath-lamp that explains, specifically, how to use metamath-lamp. I think that document is mostly done (in the sense that any software in use is "done"). There should be changes due to errors/typos. Adding some images & maybe 1 more example would be good. Most importantly, this guide needs to change as metamath-lamp changes. If programmable automation is added there might need to be a need for much more, but not until that point.

"let's advise newcomers to start with 'Introduction to Metamath for beginners' guide, which uses metamath-lamp, but it is not completely dedicated to it"?

It's hard to explain how to use a tool without being tied to the tool.

To be precise, what I am proposing:

Creating a new repo for "Introduction to Metamath for beginners" (this is just an > example name for the guide). You will be the owner of the repo. You will be composing this guide in the most beneficial for Metamath way explaining different approaches to prove theorems using metamath-lamp.

I'm not sure I'm the best person to write the tips. As far as the foundations of Metamath, well, there's a book :-).

I have thought about writing an introduction to set.mm, which would also introduce (as a side) both Metamath and mathematical foundations. It'd basically be a guided tour of set.mm. I think that's more likely the direction I would take.

[david-a-wheeler]

Hmm.. one advantage of a separate repo, in the metamath org, is that it'd get more visibility and maybe more would help improve it. That's a decent argument for doing it.