Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Jump to bottom

Overhaul of the Configuration #3031

Merged
merged 15 commits into from
Apr 6, 2023
Merged

Overhaul of the Configuration #3031

merged 15 commits into from
Apr 6, 2023

Conversation

wadoon
Copy link
Member

@wadoon wadoon commented Feb 7, 2023 •
edited
Loading

The KeY settings are in a hysterical and historic shape.

This PR tries to homogenize the settings to Java POJOs using the JavaBeans standard and mechanism. The measurement include:

  • Introduction of Getter/Setter
  • Removal of SettingsListener in favour of PropertyChangeListener
    (You can listen on individual configuration changes.)

Most of the changes results from dependencies to the SettingsListener, or the change of field-access to getter and setter.

A next PR step will change the settings language in KeY files to a custom type-safe backward
compatible language.

@wadoon
Make everything setting a POJO
37ca07f
@wadoon
Merge branch 'master' into weigl/config
331aa01 
* master: (301 commits)
  Spotless: Don't join manually split lines
  Fixed two more files with broken comments (KeYProject#1710)
  manual formatting corrections (not for recoder, tests, and resources)
  applied spotless rules to .key files
  applied spotless rules to Java sources
  define KeY code style, remove options not supported by Eclipse formatter, enable spotless toggles, removed license header from spotless configuration, removed indentation config for .key files (did not really work)
  Fix Jenkins master script after !559
  Temporarily disable reloading sort.proof.gz because of KeYProject#1720
  ChoiceExpr: En-/Disabling taclets/goal templates using boolean expression
  Split `testRunAllProofs` into two tasks
  Fast fix: Do not run pipeline defined by the Jenkinsfile on "Master" worker
  Focus first cell in the taclet instantiation dialog on open
  Close more dialogs on escape press and code deduplication
  Allow ApplyTacletDialog to be closed by pressing Escape
  Fix getMainWindow infinite recursion
  Fix Exception when parsing "<unknown>" URL on Windows
  Disable exploration tree updates when disabled
  Remove space from taclet proof save file name
  Allows to have an expression on the lhs in a set statement. Hence,
  further logging commands fixed
  ...

# Conflicts:
#	key/key.core.example/src/main/java/org/key_project/Main.java
#	key/key.core.proof_references/src/test/java/de/uka/ilkd/key/proof_references/testcase/AbstractProofReferenceTestCase.java
#	key/key.core.symbolic_execution.example/src/main/java/org/key_project/example/Main.java
#	key/key.core.symbolic_execution/src/main/java/de/uka/ilkd/key/symbolic_execution/util/SymbolicExecutionUtil.java
#	key/key.core.symbolic_execution/src/test/java/de/uka/ilkd/key/symbolic_execution/testcase/AbstractSymbolicExecutionTestCase.java
#	key/key.core.symbolic_execution/src/test/java/de/uka/ilkd/key/symbolic_execution/testcase/TestSymbolicExecutionTreeBuilder.java
#	key/key.core.symbolic_execution/src/test/java/de/uka/ilkd/key/symbolic_execution/testcase/TestSymbolicLayoutExtractor.java
#	key/key.core.symbolic_execution/src/test/java/de/uka/ilkd/key/symbolic_execution/testcase/po/TestFunctionalOperationContractPO.java
#	key/key.core.symbolic_execution/src/test/java/de/uka/ilkd/key/symbolic_execution/testcase/po/TestProgramMethodPO.java
#	key/key.core.symbolic_execution/src/test/java/de/uka/ilkd/key/symbolic_execution/testcase/strategy/TestExceptionBreakpointStopConditionCaughtOrUncaught.java
#	key/key.core.symbolic_execution/src/test/java/de/uka/ilkd/key/symbolic_execution/testcase/strategy/TestExceptionBreakpointStopConditionWithHitCount.java
#	key/key.core.symbolic_execution/src/test/java/de/uka/ilkd/key/symbolic_execution/testcase/strategy/TestExceptionBreakpointStopConditionWithSubclasses.java
#	key/key.core.symbolic_execution/src/test/java/de/uka/ilkd/key/symbolic_execution/testcase/strategy/TestJavaWatchpointStopConditionWithHitCount.java
#	key/key.core.symbolic_execution/src/test/java/de/uka/ilkd/key/symbolic_execution/testcase/strategy/TestKeYWatchpointGlobalVariablesOnSatisfiable.java
#	key/key.core.symbolic_execution/src/test/java/de/uka/ilkd/key/symbolic_execution/testcase/strategy/TestKeYWatchpointGlobalVariablesOnTrueWithHitCount.java
#	key/key.core.symbolic_execution/src/test/java/de/uka/ilkd/key/symbolic_execution/testcase/strategy/TestKeYWatchpointMethodsOnSatisfiable.java
#	key/key.core.symbolic_execution/src/test/java/de/uka/ilkd/key/symbolic_execution/testcase/strategy/TestLineBreakpointStopConditionSimpleWithConditions.java
#	key/key.core.symbolic_execution/src/test/java/de/uka/ilkd/key/symbolic_execution/testcase/strategy/TestLineBreakpointStopConditionSimpleWithHitCount.java
#	key/key.core.symbolic_execution/src/test/java/de/uka/ilkd/key/symbolic_execution/testcase/strategy/TestLineBreakpointStopConditionSimpleWithLoopInvariant.java
#	key/key.core.symbolic_execution/src/test/java/de/uka/ilkd/key/symbolic_execution/testcase/strategy/TestMethodBreakpointWithConditions.java
#	key/key.core.symbolic_execution/src/test/java/de/uka/ilkd/key/symbolic_execution/testcase/strategy/TestMethodBreakpointWithHitCount.java
#	key/key.core.symbolic_execution/src/test/java/de/uka/ilkd/key/symbolic_execution/testcase/strategy/TestStepOverSymbolicExecutionTreeNodesStopCondition.java
#	key/key.core.symbolic_execution/src/test/java/de/uka/ilkd/key/symbolic_execution/testcase/strategy/TestStepReturnSymbolicExecutionTreeNodesStopCondition.java
#	key/key.core.symbolic_execution/src/test/java/de/uka/ilkd/key/symbolic_execution/testcase/util/TestSymbolicExecutionUtil.java
#	key/key.core.testgen/src/main/java/de/uka/ilkd/key/settings/TestGenerationSettings.java
#	key/key.core.testgen/src/main/java/de/uka/ilkd/key/smt/testgen/AbstractTestGenerator.java
#	key/key.core.testgen/src/main/java/de/uka/ilkd/key/testgen/ModelGenerator.java
#	key/key.core.testgen/src/test/java/de/uka/ilkd/key/testcase/smt/ce/SMTTestSettings.java
#	key/key.core/src/main/java/de/uka/ilkd/key/java/recoderext/JMLTransformer.java
#	key/key.core/src/main/java/de/uka/ilkd/key/proof/Proof.java
#	key/key.core/src/main/java/de/uka/ilkd/key/proof/init/InitConfig.java
#	key/key.core/src/main/java/de/uka/ilkd/key/proof/io/AutoSaver.java
#	key/key.core/src/main/java/de/uka/ilkd/key/settings/AbstractPropertiesSettings.java
#	key/key.core/src/main/java/de/uka/ilkd/key/settings/ChoiceSettings.java
#	key/key.core/src/main/java/de/uka/ilkd/key/settings/GeneralSettings.java
#	key/key.core/src/main/java/de/uka/ilkd/key/settings/LemmaGeneratorSettings.java
#	key/key.core/src/main/java/de/uka/ilkd/key/settings/NewSMTTranslationSettings.java
#	key/key.core/src/main/java/de/uka/ilkd/key/settings/ProofDependentSMTSettings.java
#	key/key.core/src/main/java/de/uka/ilkd/key/settings/ProofIndependentSMTSettings.java
#	key/key.core/src/main/java/de/uka/ilkd/key/settings/Settings.java
#	key/key.core/src/main/java/de/uka/ilkd/key/settings/SettingsListener.java
#	key/key.core/src/main/java/de/uka/ilkd/key/settings/StrategySettings.java
#	key/key.core/src/main/java/de/uka/ilkd/key/settings/TermLabelSettings.java
#	key/key.core/src/main/java/de/uka/ilkd/key/speclang/SLEnvInput.java
#	key/key.core/src/main/java/de/uka/ilkd/key/util/HelperClassForTests.java
#	key/key.core/src/test/java/de/uka/ilkd/key/smt/SMTTestSettings.java
#	key/key.ui/src/main/java/de/uka/ilkd/key/gui/MainWindow.java
#	key/key.ui/src/main/java/de/uka/ilkd/key/gui/actions/HidePackagePrefixToggleAction.java
#	key/key.ui/src/main/java/de/uka/ilkd/key/gui/actions/MinimizeInteraction.java
#	key/key.ui/src/main/java/de/uka/ilkd/key/gui/actions/PrettyPrintToggleAction.java
#	key/key.ui/src/main/java/de/uka/ilkd/key/gui/actions/ToggleSequentViewTooltipAction.java
#	key/key.ui/src/main/java/de/uka/ilkd/key/gui/actions/UnicodeToggleAction.java
#	key/key.ui/src/main/java/de/uka/ilkd/key/gui/configuration/ChoiceSelector.java
#	key/key.ui/src/main/java/de/uka/ilkd/key/gui/keyshortcuts/KeyStrokeSettings.java
#	key/key.ui/src/main/java/de/uka/ilkd/key/gui/lemmatagenerator/LoadUserTacletsDialog.java
#	key/key.ui/src/main/java/de/uka/ilkd/key/gui/originlabels/ToggleOriginHighlightAction.java
#	key/key.ui/src/main/java/de/uka/ilkd/key/gui/smt/TacletTranslationSelection.java
#	key/key.ui/src/main/java/de/uka/ilkd/key/gui/smt/settings/TranslationOptions.java
#	key/keyext.exploration/src/main/java/org/key_project/exploration/actions/ShowInteractiveBranchesAction.java
#	key/keyext.ui.testgen/src/main/java/de/uka/ilkd/key/gui/testgen/TestgenOptionsPanel.java
@wadoon
fix errors due to merge
3f29c96
@wadoon
InitConfig should be modifiable
df865af
@wadoon
Merge branch 'master' into weigl/config
2c6b69f 
* master: (160 commits)
  .git-blame-ignore-revs: ignore formatting commits
  Update checkstyle configuration to 10.6.0
  Move subprojects to top level
  Keep PositionInfo in ForToWhileTransformation
  log instead of disabling EditMostRecentFileAction on error
  Remove KeYDesktop interface, use java.awt.Desktop directly
  Logview open log file fallback: Browse dir
  Fixing a few typos in example files
  reducing the binary filesize by only including the necessary example files
  Fix typo in comment
  Checkstyle
  Immediately resize proof tree font
  Fix Z3 counterexample generation
  Recalculate all unique names on every change since the algorithm is incremental and does not change old names.
  SonarCube
  Add comments and move main method to tests
  Improve naming of recent files
  Keep entry class private, it's not used outside the class
  corrected the formatting
  Test for polarity check during replay
  ...
@wadoon
Merge remote-tracking branch 'origin/main' into weigl/config
1f22e51 
# By Julian Wiesler (91) and others
# Via GitHub (23) and others
* origin/main: (144 commits)
  improving javadoc, removing old code.
  Throw exception with location information on invalid unicode escape sequence
  Move JavaCharStream to the correct folder on build
  Report location on error in constant evaluation
  applying spotless
  small fixes and improvements to proof scripts
  adding features to immutable lists
  Fix javadoc formatting
  Correctly handle unloading proofs
  Formatting and documentation
  ignore class output, add test case
  Javac issues extension: handle non-Java proofs
  Fix construction of Javac issue dialog
  fix typo
  Update tests.yml
  Fix javacc deprecation warning
  Fix branch name in Checkstyle script
  Update feature_request.md
  copy bug-report from gitlab to github
  Update dlsmt.sh
  ...

# Conflicts:
#	key.core/src/main/java/de/uka/ilkd/key/settings/AbstractPropertiesSettings.java
#	key.ui/src/main/java/de/uka/ilkd/key/gui/colors/ColorSettings.java
@wadoon
spotless
29d3eb2
@wadoon
strange artifact removed
e0e54ef
@wadoon
fix auto-merge errors
211a1ff
@FliegendeWurst FliegendeWurst added the 🛠 Maintenance Code quality and related things w/o functional changes label Mar 24, 2023
@wadoon wadoon self-assigned this Mar 31, 2023
@wadoon wadoon added this to the v2.12.0 milestone Apr 3, 2023
@wadoon
Merge remote-tracking branch 'origin/main' into weigl/config
14727e1 
* origin/main: (25 commits)
  Fix name
  Fix indent
  Add link to the newest artifact
  Better artiweb comment workflow
  Update tests.yml
  update symbex oracles
  add a config for Github codespaces
  fix merge error
  fix decprecation in Gradle
  Bump com.github.johnrengelman.shadow from 7.1.0 to 8.1.1
  apply spotless
  set an import order for Java code
  Format
  Fix search and replace errors
  Comments for other oracle files
  TestPositions javadoc and comments
  Make Position constructor private, explicit factory method, doc
  ProofJavaPrgoramFactoryTest
  Fix positions around array types
  Fix annotations
  ...
@wadoon
remove config grammar
fe66a28
@wadoon
remove codespace config
13b3698
@wadoon wadoon marked this pull request as ready for review April 3, 2023 11:26
@wadoon wadoon mentioned this pull request Apr 3, 2023
Merged
@wadoon wadoon requested a review from jwiesler April 5, 2023 11:59
@wadoon wadoon enabled auto-merge April 5, 2023 11:59
@wadoon
fix issue of reviewer
c84c18b
@wadoon
Merge remote-tracking branch 'origin/main' into weigl/config
6505700 
* origin/main: (62 commits)
  Fix comment author and nicer message
  fix typo in filename
  Fail gracefully
  Fix conversion to number of empty string
  Unused files
  Fix bsumSplitInvalid being notprovable
  Move file again
  Move file
  Remove duplicate group
  Spotless
  Fix option being ignored by not being formatted
  Fix proof settings not being used
  Sort output of DefaultChoices
  Cleanup
  Fix input
  Fix input
  Fix writing of the pr number
  Fix type of `Long.MIN_VALUE` and `Long.MAX_VALUE`
  Reword message
  Fix script syntax errors
  ...
@wadoon wadoon added this pull request to the merge queue Apr 6, 2023
@github-actions
Copy link

github-actions bot commented Apr 6, 2023

Thank you for your contribution.

The test artifacts are available on Artiweb.
The newest artifact is here.

Merged via the queue into KeYProject:main with commit dd62d03 Apr 6, 2023
@wadoon wadoon deleted the weigl/config branch April 6, 2023 03:42
jwiesler
jwiesler reviewed Apr 7, 2023
View reviewed changes
key.core/src/main/java/de/uka/ilkd/key/settings/ChoiceSettings.java
public void writeSettings(Properties props) {
StringBuilder choiceSequence = new StringBuilder();
Copy link
Contributor

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

@wadoon you deleted an earlier change from me here by the way...

@wadoon wadoon mentioned this pull request Jul 16, 2023
Open
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Reviewers

@jwiesler jwiesler jwiesler approved these changes

Assignees

@wadoon wadoon

Labels
🛠 Maintenance Code quality and related things w/o functional changes
Projects
None yet
Milestone
v2.12.0
Development

Successfully merging this pull request may close these issues.
3 participants
@wadoon @jwiesler @FliegendeWurst