When should version 11 be released?

[david-a-wheeler]

When should version 11 be released?

In the end, that decision is up to @expln . Here is expln's v11 milestone list

That said, it sounds like it'd be useful to have an organized place to discuss this, and I'd rather have an issue specifically focused on it.

As expln said in a comment in issue 16:

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.

Since this is fundamentally about the tool, I've created an issue here in the tool issue tracker. A related issue is Create introduction videos with audio.

[david-a-wheeler]

@expln : My inner 5-year-old wants everything in the current v11 list and more, and wants it right now :-).

That said, I'm a believer in "release early, release often". The sooner you release, the sooner you get feedback on what's important (and what isn't).

There's already more than enough functionality to justify a release, really.

I have one request before v11 is released, if I may request it and it doesn't take too long:

• Enable visualization per justification, instead of a global setting Enable visualization per justification, instead of a global setting #56

That's weirdly specific, I know. The primary reason is that I want "enough UI stability" before I create a video, so that the video won't look too wrong when the next few tool releases come out. Issue #56 will involve a nontrivial UI change, so I'd rather have that in before making a video. I intend to focus on the 2+2=4 video, and visualization is definitely something I intend to emphasize. So I'd prefer it if its enabling/disability functionality per step was already implemented.

Also, this ability will make it easier for users to explore the justifications, even on smaller screens. That way they can enable displaying just justifications in some places, and full visualizations in others.

Given that, here at the headline items that I see:

• Now works on smartphones' browsers. A "long click" (long touch) is interpreted the same as alt-click, giving you access to all tool functionality.
• Explorer lets you view the axioms & theorems in the current context. You can select any of them to show the detailed proofs (with or without syntax proofs) and use hyperlinks to switch to other proofs.
• One step can be designated as the "goal". The tool keeps the goal at then end, making interactions simpler.
• Visualizations can be enabled or disabled individually for any step you desire, instead of being "all displayed when the justifications are shown" or "all hidden when justifications are shown".
• The iset.mm database is now an easily-selected option for our intuitionistic friends.

Oh, this hints at a nomenclature change I'm thinking of doing in the guide. I now think I should say that a "proof consists of many steps", and each step includes an id, step type (H/P/G), justification (hyp and ref), and statement. If you have thoughts about that nomenclature change in the guide, please comment here: metamath/lamp-guide#62

[david-a-wheeler]

So after you implement #56 and it's adequately reliable to your satisfaction, I recommend you ship it as version 11. Announce the results to the world, and move the other proposed items to version 12.

Again, this is all up to you. But there's no reason to bottle up the goodness. There will always be something more you could add :-).

[david-a-wheeler]

Also, while there are many awesome proposals in the current v11 list, there are two larger capabilities, either of which might make sense for version 12:

• Undo/redo. Implement undo/redo #33 - this is important, because once added, users will be far less fearful about experimenting.
• Full syntactic unification Proposal: Allow bottom-up prover to unify work variables more broadly (long-term) #77 - this is probably going to be a game-changer in terms automatically finding proofs. It's probably also necessary to convince mmj2 users to consider using it instead (since mmj2 has it).

Once you implement either one I think you should cut another release. Either one of those, by themselves, is helpful enough that users would immediately want it.

[expln]

I'm a believer in "release early, release often". The sooner you release, the sooner you get feedback on what's important (and what isn't).

You are right. I like this idea.

I have one request before v11 is released, if I may request it and it doesn't take too long:
Enable visualization per justification, instead of a global setting #56

Sure, that should not take too long. I will include it into v11.

here at the headline items that I see

Almost everything you listed is ready. I agree with "release early, release often". So I will restructure my v11 list based on your response.

there are two larger capabilities, either of which might make sense for version 12

Yes, undo/redo should be implemented ASAP. As of "unify work variables more broadly", I also consider it as a an urgent change, but it may take some time because it may require to change some core functions. So you may see some other changes being implemented between "undo/redo" and "unify work variables more broadly".

Thanks for your extensive feedback on the roadmap!

Soon you may see I deploy new features to dev without detailed explanations in the corresponding issues - this is because I prefer to code in the beginning of the day and write comments in the evening. So, don't interpret this as I don't want to explain what I am doing, that's just my way of optimizing work :)

[david-a-wheeler]

Yes, undo/redo should be implemented ASAP. As of "unify work variables more broadly", I also consider it as a an urgent change, but it may take some time because it may require to change some core functions. So you may see some other changes being implemented between "undo/redo" and "unify work variables more broadly".

That makes sense, that's what I expect will happen.

Thanks for your extensive feedback on the roadmap!

Sure! Thanks for this cool tool! I'm sure I'll have many more nits to report, but I wouldn't bother if it wasn't cool.

Soon you may see I deploy new features to dev without detailed explanations in the corresponding issues - this is because I prefer to code in the beginning of the day and write comments in the evening. So, don't interpret this as I don't want to explain what I am doing, that's just my way of optimizing work :)

Sure! Thanks for letting me know. It clearly works for you :-).

[david-a-wheeler]

Wow! The latest improvements in the development version are stunning, especially on a smartphone. The new options (to make things fit on the screen better) make it much nicer on a smartphone, I even got to show the development version to a mathematician friend using my phone. I also like the ability to see the justification (ref and hyps) for each step; now it meets (and even exceeds) mmj2 in this area.

I can't figure out how to get visualizations now from within the editor. I presume that's "work in progress". There are endless possible refinements, but that's the only blocker for me right now. I can't wait to see this wrapped up and released!

[expln]

I am glad you liked it!

how to get visualizations now from within the editor

mm-lamp is able to show visualizations only for steps marked with a green checkmark or with an orange ~. When you have such a step you may click on its step type (P or G letters) or on its label. If justification is always shown, then the visualization will be opened right upon clicking. If justification is not always shown, then the clicking will open the justification first, and you will see a new icon button there which opens visualization. If you disabled showing labels and step types then you cannot open visualizations.

I will explain this and all my other recent changes in more detail later today.

[david-a-wheeler]

When you have such a step you may click on its step type (P or G letters) or on its label. If justification is always shown, then the visualization will be opened right upon clicking.

On a smartphone I have justifications always displayed. When I touch the green checkmark, I usually see the compressed proof, but sometimes I see the visualization. It seems random which happens.

[expln]

The compressed proof is opened when you touch the green checkmark. The visualization is opened when you touch the label or the step type. The green checkmark and the label are located very close. I think you may be touching the green check mark unintentionally instead of the label. To open visualization, try to touch the label but more on the right side. Then you will be touching the label or the step type, but both of them will open the visualization.

[david-a-wheeler]

Ah! I was doing many experiments on my smartphone, where tooltips cannot be seen.

Okay, here is what I think version 11 is doing (per comments above, tooltips, and experimentation):

• I presume click==tap and long-click==long-tap throughout.
• Checkmark: Click = show compressed proof; Long-click no different
• Label: click=visualization IF there's a green checkmark (must use unification to get that), long-click = edit
• Step type: click=show/hide justification (when they aren't always shown), long-click=edit step type via dropdown
• Justification: Click = edit, long-click no different. Doing this always removes all checkmarks and thus disables enabling visualizations, even when the result is unchanged (e.g., via cancel).
• Statement: Click = edit, long-click = select statement fragment

The functionality is awesome, including controlling what's displayable.

One problem I had in testing: When a justification is edited & then cancelled (or in other ways not edited), all checkmarks disappear & that disables visualizations. This led me to think that enabling visualizations was unreliable, because it's really easy to edit & cancel, thinking "nothing changed" but as a side-effect the visualizations got disabled.

More generally, the mapping seems inconsistent. Editing is sometimes a long click and is sometimes a short click, depending on the field. I think that in an editor (at least) a "simple click" should always cause an edit if an edit makes sense, as that would be more consistent. The long-click would be used for some other behavior (like fragment selection). So I suggest this default mapping:

• Checkmark: Click = show compressed proof; Long-click visualization toggle
• Label: click=edit; long-click=visualization toggle
• Step type: click=edit (step type via dropdown), long-click: show/hide justification
• Justification: Click = edit, long-click visualization toggle.
• Statement: Click = edit, long-click = select statement fragment

I also suggest that if "visualization toggle" tries to reveal a hidden visualization, automatically invoke unification if there isn't a green checkmark. After all, if the user requested it, the user presumably thinks it's possible & we should try to achieve it.

Finally, as hinted above, it'd be better if editing the justification field, but not changing it, didn't remove green checkmarks. Noticing "nothing has changed", and doing nothing as a result, would eliminate a subtle UI trap.

I note this now because I want to talk about the UI in my video, so if the default mappings are going to get changed I'd like that to happen sooner :-).

In the longer term it'd be nice if touchscreens could see tooltips (e.g., show tooltips during a long-press, and if a user moves off the element it won't count as a long-press). Maybe tooltips coudl be revealed on "touch-down" and disappear on "touch-up"? In any case, supporting tooltips on touchscreens sounds like a "future version" capability sadly :-).

