print failing test cases on console using Github's annotations

Author: wadoon

.github/junit2annotations.py

@@ -0,0 +1,25 @@
+#!/usr/bin/python
+
+import sys
+import xml.etree.ElementTree as ET
+from pathlib import Path
+
+
+def main():
+  path = Path(r".") # path to the root dir from where you want to start searching
+
+  for t in path.glob("**/TEST-*xml"):
+    print(t)
+    tree = ET.parse(t)
+    root = tree.getroot()
+
+    for c in root:
+      failure = c.find("failure") # failure in test case
+      if failure is not None:
+	# ::error file={name},line={line},endLine={endLine},title={title}::{message}
+        case_name = c.attrib['name']
+        classname = c.attrib['classname']
+        message = failure.attrib['message'][0:80]
+        print(f"::error title=Testcase-missed,file={classname}::Error in test case '{case_name}' and {message}")
+
+if __name__=='__main__': main()

.github/workflows/tests.yml

@@ -100,3 +100,4 @@ jobs:
             **/build/test-results/*/*.xml
             key.core/build/reports/runallproofs/*
             **/build/reports/
+      - run: "python .github/junit2annotations.py"

build.gradle

@@ -74,11 +74,15 @@ subprojects {
     apply plugin: "com.diffplug.spotless"
     apply plugin: "checkstyle"
     apply plugin: "pmd"
+    apply plugin: 'jacoco'
     apply plugin: "org.checkerframework"
 
     group = rootProject.group
     version = rootProject.version
 
+    //conditionally enable jacoco coverage when `-DjacocoEnabled=true` is given on CLI.
+    def jacocoEnabled = System.properties.getProperty("jacocoEnabled") ?: "false"
+
     java {
         sourceCompatibility = 21
         targetCompatibility = 21
@@ -136,7 +140,7 @@ subprojects {
         systemProperty "testcases", "src/test/resources/testcase"
         systemProperty "TACLET_PROOFS", "tacletProofs"
         systemProperty "EXAMPLES_DIR", file("$rootProject/key.ui/examples")
-        systemProperty "RUNALLPROOFS_DIR", layout.buildDirectory.dir("report/runallproves")
+        systemProperty "RUNALLPROOFS_DIR", layout.buildDirectory.dir("report/runallproves").get().toString()
 
         systemProperty "key.disregardSettings", "true"
         maxHeapSize = "4g"
@@ -171,6 +175,10 @@ subprojects {
             outputs.upToDateWhen { false }
             showStandardStreams = true
         }
+
+        jacoco {
+            enabled = jacocoEnabled
+        }
     }
 
     tasks.register('testFast', Test) {
@@ -194,6 +202,10 @@ subprojects {
             // by assigning only 'failed' and 'skipped' events
             info.events = ["failed", "skipped"]
         }
+
+        jacoco {
+            enabled = jacocoEnabled
+        }
     }
 
     // The following two tasks can be used to execute main methods from the project
@@ -285,6 +297,23 @@ subprojects {
         }
     }
 
+    jacoco {
+        toolVersion = '0.8.12'
+    }
+
+    jacocoTestReport {
+        reports {
+            html.required = true
+            html.outputLocation = layout.buildDirectory.dir('jacocoHtml')
+            xml.required = true
+            csv.required = false
+        }
+    }
+
+    test.finalizedBy jacocoTestReport
+    testFast.finalizedBy jacocoTestReport
+
+
     spotless {
         // see https://github.com/diffplug/spotless/tree/main/plugin-gradle
 
@@ -543,13 +572,6 @@ tasks.register('alldocJar', Zip){
     destinationDirectory = layout.buildDirectory.dir("distribution")
 }
 
-//conditionally enable jacoco coverage when `-DjacocoEnabled=true` is given on CLI.
-def jacocoEnabled = System.properties.getProperty("jacocoEnabled") ?: "false"
-if (jacocoEnabled.toBoolean()) {
-    project.logger.lifecycle("Jacoco enabled. Test performance will be slower.")
-    apply from: rootProject.file("scripts/jacocokey.gradle")
-}
-
 
 @Memoized
 def getChangedFiles() {

key.core/build.gradle

@@ -133,7 +133,7 @@ tasks.register('testProveRules', Test) {
     description 'Proves KeY taclet rules tagged as lemma'
     group "verification"
     filter { includeTestsMatching "ProveRulesTest" }
-    //useJUnitPlatform() {includeTags "testProveRules"    }
+    jacoco { enabled = false }
 }
 
 tasks.register('testRunAllFunProofs', Test) {
@@ -142,6 +142,7 @@ tasks.register('testRunAllFunProofs', Test) {
     filter {
         includeTestsMatching "RunAllProofsFunctional"
     }
+    jacoco { enabled = false }
 }
 
 tasks.register('testRunAllInfProofs', Test) {
@@ -150,6 +151,7 @@ tasks.register('testRunAllInfProofs', Test) {
     filter {
         includeTestsMatching "RunAllProofsInfFlow"
     }
+    jacoco { enabled = false }
 }
 
 
@@ -159,6 +161,7 @@ tasks.register('testProveSMTLemmas', Test) {
     filter {
         includeTestsMatching "ProveSMTLemmasTest"
     }
+    jacoco { enabled = false }
 }
 
 // Run the tests for the new smt translation in strict mode
@@ -170,6 +173,7 @@ tasks.register('testStrictSMT', Test) {
     filter {
         includeTestsMatching "MasterHandlerTest"
     }
+    jacoco { enabled = false }
 }
 
 //Generation of the three version files within the resources by executing `git'.