Merge branch 'main' into weigl/keyformat

.github/pull_request_template.md

@@ -10,7 +10,7 @@ remain since they will be invisible when showing the PR.
 
 <!-- Please remove if this PR is not related to an issue. -->
 <!-- Please add number if it is in answer to an issue. -->
-This pull request addresses #.
+This pull request resolves #.
 
 ## Intended Change
 

key.core.example/build.gradle

@@ -1,5 +1,12 @@
+plugins {
+    id 'application'
+}
+
 description "Example project to use KeY's APIs"
 
+mainClassName ="org.key_project.Main"
+
 dependencies {
     implementation project(":key.core")
+    implementation 'ch.qos.logback:logback-classic:1.5.15'
 }

key.core.example/src/main/java/org/key_project/Main.java

@@ -38,6 +38,7 @@ public class Main {
      * @param args The start parameters.
      */
     public static void main(String[] args) {
+        LOGGER.info("Starting KeY example application.");
         File location = args.length == 1 ? new File(args[0]) : new File("example");
         // Path to the source code folder/file or to a *.proof file
         try {
@@ -90,6 +91,7 @@ private static void proveEnvironmemt(KeYEnvironment<?> env) {
             final List<Contract> proofContracts = getContracts(env);
 
             for (Contract contract : proofContracts) {
+                LOGGER.info("Found contract '" + contract.getDisplayName());
                 proveContract(env, contract);
             }
         } finally {

key.core.example/src/main/resources/logback.xml

@@ -0,0 +1,56 @@
+<configuration>
+    <!-- disables logback configuration messages on start up, see #1725 -->
+    <!--<statusListener class="ch.qos.logback.core.status.NopStatusListener" />-->
+
+    <timestamp key="timestamp" datePattern="yyyyMMdd'T'HHmmss"/>
+
+    <appender name="FILE" class="ch.qos.logback.core.FileAppender">
+        <file>${user.home}/.key/logs/key_${timestamp}.log</file>
+        <append>false</append>
+        <encoder>
+            <charset>UTF-8</charset>
+            <!-- replace newlines by \n to allow line-based filtering (see LogView) -->
+            <pattern>%date|%level|%thread|%logger|%file:%line|%replace(%msg){'[\n\r]','\\n'}|%replace(%ex){'[\n\r]','\\n'}%nopex|%n</pattern>
+            <outputPatternAsHeader>true</outputPatternAsHeader>
+        </encoder>
+    </appender>
+
+    <appender name="STDOUT" class="ch.qos.logback.core.ConsoleAppender">
+        <encoder>
+            <pattern>[%date{HH:mm:ss.SSS}] %highlight(%-5level) %cyan(%logger{0}) - %msg%ex%n</pattern>
+        </encoder>
+        <!--
+            The threshold of this filter is also selected by the command line option "verbose <int>" where
+                SILENT = 0 (completely off)
+                NORMAL = 1
+                INFO = 2
+                DEBUG = 3
+                TRACE = 4
+        -->
+        <filter class="ch.qos.logback.classic.filter.ThresholdFilter">
+            <level>INFO</level>
+        </filter>
+    </appender>
+
+    <root level="trace">
+        <appender-ref ref="STDOUT"/>
+        <appender-ref ref="FILE"/>
+    </root>
+
+    <!--
+        A logger for development, also print to CONSOLE. This logger is not restricted by any command line options.
+        You should not use this code on the master branch.
+    -->
+    <appender name="STDERR" class="ch.qos.logback.core.ConsoleAppender">
+        <encoder>
+            <pattern>[%relative] %highlight(%-5level) %cyan(%logger{0}): %msg %n</pattern>
+        </encoder>
+        <filter class="ch.qos.logback.classic.filter.ThresholdFilter">
+            <level>TRACE</level>
+        </filter>
+    </appender>
+    <logger name="key.devel" level="DEBUG">
+        <appender-ref ref="STDERR"/>
+    </logger>
+
+</configuration>