[expln]

The functionality is awesome, including controlling what's displayable.

Thank you!

More generally, the mapping seems inconsistent.

I created a separate issue to discuss this - #97

I also suggest that if "visualization toggle" tries to reveal a hidden visualization, automatically invoke unification if there isn't a green checkmark. After all, if the user requested it, the user presumably thinks it's possible & we should try to achieve it.

Good idea, I created an issue for that #96

In the longer term it'd be nice if touchscreens could see tooltips (e.g., show tooltips during a long-press, and if a user moves off the element it won't count as a long-press). Maybe tooltips coudl be revealed on "touch-down" and disappear on "touch-up"? In any case, supporting tooltips on touchscreens sounds like a "future version" capability sadly :-).

I saw you posted a comment #23 (comment) with some hint on how React allows to easily implement this. I will check it. Thanks!

One problem I had in testing: When a justification is edited & then cancelled (or in other ways not edited), all checkmarks disappear & that disables visualizations.
Finally, as hinted above, it'd be better if editing the justification field, but not changing it, didn't remove green checkmarks. Noticing "nothing has changed", and doing nothing as a result, would eliminate a subtle UI trap.

I agree, this causes some inconvenience. This was the easiest way for me to ensure the UI doesn't show stale information. But for sure it can be and should be improved. I created a corresponding issue - #95

