Additions for later versions - discussion

[david-a-wheeler]

I'm really looking forward to the version 11 release. It seems like a good time to start discussing version 12.

While what's in version 12 is up to @expln, I figure I can provide feedback :-).

Here is the current list by @expln of milestone plans for version 12 (v12).

Here are my top priorities - @expln let me know if this information is useful.

1. Implement undo/redo #33 Alg - once this is implemented, people will be less afraid to experiment.
2. Proposal: Allow bottom-up prover to unify work variables more broadly (long-term) #77 Alg - this is key for gaining parity with mmj2 and simplifies use. This isn't currently on the v12 list. I totally understand if that's deferred, but I think this one is key. I think there are two parts to this: (1) full unification during global substitution (the "substitution" icon) - I think this should always be the case. (2)) full unification during bottom-up search - I think this should be an option for bottom-up search, but also supporting the current matching algorithm.
3. By default ignore any statements marked (New usage is discouraged.) #31 Alg - proofs generally won't be accepted if they incorrectly include discouraged statements, best to nip this problem early
4. By default don't use discouraged syntax nor later syntax #108 - don't use discouraged syntax by default.

And my top desirata (but not as important as the ones above):

1. Add "paste" to edit fragment selector dialogue (easy win!) #42 UI - this is helpful to all, especially for longer expressions. However, it's especially helpful on smartphones - the "paste" is awkward, and keyboards are usually soft keyboards.
2. Automate creating of labels for hypotheses #32 UI - I expect this to be easy to implement, and it's a nice touch. It also quietly helps users avoid creating bogus hypotheses labels.
3. Open proof explorer by clicking refs in justifications #99 UI
4. Proposal (low priority): Make tooltips work on smartphones (in addition to larger displays) #23 UI
5. In visualizations, don't repeat if conclusion is all constants (low priority) #115 UI - more because I expect this to be simple to implement, if (stmt.filter(variable).exists) { ... show the mapping and final statement }.

[david-a-wheeler]

@expln - your priorities may be different, but I thought you might find it useful to hear what I would really like to see.

[expln]

The first 4 items agree with my point of view. Looks like the remaining items also agree. I've already started working on undo/redo. I gave this short response to show that I didn't miss this issue :) I will analyze all the open issues and reply with my priorities, but in some time.

[expln]

@david-a-wheeler

Undo/redo is completed. I agree that the next most important item should be the full unification. I will start working on it. But I am planning to spend few days on implementing other useful things which should not take a lot of time like automatic labeling for hypotheses, disabling parentheses autocompletion etc. I am going to re-read all the available issues and pick what is simple.

[david-a-wheeler]

Congratulations! I think this undo/redo functionality is a a big deal, it'll mean that users can experiment with confidence.

Good luck on the other items! Your plan makes 100% sense to me.

You're more than welcome to make announcements to the Metamath mailing list yourself, but if you'd like me to make one on your behalf, let me know.

[expln]

Thanks! If you wish you may make an announcement :)

[expln]

Thank you for posting the announcement!

[expln]

@david-a-wheeler

Some of the issues from the "second" priority group are implemented in version 15.

I propose to rename this issue to something like "Discussion of priorities" or something like that since the version 12 is no longer relevant.