Get rid of experimental flag using more fine-grained flags

[wadoon]

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

• A new settings FeatureSettings which is basically a set string (features to be activated)
• A set of feature flags in places where Main.isExperimentalMode() were requested.
• A settings panel
  
• A behavior for --experimental, activating all features.
• Feature flags are stored and read in the proof-independent settings
• Changes in feature flags can have an effect depending on the feature

Type of pull request

• New feature (non-breaking change which adds functionality)
• There are changes to the (Java) code
• Other: The effect of CLI parameter --experimental.

Ensuring quality

• I made sure that introduced/changed code is well documented (javadoc and inline comments).

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

[unp1]

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]

Nice. There are two exceptions I get (described as comments in the PR), whcih should be fixed before merging.

[unp1]

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]

Bugs repaired.

[unp1]

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

I experience now the following two issues:

• 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
• starting with --experimental throws the exceptions

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)

also I get the following log error when starting KeY

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

[wadoon]

• 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]

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 ⚠️
...ka/ilkd/key/settings/ProofIndependentSettings.java	18.18%	8 Missing and 1 partial ⚠️
.../ilkd/key/settings/AbstractPropertiesSettings.java	52.94%	8 Missing ⚠️
...ilkd/key/settings/ProofIndependentSMTSettings.java	33.33%	4 Missing ⚠️
...in/java/de/uka/ilkd/key/settings/ViewSettings.java	0.00%	1 Missing ⚠️

Additional details and impacted files

@@             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     

☔ View full report in Codecov by Sentry.
📢 Have feedback on the report? Share it here.

[wadoon]

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]

[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]

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]

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