Proposal: Change how justifications & hypothesis changes are done (not sure this is a good idea)

[david-a-wheeler]

This is a UI proposal, it doesn't change functionality. Do with it as you will, it's not critical, but maybe you'll find it interesting.

Currently there's a little "P" that toggles display of a justification on the next line. But often I want to see all justifications or none, and having each one on its line wastes a tremendous amount of space when I'm using a larger display.

I proposal instead having a toggle at the top that turns on/off displays of justifications; when on, it displays in the same line the justification or something that indicates it's a hypotheses (maybe HYP). When off, this becomes a tiny minimized column that shows H or P (if it's a justified provable statement) or "-" (if it's supposed to be provable but is not yet justified). Hovering over it shows a tooltip: "Hypothesis NUMBER" if a hypothesis, the justification if it's justified along with "Press Alt- to generate proof", or "This is not yet proven". You could change a statement between H and P by selecting it and then selecting a new button at the top "H<>P" (this would make the ability to change a statement type more obvious).

[david-a-wheeler]

Hmm, after using this further, I realize that the "next line" is nice on narrow screens like those on smart phones... and that this system is quite usable on a smart phone. I don't know if my proposal would work so well on a smart phone.

[expln]

Probably I can implement different behavior depending on a screen width. I will check.

[david-a-wheeler]

I'm sure you can change how things look depending on the width, since simple CSS can do that.

However, I don't think you want to change too much about behavior - instead, provide multiple mechanisms that all work (if they work at all). I expect some users to use both a smartphone and a big screen (e.g., laptop). If it's possible to do the same action it should work the same way. I may be reading too much into your word "behavior" :-).

[david-a-wheeler]

More thoughts...

I think it really would be nice to be able to see, on one line, the justification refs and hyp steps. But whether or not the user wants that will vary by person as well as by screen size.

So instead of making that based on width, how about making two on/off in settings, for "show refs in editor" and "show hyp steps in editor"? Then the user can turn each on or off. If on, that extra info will be available on that line. Extra points if you can click on the ref (opening a dynamic tab on it) and the step used (jumping to it).

[expln]

So instead of making that based on width, how about making two on/off in settings, for "show refs in editor" and "show hyp steps in editor"? Then the user can turn each on or off.

Yes, I think this is a good approach. I actually was going to implement it. But I also include more options to show/hide other UI elements: checkboxes, labels, H/P/G indicators. I am going to place these options in the editor for not to switch to the settings tab.

Extra points if you can click on the ref (opening a dynamic tab on it) and the step used (jumping to it).

In that case long-click to edit and short click to jump?

[david-a-wheeler]

Yes, I think this is a good approach. I actually was going to implement it. But I also include more options to show/hide other UI elements: checkboxes, labels, H/P/G indicators. I am going to place these options in the editor for not to switch to the settings tab.

Sure!

Extra points if you can click on the ref (opening a dynamic tab on it) and the step used (jumping to it).

In that case long-click to edit and short click to jump?

This is regarding the steps and justification, right? The goal of course is consistency.

Hmm, that sounds right, I guess the rule is: "on a link, normal click always jumps to it, long click might do something else". In that case all hyperlinks (like the step id or ref) to jump to something should be made to look like a hyperlink. That would help discoverability too, if in the explorer the name of the theorem/axiom looked like a hyperlink. By "looks like a hyperlink" I mean "underlined and in blue" or some similar visual indicator.

[david-a-wheeler]

BTW, your v11 list is ambitious! Can't wait to see it released.

[expln]

@david-a-wheeler

Currently I am concentrating on implementation of the features you listed as required or highly wanted for the video tutorial. The features in v11 list are those which I estimated as relatively easy to implement (I was in rush, so I could miss some or include something by mistake). The problem is that it is difficult to predict how much time I need to complete everything. I planed to finish the features you listed and then ask you if you want to wait until I am done with everything else in v11 list, or you want to start creating the video tutorial as soon as possible. Since you already noticed this list, could you please review it and let me know if you are ok to wait for everything in it (with undefined due date)? Or you may select only what is valuable for the video tutorial, and everything else will be moved to v12. Another option is to select most wanted features and set up a hard deadline (say 2-3 weeks after I finish the features you've listed for the tutorial) and whatever is ready until then gets published to the latest version and everything else is moved to v12.

It is not required to come up with a decision right now, we may discuss this when I finish the features you've listed for the tutorial.

We also may move this discussion to the tutorial related issue in the guide repo.

[david-a-wheeler]

Thanks for offering to discuss v11. That is its own issue, so in the hope of making things easier to understand, I created a separate issue to discuss that: #83

[expln]

@david-a-wheeler

There is a bug on dev (which I've just noticed) - justifications are shown for hypotheses too. I am going to implement the following (in v11, because that should be easy):

1. The content of justification for hypotheses will always be HYP.
2. If you add a new step and want it to be a hypothesis then you may set its justification to hyp and it will be automatically converted to a hypothesis. So you don't need to use the step type indicator and you may even hide it.
3. If you remove content of the justification then it is automatically converted to a P.

Please let me know if you think this is wrong or you have a better idea.

(I came up with this idea after re-reading your first comment in this issue :) )

[david-a-wheeler]

justifications are shown for hypotheses too. I am going to implement the following (in v11, because that should be easy)

I like that! I'm guessing there will be no ":", so a database with label "HYP" would not be confused with that being an axiom or theorem. Presumably we don't want local labels named HYP.

[david-a-wheeler]

BTW, I think showing the justifications by default is wise. It certainly makes the tool easler to explain, and even on a smartphone I do want to see them.

[expln]

I'm guessing there will be no ":", so a database with label "HYP" would not be confused with that being an axiom or theorem.

Yes, : will be used to distinguish these cases visually. However, internally, mm-lamp checks if a step is H or P. If the step is H then mm-lamp doesn't even attempt to interpret its justification.
Also, internally there is no G type, only H and P; G = {type:P, isGoal:true}

Presumably we don't want local labels named HYP.

Currently I don't want to restrict users by this rule. If it is not forbidden by Metamath, then let them do whatever they want ( in the scope of what mm-lamp can do :) )

[expln]

This is implemented on dev. Here is a brief description of what was changed:

• It is possible to select what to show on same line with each step.
  Use "main menu" in the editor to open "view options" dialog. This dialog allows to select what to show and what to hide.
• If justifications are not shown to the left of statements, then clicking on either green checkmark, or the label or the step type will reveal the justification.
• If justifications are shown to the left of statements, then clicking on either green checkmark, or the label or the step type will reveal the visualization.
• for hypotheses, a justification is also shown, but it is always HYP.
• Setting hyp (case insensitive) as a justification for a provable step will automatically change its type to H.
• Setting a justification to anything other than hyp (case insensitive) for a hypothesis step will automatically change its type to P.