From b4112577415ef154b8e3a5c7d58dd217ee2a657d Mon Sep 17 00:00:00 2001 From: "dependabot[bot]" <49699333+dependabot[bot]@users.noreply.github.com> Date: Mon, 1 Jul 2024 20:05:33 +0000 Subject: [PATCH 1/4] Bump the gradle-deps group with 4 updates Bumps the gradle-deps group with 4 updates: [org.junit.jupiter:junit-jupiter-api](https://github.com/junit-team/junit5), [org.junit.jupiter:junit-jupiter-params](https://github.com/junit-team/junit5), [org.junit.jupiter:junit-jupiter-engine](https://github.com/junit-team/junit5) and org.checkerframework. Updates `org.junit.jupiter:junit-jupiter-api` from 5.10.2 to 5.10.3 - [Release notes](https://github.com/junit-team/junit5/releases) - [Commits](https://github.com/junit-team/junit5/compare/r5.10.2...r5.10.3) Updates `org.junit.jupiter:junit-jupiter-params` from 5.10.2 to 5.10.3 - [Release notes](https://github.com/junit-team/junit5/releases) - [Commits](https://github.com/junit-team/junit5/compare/r5.10.2...r5.10.3) Updates `org.junit.jupiter:junit-jupiter-engine` from 5.10.2 to 5.10.3 - [Release notes](https://github.com/junit-team/junit5/releases) - [Commits](https://github.com/junit-team/junit5/compare/r5.10.2...r5.10.3) Updates `org.checkerframework` from 0.6.39 to 0.6.41 --- updated-dependencies: - dependency-name: org.junit.jupiter:junit-jupiter-api dependency-type: direct:production update-type: version-update:semver-patch dependency-group: gradle-deps - dependency-name: org.junit.jupiter:junit-jupiter-params dependency-type: direct:production update-type: version-update:semver-patch dependency-group: gradle-deps - dependency-name: org.junit.jupiter:junit-jupiter-engine dependency-type: direct:production update-type: version-update:semver-patch dependency-group: gradle-deps - dependency-name: org.checkerframework dependency-type: direct:production update-type: version-update:semver-patch dependency-group: gradle-deps ... Signed-off-by: dependabot[bot] --- build.gradle | 8 ++++---- 1 file changed, 4 insertions(+), 4 deletions(-) diff --git a/build.gradle b/build.gradle index 935addaa9a8..6df46bffc01 100644 --- a/build.gradle +++ b/build.gradle @@ -24,7 +24,7 @@ plugins { id "com.diffplug.spotless" version "6.25.0" // EISOP Checker Framework - id "org.checkerframework" version "0.6.39" + id "org.checkerframework" version "0.6.41" } // Configure this project for use inside IntelliJ: @@ -90,11 +90,11 @@ subprojects { checkerFramework "io.github.eisop:checker:$eisop_version" testImplementation("ch.qos.logback:logback-classic:1.5.6") - testImplementation 'org.junit.jupiter:junit-jupiter-api:5.10.2' - testImplementation 'org.junit.jupiter:junit-jupiter-params:5.10.2' + testImplementation 'org.junit.jupiter:junit-jupiter-api:5.10.3' + testImplementation 'org.junit.jupiter:junit-jupiter-params:5.10.3' testImplementation project(':key.util') - testRuntimeOnly 'org.junit.jupiter:junit-jupiter-engine:5.10.2' + testRuntimeOnly 'org.junit.jupiter:junit-jupiter-engine:5.10.3' } tasks.withType(JavaCompile) { From c6ffa71e1ad4af153bcd4ecdecdc28585833c275 Mon Sep 17 00:00:00 2001 From: "dependabot[bot]" <49699333+dependabot[bot]@users.noreply.github.com> Date: Mon, 1 Jul 2024 20:24:59 +0000 Subject: [PATCH 2/4] Bump gradle/actions from 3.3.2 to 3.4.2 in the github-actions-deps group Bumps the github-actions-deps group with 1 update: [gradle/actions](https://github.com/gradle/actions). Updates `gradle/actions` from 3.3.2 to 3.4.2 - [Release notes](https://github.com/gradle/actions/releases) - [Commits](https://github.com/gradle/actions/compare/v3.3.2...v3.4.2) --- updated-dependencies: - dependency-name: gradle/actions dependency-type: direct:production update-type: version-update:semver-minor dependency-group: github-actions-deps ... Signed-off-by: dependabot[bot] --- .github/workflows/code_quality.yml | 8 ++++---- .github/workflows/gradle-publish.yml | 2 +- .github/workflows/javadoc.yml | 2 +- .github/workflows/nightlydeploy.yml | 2 +- .github/workflows/opttest.yml | 2 +- .github/workflows/tests.yml | 4 ++-- .github/workflows/tests_winmac.yml | 4 ++-- 7 files changed, 12 insertions(+), 12 deletions(-) diff --git a/.github/workflows/code_quality.yml b/.github/workflows/code_quality.yml index a13aecf615f..327890ba723 100644 --- a/.github/workflows/code_quality.yml +++ b/.github/workflows/code_quality.yml @@ -20,7 +20,7 @@ jobs: distribution: 'corretto' cache: 'gradle' - name: Setup Gradle - uses: gradle/actions/setup-gradle@v3.3.2 + uses: gradle/actions/setup-gradle@v3.4.2 - name: Build with Gradle run: ./gradlew -DENABLE_NULLNESS=true compileTest @@ -49,7 +49,7 @@ jobs: java-version: '21' cache: 'gradle' - name: Setup Gradle - uses: gradle/actions/setup-gradle@v3.3.2 + uses: gradle/actions/setup-gradle@v3.4.2 - name: SpotlessCheck run: ./gradlew --continue spotlessCheck @@ -81,7 +81,7 @@ jobs: java-version: '21' cache: 'gradle' - name: Setup Gradle - uses: gradle/actions/setup-gradle@v3.3.2 + uses: gradle/actions/setup-gradle@v3.4.2 - name: Checkstyle run: ./gradlew --continue checkstyleMainChanged - run: | @@ -108,7 +108,7 @@ jobs: java-version: '21' cache: 'gradle' - name: Setup Gradle - uses: gradle/actions/setup-gradle@v3.3.2 + uses: gradle/actions/setup-gradle@v3.4.2 - name: PMD checks run: ./gradlew --continue pmdMainChanged diff --git a/.github/workflows/gradle-publish.yml b/.github/workflows/gradle-publish.yml index e46dd959484..ab43091e529 100644 --- a/.github/workflows/gradle-publish.yml +++ b/.github/workflows/gradle-publish.yml @@ -22,7 +22,7 @@ jobs: server-id: github # Value of the distributionManagement/repository/id field of the pom.xml - name: Setup Gradle - uses: gradle/actions/setup-gradle@v3.3.2 + uses: gradle/actions/setup-gradle@v3.4.2 - name: Assemble with Gradle run: ./gradlew assemble diff --git a/.github/workflows/javadoc.yml b/.github/workflows/javadoc.yml index 82e5a48f7be..1ebbb82c9fe 100644 --- a/.github/workflows/javadoc.yml +++ b/.github/workflows/javadoc.yml @@ -19,7 +19,7 @@ jobs: distribution: 'corretto' cache: 'gradle' - name: Setup Gradle - uses: gradle/actions/setup-gradle@v3.3.2 + uses: gradle/actions/setup-gradle@v3.4.2 - name: Build Documentation with Gradle run: ./gradlew alldoc diff --git a/.github/workflows/nightlydeploy.yml b/.github/workflows/nightlydeploy.yml index 97cd713ffac..f60a7fc2762 100644 --- a/.github/workflows/nightlydeploy.yml +++ b/.github/workflows/nightlydeploy.yml @@ -31,7 +31,7 @@ jobs: distribution: 'temurin' - name: Setup Gradle - uses: gradle/actions/setup-gradle@v3.3.2 + uses: gradle/actions/setup-gradle@v3.4.2 - name: Build with Gradle run: ./gradlew --parallel assemble diff --git a/.github/workflows/opttest.yml b/.github/workflows/opttest.yml index 360cb718d81..8093ed2b328 100644 --- a/.github/workflows/opttest.yml +++ b/.github/workflows/opttest.yml @@ -25,7 +25,7 @@ jobs: cache: 'gradle' - name: Setup Gradle - uses: gradle/actions/setup-gradle@v3.3.2 + uses: gradle/actions/setup-gradle@v3.4.2 - name: Test with Gradle run: ./gradlew --continue ${{ matrix.tests }} diff --git a/.github/workflows/tests.yml b/.github/workflows/tests.yml index a9f68ed0541..e45ebec48c2 100644 --- a/.github/workflows/tests.yml +++ b/.github/workflows/tests.yml @@ -38,7 +38,7 @@ jobs: cache: 'gradle' - name: Setup Gradle - uses: gradle/actions/setup-gradle@v3.3.2 + uses: gradle/actions/setup-gradle@v3.4.2 - name: Test with Gradle run: ./gradlew --continue -DjacocoEnabled=true -x :key.core.symbolic_execution:test -x :key.core.proof_references:test test @@ -87,7 +87,7 @@ jobs: shell: bash - name: Setup Gradle - uses: gradle/actions/setup-gradle@v3.3.2 + uses: gradle/actions/setup-gradle@v3.4.2 - name: "Running tests: ${{ matrix.test }}" run: ./gradlew --continue ${{ matrix.test }} diff --git a/.github/workflows/tests_winmac.yml b/.github/workflows/tests_winmac.yml index 96a248d0b2c..fd4cbb74b31 100644 --- a/.github/workflows/tests_winmac.yml +++ b/.github/workflows/tests_winmac.yml @@ -30,7 +30,7 @@ jobs: - name: Setup Gradle uses: - gradle/actions/setup-gradle@v3.3.2 + gradle/actions/setup-gradle@v3.4.2 - name: Test with Gradle run: ./gradlew --continue -x :key.core.symbolic_execution:test -x :key.core.proof_references:test test @@ -76,7 +76,7 @@ jobs: run: .github/dlsmt.sh - name: Setup Gradle - uses: gradle/actions/setup-gradle@v3.3.2 + uses: gradle/actions/setup-gradle@v3.4.2 - name: "Running tests: ${{ matrix.test }}" run: ./gradlew --continue ${{ matrix.test }} From dc486e411e98319a9d65de7e72d4d9404b763f57 Mon Sep 17 00:00:00 2001 From: Mattias Ulbrich Date: Sun, 7 Jul 2024 14:35:28 +0200 Subject: [PATCH 3/4] saving proofs for sequent problems Parsing sequents in \problem{...} has been supported for a while now. This commit adapts the saving routine accordingly. --- .../key/proof/io/OutputStreamProofSaver.java | 8 ++- .../uka/ilkd/key/proof/io/ProofSaverTest.java | 52 +++++++++++++++++++ 2 files changed, 59 insertions(+), 1 deletion(-) create mode 100644 key.core/src/test/java/de/uka/ilkd/key/proof/io/ProofSaverTest.java diff --git a/key.core/src/main/java/de/uka/ilkd/key/proof/io/OutputStreamProofSaver.java b/key.core/src/main/java/de/uka/ilkd/key/proof/io/OutputStreamProofSaver.java index 9bfd785e9e4..90223c6dbb5 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/proof/io/OutputStreamProofSaver.java +++ b/key.core/src/main/java/de/uka/ilkd/key/proof/io/OutputStreamProofSaver.java @@ -209,7 +209,13 @@ public void save(OutputStream out) throws IOException { } final Sequent problemSeq = proof.root().sequent(); ps.println("\\problem {"); - printer.printSemisequent(problemSeq.succedent()); + if(problemSeq.antecedent().isEmpty() && problemSeq.succedent().size() == 1) { + // Problem statement is a single formula ... + printer.printSemisequent(problemSeq.succedent()); + } else { + // Problem statement is a proper sequent ... + printer.printSequent(problemSeq); + } ps.println(printer.result()); ps.println("}\n"); } diff --git a/key.core/src/test/java/de/uka/ilkd/key/proof/io/ProofSaverTest.java b/key.core/src/test/java/de/uka/ilkd/key/proof/io/ProofSaverTest.java new file mode 100644 index 00000000000..97add25bbbb --- /dev/null +++ b/key.core/src/test/java/de/uka/ilkd/key/proof/io/ProofSaverTest.java @@ -0,0 +1,52 @@ +package de.uka.ilkd.key.proof.io; + +import de.uka.ilkd.key.java.Services; +import de.uka.ilkd.key.logic.Sequent; +import de.uka.ilkd.key.nparser.KeyIO; +import de.uka.ilkd.key.proof.Proof; +import de.uka.ilkd.key.proof.init.AbstractProfile; +import de.uka.ilkd.key.proof.init.InitConfig; +import de.uka.ilkd.key.rule.TacletForTests; +import de.uka.ilkd.key.util.KeYConstants; +import org.jspecify.annotations.Nullable; +import org.junit.jupiter.api.Test; + +import java.io.File; +import java.io.IOException; + +import static org.junit.jupiter.api.Assertions.*; + +class ProofSaverTest { + + void testSaveProblemToFile(String content) throws IOException { + Services services = TacletForTests.services(); + KeyIO io = new KeyIO(services); + KeyIO.Loader loader = io.load(content); + Sequent seq = loader.parseFile().loadProblem().getProblem(); + final InitConfig initConfig = + new InitConfig(new Services(AbstractProfile.getDefaultProfile())); + Proof proof = new Proof("test", seq, "", initConfig, null); + File file = File.createTempFile("proofSaveTest", ".key"); + file.deleteOnExit(); + String status = new ProofSaver(proof, file).save(); + assertNull(status); + + KeyIO io2 = new KeyIO(services); + KeyIO.Loader loader2 = io2.load(content); + Sequent seq2 = loader2.parseFile().loadProblem().getProblem(); + + assertEquals(seq, seq2); + } + + @Test + void saveTermProblemToFile() throws IOException { + String content = "\\problem { true }"; + testSaveProblemToFile(content); + } + + @Test + void saveSequentProblemToFile() throws IOException { + String content = "\\problem { true, false ==> false, false }"; + testSaveProblemToFile(content); + } +} \ No newline at end of file From ea0879b48926a6a5ebe4761e807042600153a97a Mon Sep 17 00:00:00 2001 From: Mattias Ulbrich Date: Sun, 7 Jul 2024 17:02:15 +0200 Subject: [PATCH 4/4] spotlessing ... --- .../key/proof/io/OutputStreamProofSaver.java | 2 +- .../de/uka/ilkd/key/proof/io/ProofSaverTest.java | 16 +++++++++------- 2 files changed, 10 insertions(+), 8 deletions(-) diff --git a/key.core/src/main/java/de/uka/ilkd/key/proof/io/OutputStreamProofSaver.java b/key.core/src/main/java/de/uka/ilkd/key/proof/io/OutputStreamProofSaver.java index 90223c6dbb5..82ee5ef01ad 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/proof/io/OutputStreamProofSaver.java +++ b/key.core/src/main/java/de/uka/ilkd/key/proof/io/OutputStreamProofSaver.java @@ -209,7 +209,7 @@ public void save(OutputStream out) throws IOException { } final Sequent problemSeq = proof.root().sequent(); ps.println("\\problem {"); - if(problemSeq.antecedent().isEmpty() && problemSeq.succedent().size() == 1) { + if (problemSeq.antecedent().isEmpty() && problemSeq.succedent().size() == 1) { // Problem statement is a single formula ... printer.printSemisequent(problemSeq.succedent()); } else { diff --git a/key.core/src/test/java/de/uka/ilkd/key/proof/io/ProofSaverTest.java b/key.core/src/test/java/de/uka/ilkd/key/proof/io/ProofSaverTest.java index 97add25bbbb..d55f9f78743 100644 --- a/key.core/src/test/java/de/uka/ilkd/key/proof/io/ProofSaverTest.java +++ b/key.core/src/test/java/de/uka/ilkd/key/proof/io/ProofSaverTest.java @@ -1,5 +1,11 @@ +/* This file is part of KeY - https://key-project.org + * KeY is licensed under the GNU General Public License Version 2 + * SPDX-License-Identifier: GPL-2.0-only */ package de.uka.ilkd.key.proof.io; +import java.io.File; +import java.io.IOException; + import de.uka.ilkd.key.java.Services; import de.uka.ilkd.key.logic.Sequent; import de.uka.ilkd.key.nparser.KeyIO; @@ -7,12 +13,8 @@ import de.uka.ilkd.key.proof.init.AbstractProfile; import de.uka.ilkd.key.proof.init.InitConfig; import de.uka.ilkd.key.rule.TacletForTests; -import de.uka.ilkd.key.util.KeYConstants; -import org.jspecify.annotations.Nullable; -import org.junit.jupiter.api.Test; -import java.io.File; -import java.io.IOException; +import org.junit.jupiter.api.Test; import static org.junit.jupiter.api.Assertions.*; @@ -24,7 +26,7 @@ void testSaveProblemToFile(String content) throws IOException { KeyIO.Loader loader = io.load(content); Sequent seq = loader.parseFile().loadProblem().getProblem(); final InitConfig initConfig = - new InitConfig(new Services(AbstractProfile.getDefaultProfile())); + new InitConfig(new Services(AbstractProfile.getDefaultProfile())); Proof proof = new Proof("test", seq, "", initConfig, null); File file = File.createTempFile("proofSaveTest", ".key"); file.deleteOnExit(); @@ -49,4 +51,4 @@ void saveSequentProblemToFile() throws IOException { String content = "\\problem { true, false ==> false, false }"; testSaveProblemToFile(content); } -} \ No newline at end of file +}