Refactor and clarify the loading process of KeY, which has become complicated and hard to maintain.
Underlying problem
The loading process is currently messy, increasingly complex, and not understandable. Changes are often successful only by luck, making maintenance and extensions very difficult.
The loading process mainly occurs in ProblemInitializer, along with InitConfig and Services. Later the ProofObligationLoaders are triggered for creating the PO.
One of the major problems is, e.g., the ProofSettings, especially the ChoiceSettings and their precedence from various sources (settings, profile, useOption, user-defaults). The other problem is the separation of Java and KeY loading.
Refactor and clarify the loading process of KeY, which has become complicated and hard to maintain.
Underlying problem
The loading process is currently messy, increasingly complex, and not understandable. Changes are often successful only by luck, making maintenance and extensions very difficult.
The loading process mainly occurs in
ProblemInitializer, along withInitConfigandServices. Later theProofObligationLoaders are triggered for creating the PO.One of the major problems is, e.g., the
ProofSettings, especially theChoiceSettingsand their precedence from various sources (settings, profile,useOption, user-defaults). The other problem is the separation of Java and KeY loading.