[expln]

@david-a-wheeler

Continuing conversation from #107 (comment)

I don't know of any other issues that prevent a v11 release. I would love to see undo/redo and full unification (high priority for me), but I think you should not delay v11 for those. What you have is already awesome.

I found one bug. It happens when a statement may be proved by two different justifications.
If one justification is specified in the editor, but the prover finds another then the one in the editor is marked as incorrect.
This happens because the prover stops searching as soon as it finds any valid proof.
The fix is not complex. I want to include it into v11.

I will put undo/redo and full unification into the next version. Not necessarily v12, but I understand their importance, so I will work on them with the highest priority.
I already have more or less clear plan how to do both of these items.

I plan to release v11 by the end of this week. Usually I don't have enough time during working days, but I hope I will have enough time on the weekend.

FYI: I demoed v11 to my daughter, who isn't normally very interested in math, but she found the visualizations intriguing and started asking questions. They really are a big help in explaining what's going on.

That's nice! I am very glad that mm-lamp becomes useful :)

[david-a-wheeler]

The truly infinite thing in the universe is user feature requests, so I've created many :-).

However, you've long since exceeded the bar of "is this version of the tool better than it was before". So I think whenever you decide to release it'll be great. The updated guide is generally ready; there are a few small things I intend to do this weekend as well, but don't wait for me!

[expln]

Thanks for your efforts to not leave me out of feature requests :)

Yeah, I still plan to release it by the end of the week. There always will be some discrepancies between the app and the guide. But we will fix them and... make new ones :)

[david-a-wheeler]

There always will be some discrepancies between the app and the guide. But we will fix them and... make new ones :)

I look forward to all the discrepancies you create because of new additions in the tool :-).

[david-a-wheeler]

You've obviously made the decision to release - thank you!

I will close this comment, as it has been overcome by events.