HacKeYthon: Improved Taclet Options

[tobias-rnh]

Related Issue

This pull request addresses #3414.

Intended Change

Remove the old dialog to change taclet options. Taclet options can now be accessed through the new unified settings dialog ("Options" -> "Show Settings" -> "Taclet Options"). Additionally, a bug was fixed where a warning header did not disappear, even after a proof was loaded.

As of now, the radio buttons selected are still only the default ones and not the options selected in the current proof.

Type of pull request

• [x] Bug fix (non-breaking change which fixes an issue)
• [ ] Refactoring (behaviour should not change or only minimally change)
• [ ] New feature (non-breaking change which adds functionality)
• [x] Breaking change (fix or feature that would cause existing functionality to change) Old Taclet Options are not accessible through the options tab directly anymore
• [x] There are changes to the (Java) code
• [ ] There are changes to the taclet rule base
• [ ] There are changes to the deployment/CI infrastructure (gradle, github, ...)
• [ ] Other:

Ensuring quality

• [x] I made sure that introduced/changed code is well documented (javadoc and inline comments). Really only inline comments
• [ ] I made sure that new/changed end-user features are well documented (https://github.com/KeYProject/key-docs).
• [ ] I added new test case(s) for new functionality.
• [x] I have tested the feature as follows: I manually inspected the menus and how they behaved before and after loading a proof
• [ ] I have checked that runtime performance has not deteriorated.

Additional information and contact(s)

As a reference, how things were looking before and now:

The options tab previously had an entry to get to taclet options directly.

Now, this is not the case anymore since the options are now contained in a unified settings dialog.

Before, even when a proof was loaded, there was still a header shown in the taclet options stating that there was no proof loaded.

This is fixed now.

At "Proof"->"Show Active Taclet Options" you can see the active taclet options with a path given at the bottom to change the taclet options.

Now, the path to the taclet options has been changed to reflect the new way to change taclet options.

The contributions within this pull request are licensed under GPLv2 (only) for inclusion in KeY.

[codecov[bot]]

Codecov Report

Attention: Patch coverage is 0% with 2 lines in your changes missing coverage. Please review.

Project coverage is 38.16%. Comparing base (6126701) to head (79eff2d). Report is 8 commits behind head on main.

Files	Patch %	Lines
.../src/main/java/de/uka/ilkd/key/nparser/KeyAst.java	0.00%	2 Missing :warning:

Additional details and impacted files

@@            Coverage Diff            @@
##               main    #3433   +/-   ##
=========================================
  Coverage     38.16%   38.16%           
  Complexity    17222    17222           
=========================================
  Files          2109     2109           
  Lines        127644   127644           
  Branches      21458    21458           
=========================================
  Hits          48710    48710           
  Misses        72944    72944           
  Partials       5990     5990           

:umbrella: View full report in Codecov by Sentry.
:loudspeaker: Have feedback on the report? Share it here.

[Drodt]

@tobias-rnh We should work on this. Remind me at our next meeting.

[wadoon]

Maybe add a label to the UI that show the current selected prove.

[wadoon]

As a reminder, the taclet options are now updatable after parsing due to the new parser (and the later evaluation of the taclet options), but for soundness reasons, we should only allow this for single-noded proofs.

[mattulbrich]

As a reminder, the taclet options are now updatable after parsing due to the new parser (and the later evaluation of the taclet options), but for soundness reasons, we should only allow this for single-noded proofs.

I don't think I understand that. How can the taclet options be changed after the problem has been parsed/loaded? What is a single-noded proof?

[mattulbrich]

I seem to remember that the taclet options were sometimes set arbitrarily and neither to the current values nor to the ones to be loaded in the future. Perhaps that's fixed now.

I wonder what values I see there: Those for the upcoming load process, right?

I would really like to have a note with a :warning: sign indicating that the current version of the taclet options is not the ones set for the currently loaded proof. A link/hint to the current settings would be nice then.

(That window would deserve some update too. ...)

[mattulbrich]

Why is the menu item called "Show Settings" and not "Settings"; one can change them after all. Suggest to rename it while we are at it.

[mattulbrich]

(That window would deserve some update too. ...)

I took care of that, merging the two ways to show the currently active taclet options (read-only).

[mattulbrich]

The taclet option pane in the settings dialog was very bad to get a good overview. I refactored it a bit and it looks now as follows:

I hope this fits our needs. /cc @wadoon

[wadoon]

As a reminder, the taclet options are now updatable after parsing due to the new parser (and the later evaluation of the taclet options), but for soundness reasons, we should only allow this for single-noded proofs.

I don't think I understand that. How can the Taclet options be changed after the problem has been parsed/loaded? What is a single-noded proof?

The old parser parsed only these Taclet sections where the Taclet options are positively evaluated. The new parser parses and builds every Taclet. Inactive Taclets are removed in the last step within InitConfig. There is one reason, why we should allow to re-evaluate the set of active/inactive Taclets and update the Taclet indices accordingly. That reason is that Taclets might have been applied, which are not active anymore. For a single-noded proof (a proof with only a single node: the root) that situation is never valid.

[tobias-rnh]

I have now changed the proof tab to only contain the entry for the active settings and not for the taclets. When no proof is loaded, there are no default values displayed as proof-dependent settings. Instead, it just informs the user that no proof is loaded.

I have also moved the node for term labels to the proof-independent settings, as the previous code got these settings from independentSettings but still added the node to proof-dependent settings:

Settings termLabelSettings = independentSettings.getTermLabelSettings();
proofSettingsNode.add(generateTableNode("Term Labels", termLabelSettings));

There is also another bug: After starting KeY and before loading a proof, I am told and can not change the taclet options as no proof is loaded. If I load a proof, abandon it (Proof > Abandon Proof) and now open the options, I see the following:

The radio buttons are still functional, and after changing some taclet options and reloading the proof, the changed taclet options can be seen under all active settings. But the dialog still says that no proof is loaded and I should not be able to change taclet options. Do you have any wishes how this should be resolved?

[wadoon]

That is not a bug, it is a feature.

The problem is, that the Taclet options are defined in the KeY files, and you have to read them to offer a dialog to set them. And if all the proofs are abondoned, you still know the Taclet options and you can set them because you normally need to reload any ways.

[mattulbrich]

That is not a bug, it is a feature.

The problem is, that the Taclet options are defined in the KeY files, and you have to read them to offer a dialog to set them. And if all the proofs are abondoned, you still know the Taclet options and you can set them because you normally need to reload any ways.

Well, bug or not, it seems inconsistent: The warning tells you cannot see and change things, yet the menu shows you can change things. So ... we should either deactivate the warning or disable the dialogue at that point.

[tobias-rnh]

Now, when a taclet option is changed, a warning icon is displayed. Hovering over it (or the title), a tooltip shows the option that is active in the currently loaded proof.

For consistency when no proof is loaded, the taclet options may not be changed.

[wadoon]

Well, bug or not, it seems inconsistent: The warning tells you cannot see and change things, yet the menu shows you can change things. So ... we should either deactivate the warning or disable the dialogue at that point.

Disabling the dialog seems to be a bad option: A user who wants to be safe, and that the next proof is loaded with the right Taclet options would close all the proofs, set the options, and reload.

If we really want an improvement in user experience, we should rather re-think our way of dealing with Taclet options.

They are not dynamically used as they could be. In nearly all of the cases, only the built-in Taclet base is using them.

[mattulbrich]

I think Tobias' warning implementation (as discussed) looks like the right thing to me.

[Drodt]

I also agree with Mattias and Tobias

[Drodt]

My manual tests work and I encountered no issues.

[WolframPfeifer]

While I am ok with the status quo after this PR, I agree with @wadoon that we should rework the way how our taclet settings work in the future:

1. In my opinion, we could safely remove the feature to add taclet options in user-defined .key files (has this ever been used by somebody?).
2. With 1, we could parse the taclet options (not the taclets itself!) directly at the start of KeY (or at least as soon as the option dialog is opened). This would then allow the workflow mentioned above by @wadoon (which makes sense from the user's perspective): Closing all proofs, setting taclet options, starting the next proof with the just selected options.
3. As mentioned by @unp1 in a recent meeting: Loading a .key file with settings specified silently (!) overwrites the settings the user has selected in the GUI, so an idea might to ask which of those should be used or at least give a warning.