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.

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

Open
wants to merge 10 commits into
base: main
Choose a base branch
from
Open

Abbreviations Manager #3202

wants to merge 10 commits into from

Conversation

wadoon
Copy link
Member

@wadoon wadoon commented Jul 14, 2023

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:

image

The widget offers following features:

  • view current defined abbreviations
  • load and store abbreviation mappings
    • A text file where each line <label>::==<term> describes an abbreviation.
  • transfer (import) abbreviations of currently open proofs
  • Context menu:
    • change the abbreviation label
    • delete an abbreviation
    • disable an abbreviate

@wadoon wadoon added the GUI label Jul 14, 2023
@wadoon wadoon self-assigned this Jul 14, 2023
@wadoon wadoon added this to the v2.14.0 milestone Jul 14, 2023
@codecov
Copy link

codecov bot commented Jul 14, 2023

Codecov Report

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

Comparison is base (603b2ca) 37.93% compared to head (ee98653) 37.97%.

❗ Current head ee98653 differs from pull request most recent head 6a80690. Consider uploading reports for the commit 6a80690 to get more accurate results

Files Patch % Lines
...re/src/main/java/de/uka/ilkd/key/pp/AbbrevMap.java 14.58% 41 Missing ⚠️
...ain/java/org/key_project/util/java/StringUtil.java 0.00% 16 Missing ⚠️
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.
📢 Have feedback on the report? Share it here.

@github-actions
Copy link

github-actions bot commented Jul 14, 2023

Thank you for your contribution.

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

@jwiesler
Copy link
Contributor

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.

@jwiesler
Copy link
Contributor

Can't this be stored in the proof file itself? I think this would be a better place to store.

@wadoon
Copy link
Member Author

wadoon commented Jul 16, 2023

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.

@jwiesler
Copy link
Contributor

#3031 is already merged?

Settings would be a good idea as well.

@wadoon
Copy link
Member Author

wadoon commented Jul 16, 2023

#3031 is already merged?

Settings would be a good idea as well.

Sorry, mean #3099

# 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
@wadoon wadoon marked this pull request as ready for review August 21, 2023 22:49
@FliegendeWurst
Copy link
Member

I am confused by the save abbreviations dialog. It suggests to save this data as a .proof:

p::==i_arr_5
d::==i_arr_2
l::==i_arr_8

@FliegendeWurst
Copy link
Member

How does the load abbreviations functionality work? I selected my previously saved file, but no abbreviations were restored.

@FliegendeWurst
Copy link
Member

The abbreviations transfer does not work for program variables. I think they would need to be compared by name, not by identity.

@FliegendeWurst FliegendeWurst added the Feature New feature or request label Sep 8, 2023
wadoon and others added 5 commits November 19, 2023 16:15
* 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
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
Feature New feature or request GUI
Projects
None yet
Development

Successfully merging this pull request may close these issues.

3 participants