From 22a392853dc522438d678838707a83863114a370 Mon Sep 17 00:00:00 2001
From: Wolfram Pfeifer <94171076+WolframPfeifer@users.noreply.github.com>
Date: Mon, 30 Jan 2023 20:06:49 +0100
Subject: [PATCH 1/8] Update issue templates

added templates for bug report and feature request
---
 .github/ISSUE_TEMPLATE/bug_report.md      | 31 +++++++++++++++++++++++
 .github/ISSUE_TEMPLATE/feature_request.md | 20 +++++++++++++++
 2 files changed, 51 insertions(+)
 create mode 100644 .github/ISSUE_TEMPLATE/bug_report.md
 create mode 100644 .github/ISSUE_TEMPLATE/feature_request.md

diff --git a/.github/ISSUE_TEMPLATE/bug_report.md b/.github/ISSUE_TEMPLATE/bug_report.md
new file mode 100644
index 00000000000..a124278ff05
--- /dev/null
+++ b/.github/ISSUE_TEMPLATE/bug_report.md
@@ -0,0 +1,31 @@
+---
+name: Bug report
+about: Create a report to help us improve
+title: ''
+labels: ''
+assignees: ''
+
+---
+
+**Describe the bug**
+A clear and concise description of what the bug is.
+
+**To Reproduce**
+Steps to reproduce the behavior:
+1. ...
+2. ...
+3. ...
+
+**Expected behavior**
+A clear and concise description of what you expected to happen.
+
+**Desktop (please complete the following information):**
+ - OS: [e.g. iOS]
+ - Browser [e.g. chrome, safari]
+ - Version [e.g. 22]
+
+**Additional information**
+Add any other context about the problem here.
+* Commit Hash:
+* Screenshots
+If applicable, add screenshots to help explain your problem.
diff --git a/.github/ISSUE_TEMPLATE/feature_request.md b/.github/ISSUE_TEMPLATE/feature_request.md
new file mode 100644
index 00000000000..bbcbbe7d615
--- /dev/null
+++ b/.github/ISSUE_TEMPLATE/feature_request.md
@@ -0,0 +1,20 @@
+---
+name: Feature request
+about: Suggest an idea for this project
+title: ''
+labels: ''
+assignees: ''
+
+---
+
+**Is your feature request related to a problem? Please describe.**
+A clear and concise description of what the problem is. Ex. I'm always frustrated when [...]
+
+**Describe the solution you'd like**
+A clear and concise description of what you want to happen.
+
+**Describe alternatives you've considered**
+A clear and concise description of any alternative solutions or features you've considered.
+
+**Additional context**
+Add any other context or screenshots about the feature request here.

From 8dc913caf90b8ca56dc52f727a9dd73a80a8ad78 Mon Sep 17 00:00:00 2001
From: Wolfram Pfeifer <94171076+WolframPfeifer@users.noreply.github.com>
Date: Mon, 30 Jan 2023 20:16:29 +0100
Subject: [PATCH 2/8] Update bug_report.md

---
 .github/ISSUE_TEMPLATE/bug_report.md | 12 ++++++------
 1 file changed, 6 insertions(+), 6 deletions(-)

diff --git a/.github/ISSUE_TEMPLATE/bug_report.md b/.github/ISSUE_TEMPLATE/bug_report.md
index a124278ff05..ebb75445757 100644
--- a/.github/ISSUE_TEMPLATE/bug_report.md
+++ b/.github/ISSUE_TEMPLATE/bug_report.md
@@ -19,13 +19,13 @@ Steps to reproduce the behavior:
 **Expected behavior**
 A clear and concise description of what you expected to happen.
 
-**Desktop (please complete the following information):**
- - OS: [e.g. iOS]
- - Browser [e.g. chrome, safari]
- - Version [e.g. 22]
+**System details (please complete the following information):**
+ - OS: [e.g. MacOS, Windows, Linux]
+ - Java version: [e.g. Java 11, Java 17]
 
 **Additional information**
 Add any other context about the problem here.
 * Commit Hash:
-* Screenshots
-If applicable, add screenshots to help explain your problem.
+  Please provide the commit hash of the KeY version where the bug occurred.
+* Screenshots:
+  If applicable, add screenshots to help explain your problem.

From a049a72c5aa74d471cb6d38452d4b9e85688f93d Mon Sep 17 00:00:00 2001
From: Christian Hein <uaken@student.kit.edu>
Date: Tue, 31 Jan 2023 21:07:47 +0100
Subject: [PATCH 3/8] Fix use of unsupported string templates

Java (as opposed to Groovy and Kotlin) does not support string templates
of the form "$variable". Attempting to use the feature anyway results in
a string which literally contains the text "$variable".

See JEP 430: https://openjdk.org/jeps/430
---
 .../main/java/org/key_project/util/helper/FindResources.java  | 4 ++--
 .../src/main/java/org/key_project/util/lookup/Lookup.java     | 2 +-
 2 files changed, 3 insertions(+), 3 deletions(-)

diff --git a/key.util/src/main/java/org/key_project/util/helper/FindResources.java b/key.util/src/main/java/org/key_project/util/helper/FindResources.java
index 3ee49266f00..cae811196b8 100644
--- a/key.util/src/main/java/org/key_project/util/helper/FindResources.java
+++ b/key.util/src/main/java/org/key_project/util/helper/FindResources.java
@@ -56,7 +56,7 @@ public static <T> List<Path> getResources(String path, Class<T> clazz)
             Path dir = fs.getPath(path);
             return Files.list(dir).collect(Collectors.toList());
         }
-        throw new UnsupportedOperationException("Cannot list files for URL $dirURL");
+        throw new UnsupportedOperationException("Cannot list files for URL \"" + dirURL + "\"");
     }
 
     public static <T> List<Path> getResources(String path) throws URISyntaxException, IOException {
@@ -90,7 +90,7 @@ public static <T> Path getResource(String path, Class<T> clazz)
             Path dir = fs.getPath(path);
             return dir;
         }
