search

KeYProject / key

KeY Theorem Prover for Deductive Java Verification
https://key-project.org
Other
41 stars 24 forks source link

Get rid of experimental flag using more fine-grained flags #3370

Closed wadoon closed 8 months ago

wadoon commented 9 months ago

Motivation

The experimental flag is a bad idea. You cannot control which feature you want to activate. Instead, you are getting a full load of functionality one activated. This PR allows you to have more fine-grained feature flags, with a well-defined backward behavior for --experimental.

This PR was created for #3022 to activate the labels w/o activated all of the other untested functions.

Intended Change

Type of pull request

Ensuring quality

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

unp1 commented 9 months ago

Thanks a lot! The code looks nice.

One bug I encountered is the following exception: Exception in thread "AWT-EventQueue-0" java.lang.ClassCastException: class javax.swing.JLabel cannot be cast to class javax.swing.JPanel (javax.swing.JLabel and javax.swing.JPanel are in module java.desktop of loader 'bootstrap') at de.uka.ilkd.key.gui.settings.SettingsUi.lambda$setSettingsProvider$2(SettingsUi.java:165) at java.base/java.util.stream.ReferencePipeline$3$1.accept(ReferencePipeline.java:197) at java.base/java.util.ArrayList$ArrayListSpliterator.forEachRemaining(ArrayList.java:1708) at java.base/java.util.stream.ReferencePipeline$Head.forEach(ReferencePipeline.java:762) at java.base/java.util.stream.ReferencePipeline$7$1.accept(ReferencePipeline.java:276) at java.base/java.util.LinkedList$LLSpliterator.forEachRemaining(LinkedList.java:1249) at java.base/java.util.stream.AbstractPipeline.copyInto(AbstractPipeline.java:509) at java.base/java.util.stream.AbstractPipeline.wrapAndCopyInto(AbstractPipeline.java:499) at java.base/java.util.stream.ReduceOps$ReduceOp.evaluateSequential(ReduceOps.java:921) at java.base/java.util.stream.AbstractPipeline.evaluate(AbstractPipeline.java:234) at java.base/java.util.stream.ReferencePipeline.reduce(ReferencePipeline.java:662) at java.base/java.util.stream.ReferencePipeline.max(ReferencePipeline.java:698) at de.uka.ilkd.key.gui.settings.SettingsUi.setSettingsProvider(SettingsUi.java:169) at de.uka.ilkd.key.gui.settings.SettingsDialog.setSettingsProvider(SettingsDialog.java:70) at de.uka.ilkd.key.gui.settings.SettingsManager.createDialog(SettingsManager.java:125) at de.uka.ilkd.key.gui.settings.SettingsManager.showSettingsDialog(SettingsManager.java:116)

To reproduce:

  1. Start KeY with --experimental
  2. Options > Show Settings
  3. Exception
unp1 commented 9 months ago

The second exception is: java.lang.ClassCastException: class java.lang.Boolean cannot be cast to class java.lang.String (java.lang.Boolean and java.lang.String are in module java.base of loader 'bootstrap') at java.base/java.util.Properties.store0(Properties.java:937) at java.base/java.util.Properties.store(Properties.java:908) at de.uka.ilkd.key.settings.ProofIndependentSettings.saveSettings(ProofIndependentSettings.java:125) at de.uka.ilkd.key.settings.ProofIndependentSettings.lambda$new$0(ProofIndependentSettings.java:55) at java.desktop/java.beans.PropertyChangeSupport.fire(PropertyChangeSupport.java:343) at java.desktop/java.beans.PropertyChangeSupport.firePropertyChange(PropertyChangeSupport.java:335) at java.desktop/java.beans.PropertyChangeSupport.firePropertyChange(PropertyChangeSupport.java:268) at de.uka.ilkd.key.settings.AbstractSettings.firePropertyChange(AbstractSettings.java:47) at de.uka.ilkd.key.settings.AbstractPropertiesSettings$DefaultPropertyEntry.set(AbstractPropertiesSettings.java:235) at de.uka.ilkd.key.settings.ProofCachingSettings.setDispose(ProofCachingSettings.java:64)

To reproduce:

  1. Start KeY (normal mode)
  2. Select some Feature Flags and press apply
  3. Exception
wadoon commented 9 months ago

Bugs repaired.

unp1 commented 9 months ago

Thanks, the settings are now saved and I do not get the previously mentioned exceptions.

I experience now the following two issues:

wadoon commented 9 months ago
  • Activating the flags work (i.e. the checkbox is marked and the mark seems to be saved), but the extension seem not to be activated (before and after restart), e.g. activating the Test UI Bundle does not show the Test menu

Not all features are "hot" reloadable. I made the "Run All Proofs" menu item hot reload now.

I also added a flag which says if a feature requires a restart. The settings dialogue gives an information message if the state of a non-hot-loadable feature has taken place. (Note this does not scale: If there is a different settings panel which also wants to give a message on settings application we would have two message dialogs. But for now, this solution is valid.)

codecov[bot] commented 9 months ago

Codecov Report

Attention: 76 lines in your changes are missing coverage. Please review.

Comparison is base (92b25ea) 37.98% compared to head (f925398) 37.97%.

Files Patch % Lines
...java/de/uka/ilkd/key/settings/FeatureSettings.java 27.02% 52 Missing and 2 partials :warning:
...ka/ilkd/key/settings/ProofIndependentSettings.java 18.18% 8 Missing and 1 partial :warning:
.../ilkd/key/settings/AbstractPropertiesSettings.java 52.94% 8 Missing :warning:
...ilkd/key/settings/ProofIndependentSMTSettings.java 33.33% 4 Missing :warning:
...in/java/de/uka/ilkd/key/settings/ViewSettings.java 0.00% 1 Missing :warning:
Additional details and impacted files ```diff @@ Coverage Diff @@ ## main #3370 +/- ## ============================================ - Coverage 37.98% 37.97% -0.01% - Complexity 17027 17035 +8 ============================================ Files 2059 2060 +1 Lines 126051 126146 +95 Branches 21285 21292 +7 ============================================ + Hits 47883 47910 +27 - Misses 72285 72351 +66 - Partials 5883 5885 +2 ```

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

wadoon commented 9 months ago

Exception in thread "AWT-EventQueue-0" java.lang.ClassCastException: class javax.swing.JLabel cannot be cast to class javax.swing.JPanel (javax.swing.JLabel and

This is an old error, I have fixed multiple times.

The API says that a settings provider provides a JComponent, someone added a cast to JPanel, which fails for plugins enabled under --experimental.

It is a good example why experimental flag or feature flags in general may not be good design choice.

wadoon commented 9 months ago

[13:25:38.759] ERROR SimpleSettingsPanel - Cannot invoke "javax.swing.JSpinner.setForeground(java.awt.Color)" because "this.maxField" is null

A new one! I did not understood why the validator was called for a JSpinner before the class was completely created. I added a guard.

unp1 commented 8 months ago

Thanks! I tested it and it now works without any exceptions. Could you just quickly check my review remark and let me know whether it is valid or not. I will then approve the PR.

unp1 commented 8 months ago

Thanks. I approved the PR. Before merging could you check the unresolved question whether that issue is valid or intended.