Revive work on Polymorphic Sorts #3384
Draft
Conversation
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
* master: (1310 commits) make ExceptionDialog able to show files in Jar files catch headless to make key --auto runnable again made tooltip, click detection, and area to change mouse cursor more precise checkstyle tooltip and hand cursor only appear if the mouse pointer is over the highlight (probably needs optimization performance-wise) add option to toggle SourceView tooltip, change mouse pointer over highlightings to hand, shorter tooltip swap lines in gitlab ci, such that sonarqube is always reported Fix \singleton(3) JML-Extension: Assert/Assume and *_free for block contracts Better exception message in JML parser Renovating the Jml Parser check whether settings are non-null; use default value otherwise fix dependencies for gradle 7+ Add setting to disable load examples dialog window Fix #1566 fixed NPE with regroup search filter improved and corrected wrapLine specification and implementation Fixes issues with displaying syntax errors [Fix] Intersection construction of location sets in TemrBuilder adding a KeY-proven line wrapping method. ... # Conflicts: # key/key.core.test/src/de/uka/ilkd/key/parser/TestDeclParser.java # key/key.core/src/de/uka/ilkd/key/logic/sort/ProgramSVSort.java # key/key.core/src/de/uka/ilkd/key/parser/KeYLexer.g # key/key.core/src/de/uka/ilkd/key/parser/KeYParser.g # key/key.core/src/main/java/de/uka/ilkd/key/logic/sort/AbstractSort.java # key/key.core/src/main/java/de/uka/ilkd/key/logic/sort/Sort.java # key/key.core/src/main/java/de/uka/ilkd/key/proof/init/ProblemInitializer.java # key/key.core/src/main/java/de/uka/ilkd/key/proof/io/IProofFileParser.java # key/key.util.test/src/org/key_project/util/suite/AllCollectionTests.java # key/key.util/src/main/java/org/key_project/util/collection/ImmutableList.java # key/key.util/src/main/java/org/key_project/util/collection/ImmutableSLList.java # key/key.util/src/org/key_project/util/collection/DefaultImmutableSet.java # key/key.util/src/org/key_project/util/collection/ImmutableSet.java # key/key.util/src/test/java/org/key_project/util/collection/TestSLList.java
* branch should be up-to-date with current infrastructure
* origin/main: (2237 commits) Bump org.slf4j:slf4j-api from 2.0.10 to 2.0.11 Bump org.slf4j:slf4j-api from 2.0.9 to 2.0.10 spotless after discussion: all datatypes are free ignore files in */antlr4/gen/* bug fix applying spotless Configurable enabled keys for JML condition evaluation Spotless cleanups Fix selection highlight for OSS node child Remove unnecessary checks for correct change as listener is now registered correctly only for changes of interest Make usage of PropertyChangeListeners working (addendum to previous commit) Reduce number of sequentview updates Remove duplicate update of sequentview USe refactorings from #3369 but preserve non-local filter semantics for proof tree view MainWindow updates sequent view after settings change for pretty printing Minor clean up to slightly simplify complexity of path selection in ProofTreeView Fix problem with closed subtree filter Fix node filter selection display in popup dialoh and some refactoring Restore correct node selection and remove unused fields from GUIProofTreeModel ... # Conflicts: # key.core/src/main/java/de/uka/ilkd/key/logic/sort/AbstractSort.java # key.core/src/main/java/de/uka/ilkd/key/logic/sort/ParametricSort.java # key.core/src/main/java/de/uka/ilkd/key/logic/sort/ParametricSortInstance.java # key.core/src/main/java/de/uka/ilkd/key/logic/sort/ProgramSVSort.java # key.core/src/main/java/de/uka/ilkd/key/logic/sort/Sort.java # key.core/src/main/java/de/uka/ilkd/key/nparser/builder/DeclarationBuilder.java # key.core/src/main/java/de/uka/ilkd/key/proof/init/ProblemInitializer.java # key/key.core/src/main/java/de/uka/ilkd/key/logic/op/SortDependingFunction.java # key/key.core/src/main/java/de/uka/ilkd/key/logic/sort/NullSort.java # key/key.core/src/main/java/de/uka/ilkd/key/proof/io/IProofFileParser.java # key/key.core/src/main/java/de/uka/ilkd/key/rule/inst/GenericSortCondition.java # key/key.core/src/main/java/de/uka/ilkd/key/rule/inst/GenericSortInstantiations.java # key/key.core/src/test/java/de/uka/ilkd/key/parser/TestDeclParser.java # key/key.util/src/main/java/org/key_project/util/collection/ImmutableList.java # key/key.util/src/main/java/org/key_project/util/collection/ImmutableSLList.java # key/key.util/src/main/java/org/key_project/util/collection/Immutables.java
|
Support for data types: Test case fails. |
# By Drodt (57) and others # Via GitHub (25) and others * origin/main: (157 commits) ColorSettings: drop old configuration file format Merge main into extraxt-new-core Bump ch.qos.logback:logback-classic from 1.5.0 to 1.5.3 fixes #1533 added checkbox to disable example loader directly in dialog address reviewer comments: set border + spotless + typo JML enabled keys indicator for the status line add test case for adt taclets Fix position info for equality expr errors Revert debugging code Spotless Add ADT Deconstructors Moved TestSMTMod to newsmt2 spotless applied to TestSMTMod Added test for Modulo Translation Added translation from KeY mod to SMT mod. Soundness derived from translation of KeY div to SMT div preventing NPEs in overloaded operators added test cases for operator overloading activate the OverloadedOperatorHandler.java for LocSet datatype and repair translation ... # Conflicts: # key.core/src/main/java/de/uka/ilkd/key/logic/sort/AbstractSort.java # key.core/src/main/java/de/uka/ilkd/key/logic/sort/ProgramSVSort.java # key.core/src/main/java/de/uka/ilkd/key/logic/sort/Sort.java # key.core/src/main/java/de/uka/ilkd/key/nparser/builder/DeclarationBuilder.java # key.core/src/main/java/de/uka/ilkd/key/nparser/builder/DefaultBuilder.java # key.core/src/main/java/de/uka/ilkd/key/proof/init/ProblemInitializer.java # key.core/src/test/java/de/uka/ilkd/key/parser/TestDeclParser.java
* refs/heads/main: (55 commits) typo Unify type annotation notation Apply spotless Remove unnecessary warnings and serialization key.ncore done configure key.ncore fix null values eisop in ncore Fix formatting Fix more NoSuchElementExceptions Fix NoSuchElementException in JavaInfo Remove redundant nullness checks and fix test cases Fix proof script #equals must allow null values jspecify was missing in the compile classpath of tests Code style Revert JavaRedux Object Test case Fix merge issues Mark havocPacked as helper ... # Conflicts: # key.core/src/main/java/de/uka/ilkd/key/nparser/builder/DeclarationBuilder.java # key.core/src/main/java/de/uka/ilkd/key/nparser/builder/TacletPBuilder.java # key.ncore/src/main/java/module-info.java # key.ncore/src/main/java/org/key_project/logic/op/AbstractOperator.java # key.ncore/src/main/java/org/key_project/logic/op/AbstractSortedOperator.java # key.ncore/src/main/java/org/key_project/logic/sort/AbstractSort.java # key.util/src/main/java/org/key_project/util/collection/DefaultImmutableSet.java # key.util/src/main/java/org/key_project/util/collection/ImmutableSLList.java # key.util/src/main/java/org/key_project/util/collection/Immutables.java
* refs/heads/main: (40 commits) Fix comment Fix checkstyle workflow reformat with spotless Fix checkstyle workflow Fix merge conflicts & spotless fix error in the legacy compat part of the proof obligation loading revert some changes of Mattias in the Configuration fix compile error and reformat Configuration: correcting typos, making implementation consistent address reviewers comments Remove todo Spotless Fix? resolving error Move ParsableVariable to ncore Spotless Spotless Rename AbstractSV to OperatorSV Beautified code Fix settings test for SE Spotless fixes ... # Conflicts: # key.core/src/main/java/de/uka/ilkd/key/nparser/builder/DefaultBuilder.java # key.core/src/test/java/de/uka/ilkd/key/parser/TestDeclParser.java
|
There are a number of fundamental questions to be sorted out: |
* main: (33 commits) Update key.core/src/main/java/de/uka/ilkd/key/nparser/builder/TacletPBuilder.java spotless update oracle for taclet equality test change gradle github action to new syntax adding comments to jml spec factory default contracts repair soundness of assignment2UpdateRules with checked overflows spotless EQ version of seqSwapPreservesSeqPerm + proof added rule for sequences: swap preserves perm Changed types in replacement map for WD taclets, since PR #3436 made casting TermSV to ProgramVariable not applicable Fix and test goToNext() Fix goToNextSibling() (thx Tobias) Format Add comments and next() method Remove SVSubstitute Clean up inheritance Implement missing methods Start implementation of traversal Implement cursor Increase Java version ...
* origin/main: (46 commits) spotless update removed default implementations for AbstractExternalSolverRuleApp around RULE field small formatting change Bump the gradle-deps group with 6 updates Bump JetBrains/qodana-action in the github-actions-deps group set version to 2.12.4-dev increase java version to 21 added missing conversion rules from javaUnaryMinusFloat/Double to negFloat/Double add AbstractExternalSolverRuleApp to allow other external solvers to close goals fixes NullPointerException, when using compareTo with locations that dont have a URI or position Bump the github-actions-deps group with 2 updates Bump the gradle-deps group with 5 updates formatting Bump the github-actions-deps group with 2 updates Bump the gradle-deps group with 8 updates spotless generating ProofTree tooltips lazily, options to disable them completely fix for visual bug with overlapping/unreadable text in color settings Fox copyright year Bump the gradle-deps group with 6 updates ...
|
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
Add this suggestion to a batch that can be applied as a single commit.
This suggestion is invalid because no changes were made to the code.
Suggestions cannot be applied while the pull request is closed.
Suggestions cannot be applied while viewing a subset of changes.
Only one suggestion per line can be applied in a batch.
Add this suggestion to a batch that can be applied as a single commit.
Applying suggestions on deleted lines is not supported.
You must change the existing code in this line in order to create a valid suggestion.
Outdated suggestions cannot be applied.
This suggestion has been applied or marked resolved.
Suggestions cannot be applied from pending reviews.
Suggestions cannot be applied on multi-line comments.
Suggestions cannot be applied while the pull request is queued to merge.
Suggestion cannot be applied right now. Please check back later.
Introducing Sorts with Sort-Parameters.
Type of pull request