Open tobias-rnh opened 5 months ago
Attention: Patch coverage is 0%
with 2 lines
in your changes missing coverage. Please review.
Project coverage is 38.16%. Comparing base (
0ebb8b5
) to head (8f4ee86
). Report is 5 commits behind head on main.
Files | Patch % | Lines |
---|---|---|
.../src/main/java/de/uka/ilkd/key/nparser/KeyAst.java | 0.00% | 2 Missing :warning: |
:umbrella: View full report in Codecov by Sentry.
:loudspeaker: Have feedback on the report? Share it here.
@tobias-rnh We should work on this. Remind me at our next meeting.
Maybe add a label to the UI that show the current selected prove.
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.
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?
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. ...)
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.
(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).
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
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.
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?
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.
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.
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.
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.
I think Tobias' warning implementation (as discussed) looks like the right thing to me.
I also agree with Mattias and Tobias
My manual tests work and I encountered no issues.
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
Ensuring quality
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.![old_options](https://github.com/KeYProject/key/assets/93993502/f92d9d83-0357-4a38-aa32-c906add20d84)
Now, this is not the case anymore since the options are now contained in a unified settings dialog.![new_options](https://github.com/KeYProject/key/assets/93993502/a75e9561-3d0e-4394-b7da-fcae1f69ef69)
Before, even when a proof was loaded, there was still a header shown in the taclet options stating that there was no proof loaded.![no_proof_header_still_visible](https://github.com/KeYProject/key/assets/93993502/ed96adbe-54d2-4d85-995d-80d2fbfc2bfd)
This is fixed now.![no_proof_header_invisible](https://github.com/KeYProject/key/assets/93993502/eaf9ba6e-0f35-410c-abe0-c79265393d8b)
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.![active_taclet_settings_old](https://github.com/KeYProject/key/assets/93993502/5b2011a8-3c18-4701-8fc9-84be6f20fc2c)
Now, the path to the taclet options has been changed to reflect the new way to change taclet options.![active_taclet_settings_new](https://github.com/KeYProject/key/assets/93993502/e4508eda-1c83-4ea1-9a92-d1643d9deb1f)
The contributions within this pull request are licensed under GPLv2 (only) for inclusion in KeY.