-        throw new UnsupportedOperationException("Cannot list files for URL $dirURL");
+        throw new UnsupportedOperationException("Cannot list files for URL \"" + dirURL + "\"");
     }
 
     public static <T> Path getResource(String path) throws URISyntaxException, IOException {
diff --git a/key.util/src/main/java/org/key_project/util/lookup/Lookup.java b/key.util/src/main/java/org/key_project/util/lookup/Lookup.java
index dcee5d1c2a9..e8c3556a12a 100644
--- a/key.util/src/main/java/org/key_project/util/lookup/Lookup.java
+++ b/key.util/src/main/java/org/key_project/util/lookup/Lookup.java
@@ -86,7 +86,7 @@ public <T> T get(Class<T> service) {
             if (parent != null)
                 return parent.get(service);
             else
-                throw new IllegalStateException("Service $service not registered");
+                throw new IllegalStateException("Service \"" + service + "\" not registered");
         } else {
             return t.get(0);
         }

From c786aa67dc086e78e153f9ffc64330ca3671da49 Mon Sep 17 00:00:00 2001
From: Mattias Ulbrich <ulbrich@kit.edu>
Date: Wed, 1 Feb 2023 23:08:46 +0100
Subject: [PATCH 4/8] copy bug-report from gitlab to github

---
 .github/ISSUE_TEMPLATE/bug_report.md | 57 ++++++++++++++++++----------
 1 file changed, 38 insertions(+), 19 deletions(-)

diff --git a/.github/ISSUE_TEMPLATE/bug_report.md b/.github/ISSUE_TEMPLATE/bug_report.md
index ebb75445757..c2201e2638b 100644
--- a/.github/ISSUE_TEMPLATE/bug_report.md
+++ b/.github/ISSUE_TEMPLATE/bug_report.md
@@ -1,31 +1,50 @@
 ---
 name: Bug report
-about: Create a report to help us improve
+about: Create a report to help us improve KeY
 title: ''
 labels: ''
 assignees: ''
 
 ---
+<!-- 
+     Thank you for taking your time to make KeY a better tool!
+     Please replace the quoted lines (`> ...`) below with your text.
+--> 
 
-**Describe the bug**
-A clear and concise description of what the bug is.
+## Description
 
-**To Reproduce**
-Steps to reproduce the behavior:
-1. ...
-2. ...
-3. ...
+> Please describe your concern in detail!
 
-**Expected behavior**
-A clear and concise description of what you expected to happen.
+## Reproducible
+  
+> Is the issue reproducable?
+> Select one of: always, sometimes, random, have not tried, n/a 
 
-**System details (please complete the following information):**
- - OS: [e.g. MacOS, Windows, Linux]
- - Java version: [e.g. Java 11, Java 17]
+### Steps to reproduce 
 
-**Additional information**
-Add any other context about the problem here.
-* Commit Hash:
-  Please provide the commit hash of the KeY version where the bug occurred.
-* Screenshots:
-  If applicable, add screenshots to help explain your problem.
+> Describe the steps needed to reproduce the issue.
+
+1. ... 
+2. ... 
+3. ... 
+
+> What is your expected behavior and what was the actual behavior?
+
+### Additional information
+
+> Add more details here. In particular: if you have a stacktrace, put it here.
+
+---
+
+* Commit: <!-- SHA checksum of the git commit where you observed the problem-->
+
+<!--
+  If you have the permissions:
+  From the "labels" selection component on the right, please select appropriate labels:
+  * If you think this is a "bug" that should be fixed, please select Bug.
+  * Please select exactly one of the priority labels:  P:LOW, P:NORMAL, P:HIGH or P:URGENT.
+  * Please select those components (0, 1 or more) to which this issue refers 
+    (the labels with lilac background)
+-->
+
+<!-- END OF BUG TEMPLATE -->

From df1100a2e463e0e95abe16219065a5d050f5934f Mon Sep 17 00:00:00 2001
From: Mattias Ulbrich <ulbrich@kit.edu>
Date: Wed, 1 Feb 2023 23:17:18 +0100
Subject: [PATCH 5/8] Update feature_request.md

---
 .github/ISSUE_TEMPLATE/feature_request.md | 34 +++++++++++++++++------
 1 file changed, 25 insertions(+), 9 deletions(-)

diff --git a/.github/ISSUE_TEMPLATE/feature_request.md b/.github/ISSUE_TEMPLATE/feature_request.md
index bbcbbe7d615..1b4a57d312c 100644
--- a/.github/ISSUE_TEMPLATE/feature_request.md
+++ b/.github/ISSUE_TEMPLATE/feature_request.md
@@ -1,20 +1,36 @@
 ---
 name: Feature request
-about: Suggest an idea for this project
+about: Suggest an idea to improve KeY
 title: ''
 labels: ''
 assignees: ''
 
 ---
 
-**Is your feature request related to a problem? Please describe.**
-A clear and concise description of what the problem is. Ex. I'm always frustrated when [...]
+## Please describe your proposal in a ONE sentence
 
-**Describe the solution you'd like**
-A clear and concise description of what you want to happen.
+> One sentence describing your idea
 
-**Describe alternatives you've considered**
-A clear and concise description of any alternative solutions or features you've considered.
+## Underlying problem
 
-**Additional context**
-Add any other context or screenshots about the feature request here.
+> A clear and concise description of what the problem is. Ex. I'm always frustrated when [...]
+
+## Usage Scenario
+
+> Who (user scenario) would benefit from implementing the idea?
+> Describe a short use case scenario in which the suggested idea is featured.
+> Describe the solution you'd like: A clear and concise description of what you want to happen.
+
+## Alternatives 
+
+> A clear and concise description of any alternative solutions or features you've considered.
+> Why is the suggestion the best alternative?
+
+## Estimated effort
+
+> If you can: Estimate the effort that has to be invested to implement the feature request.
+> Is there still discussion needed? Or is it purely implementation? Expertises needed?
+
+## Additional context
+
+> Add any other context or screenshots about the feature request here.

From ab97843c28cf903c8012fec95793414435ddd4e4 Mon Sep 17 00:00:00 2001
From: Arne Keller <arne.keller@posteo.de>
Date: Thu, 2 Feb 2023 12:14:06 +0100
Subject: [PATCH 6/8] Fix branch name in Checkstyle script

---
 scripts/tools/checkstyle/GitDiffFilter.java          | 4 ++--
 scripts/tools/checkstyle/runIncrementalCheckstyle.sh | 2 +-
 2 files changed, 3 insertions(+), 3 deletions(-)

diff --git a/scripts/tools/checkstyle/GitDiffFilter.java b/scripts/tools/checkstyle/GitDiffFilter.java
index 27e847e1c73..e35b009a93f 100644
--- a/scripts/tools/checkstyle/GitDiffFilter.java
+++ b/scripts/tools/checkstyle/GitDiffFilter.java
@@ -26,9 +26,9 @@
  *
  * For <code>MERGE_BASE</code> the assignment
  *
- * <pre>MERGE_BASE=`git merge-base HEAD origin/master`</pre>
+ * <pre>MERGE_BASE=`git merge-base HEAD origin/main`</pre>
  *
- * proved sensible if merging against the master branch.
+ * proved sensible if merging against the main branch.
  * The <code>diffFile</code> can then be provided to the filter as
  * <pre> &lt;module name="GitDiffFilter"&gt;
  *   &lt;property name="diffFilename" value="diffFile" /&gt;
diff --git a/scripts/tools/checkstyle/runIncrementalCheckstyle.sh b/scripts/tools/checkstyle/runIncrementalCheckstyle.sh
index 0a5bff75ecc..7047b2854cc 100755
--- a/scripts/tools/checkstyle/runIncrementalCheckstyle.sh
+++ b/scripts/tools/checkstyle/runIncrementalCheckstyle.sh
@@ -5,7 +5,7 @@ cd `dirname $0`
 HOME_DIR=`readlink -f ../../..`
 DIFF_FILE=$HOME_DIR/checkstyle-diff.txt
 
-MERGE_BASE=`git merge-base HEAD origin/master`
+MERGE_BASE=`git merge-base HEAD origin/main`
 OPTIONS=""
 
 javac -cp checkstyle-10.6.0-all.jar -d . -sourcepath $HOME_DIR \

From 1b5361afaf7f6f04bbc2a4c10f8c46ecf86dcd2e Mon Sep 17 00:00:00 2001
From: Alexander Weigl <wadoon@users.noreply.github.com>
Date: Thu, 2 Feb 2023 14:58:57 +0100
Subject: [PATCH 7/8] Update tests.yml

Typo in the arguments to exclude optional test during unit-test job
---
 .github/workflows/tests.yml | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/.github/workflows/tests.yml b/.github/workflows/tests.yml
index 13725545afa..0de5a19947c 100644
--- a/.github/workflows/tests.yml
+++ b/.github/workflows/tests.yml
@@ -36,7 +36,7 @@ jobs:
       - name: Build with Gradle
         uses: gradle/gradle-build-action@v2.3.3
         with:
-          arguments: --continue -x key.core.symbolic_execution:test key.core.proof_references:test test
+          arguments: --continue -x :key.core.symbolic_execution:test -x :key.core.proof_references:test test
 
       - name: Upload test results
         uses: actions/upload-artifact@v3.1.1

From f16d3c705d3ec8bd7b4c242e18c8926dbe32328c Mon Sep 17 00:00:00 2001
From: Wolfram Pfeifer <94171076+WolframPfeifer@users.noreply.github.com>
Date: Thu, 2 Feb 2023 16:43:17 +0100
Subject: [PATCH 8/8] fix typo

---
 .github/ISSUE_TEMPLATE/bug_report.md | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/.github/ISSUE_TEMPLATE/bug_report.md b/.github/ISSUE_TEMPLATE/bug_report.md
index c2201e2638b..44c0688ae9e 100644
--- a/.github/ISSUE_TEMPLATE/bug_report.md
+++ b/.github/ISSUE_TEMPLATE/bug_report.md
@@ -17,7 +17,7 @@ assignees: ''
 
 ## Reproducible
   
-> Is the issue reproducable?
+> Is the issue reproducible?
 > Select one of: always, sometimes, random, have not tried, n/a 
 
 ### Steps to reproduce