-
Notifications
You must be signed in to change notification settings - Fork 25
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.
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
Abbreviations Manager #3202
base: main
Are you sure you want to change the base?
Abbreviations Manager #3202
Conversation
Codecov ReportAttention:
Additional details and impacted files@@ Coverage Diff @@
## main #3202 +/- ##
============================================
+ Coverage 37.93% 37.97% +0.04%
+ Complexity 17030 17024 -6
============================================
Files 2060 2059 -1
Lines 126300 126060 -240
Branches 21304 21280 -24
============================================
- Hits 47913 47874 -39
+ Misses 72499 72304 -195
+ Partials 5888 5882 -6 ☔ View full report in Codecov by Sentry. |
Thanks for abbreviation delete! What would be great imo is if I try to create an abbreviation and that name is already taken: Show an option to remove the old and use this as the new label term. |
Can't this be stored in the proof file itself? I think this would be a better place to store. |
My current story for load/store is that you attempt to proof something, notice a specification (or KeY) failure, fix it and restart the attempt. Then you can rescue the abbreviations. Proof attempts are rather not stored as proof files. But maybe we should consider storing the abbreviations in the settings. I would wait for #3031 for a type-safe lists in the settings. |
#3031 is already merged? Settings would be a good idea as well. |
# Conflicts: # key.ui/src/main/java/de/uka/ilkd/key/gui/nodeviews/DefaultBuiltInRuleMenuItem.java # key.ui/src/main/java/de/uka/ilkd/key/gui/nodeviews/InnerNodeViewMenu.java # key.ui/src/main/java/de/uka/ilkd/key/gui/nodeviews/InsertHiddenTacletMenuItem.java # key.ui/src/main/java/de/uka/ilkd/key/gui/nodeviews/InsertSystemInvariantTacletMenuItem.java # key.ui/src/main/java/de/uka/ilkd/key/gui/nodeviews/MenuItemForTwoModeRules.java # key.ui/src/main/java/de/uka/ilkd/key/gui/smt/SMTMenuItem.java
I am confused by the save abbreviations dialog. It suggests to save this data as a
|
How does the load abbreviations functionality work? I selected my previously saved file, but no abbreviations were restored. |
The abbreviations transfer does not work for program variables. I think they would need to be compared by name, not by identity. |
* origin/main: (207 commits) Use Amazon's Corretto add caching for gradle dependencies Update to Java 21 Runtime for testing Use pattern matching to avoid cast Change default notification setting to unfocused Renaming from reviewer suggestion (got lost when splitting the PR) Minor cleanup Prevent possible NullPointerException. Cleanup. Remove last usage of the legacy matcher. Check only new terms for well-typedness Move static metavariable cache to service caches Minor cleanup incl. spotless changes Use array of assumes instantiations Preparation for parallel prover engine - make Strategies stateless by introducing a specific explicit state object for TermBuffers and the Backtracking Manager This will allow strategies to execute in parallel Update keyext.ui.testgen/src/main/java/de/uka/ilkd/key/gui/testgen/CounterExampleAction.java Update keyext.ui.testgen/src/main/java/de/uka/ilkd/key/gui/testgen/TGInfoDialog.java Some cleanup and proper switching to automode Avoid access of non-private field in synchronized context Pruning a closed proof (and reopening it) did not update the proof status in the task tree and also did not select any node/goal. Minor clean up ... # Conflicts: # key.core/src/main/java/de/uka/ilkd/key/pp/AbbrevMap.java # key.ui/src/main/java/de/uka/ilkd/key/gui/nodeviews/CurrentGoalViewMenu.java # key.ui/src/main/java/de/uka/ilkd/key/gui/nodeviews/SequentViewMenu.java # key.ui/src/main/resources/META-INF/services/de.uka.ilkd.key.gui.extension.api.KeYGuiExtension
Abbreviations are built-in to the KeY system, but this construct is not very popular. This may be to their volatility: you are not able to store, and reuse them on new proof attempts.
This PR brings a new widget:
The widget offers following features:
<label>::==<term>
describes an abbreviation.