build.gradle

plugins {
    //Support for IntelliJ IDEA
    //https://docs.gradle.org/current/userguide/idea_plugin.html
    id("idea")

    //Support for Eclipse
    //https://docs.gradle.org/current/userguide/eclipse_plugin.html
    id("eclipse")  //support for Eclipse

    // Code formatting
    id "com.diffplug.spotless" version "8.4.0"

    // EISOP Checker Framework
    id "org.checkerframework" version "0.6.61"

    // Plugin for publishing via the new Nexus API
    id "io.github.gradle-nexus.publish-plugin" version "2.0.0"

    id "signing"
}


// Configure this project for use inside IntelliJ:
idea {
    module {
        downloadJavadoc = false
        downloadSources = true
    }
}

static def getDate() {
    return new Date().format('yyyyMMdd')
}

// The $BUILD_NUMBER is an environment variable set by Jenkins.
def build = System.env.BUILD_NUMBER == null ? "-dev" : "-${System.env.BUILD_NUMBER}"

group = "org.key-project"
version = "3.0.0$build"

subprojects {
    apply plugin: "java"
    apply plugin: "java-library"
    apply plugin: "maven-publish"
    apply plugin: "signing"       // GPG signing of artifacts, required by maven central
    apply plugin: "idea"
    apply plugin: "eclipse"

    apply plugin: "com.diffplug.spotless"
    apply plugin: "org.checkerframework"

    group = rootProject.group
    version = rootProject.version

    java {
        sourceCompatibility = 21
        targetCompatibility = 21
    }

    repositories {
        mavenCentral()
        maven { url = "https://git.key-project.org/api/v4/projects/35/packages/maven/" }
    }

    dependencies {
        implementation("org.slf4j:slf4j-api:2.0.17")
        testImplementation("ch.qos.logback:logback-classic:1.5.32")


        compileOnly("org.jspecify:jspecify:1.0.0")
        testCompileOnly("org.jspecify:jspecify:1.0.0")
        def eisop_version = "3.49.5-eisop1"
        compileOnly "io.github.eisop:checker-qual:$eisop_version"
        compileOnly "io.github.eisop:checker-util:$eisop_version"
        testCompileOnly "io.github.eisop:checker-qual:$eisop_version"
        checkerFramework "io.github.eisop:checker-qual:$eisop_version"
        checkerFramework "io.github.eisop:checker:$eisop_version"

        testImplementation("ch.qos.logback:logback-classic:1.5.32")
        testImplementation("org.assertj:assertj-core:3.27.7")
        testImplementation("ch.qos.logback:logback-classic:1.5.32")

        testImplementation(platform("org.junit:junit-bom:6.0.3"))
        testImplementation ("org.junit.jupiter:junit-jupiter-api")
        testImplementation ("org.junit.jupiter:junit-jupiter-params")
        testRuntimeOnly ("org.junit.jupiter:junit-jupiter-engine")
        testRuntimeOnly ("org.junit.platform:junit-platform-launcher")
        testImplementation ("org.assertj:assertj-core:3.27.7")
        testImplementation (project(':key.util'))
        testImplementation (testFixtures(project(":key.util")))

        // test fixtures
        testImplementation("com.fasterxml.jackson.dataformat:jackson-dataformat-yaml:2.21.3")
        testImplementation("com.fasterxml.jackson.datatype:jackson-datatype-jsr310:2.21.3")

        testRuntimeOnly 'org.junit.jupiter:junit-jupiter-engine'
    }

    tasks.withType(JavaCompile).configureEach {
        // Setting UTF-8 as the java source encoding.
        options.encoding = "UTF-8"
        // Setting the release to Java 21
        options.release = 21
    }

    tasks.withType(Javadoc).configureEach {
        failOnError = false
        options.addBooleanOption 'Xdoclint:none', true
        //options.verbose()
        options.encoding = 'UTF-8'
        options.addBooleanOption('html5', true)
    }

    tasks.withType(Test).configureEach {//Configure all tests
        def examplesDir = rootProject.layout.projectDirectory.dir("key.ui/examples").getAsFile()
        def runAllProofsReportDir = layout.buildDirectory.dir("report/runallproves/").get().getAsFile()
        systemProperty "test-resources", "src/test/resources"
        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").get().toString()

        systemProperty "key.disregardSettings", "true"
        maxHeapSize = "4g"

        forkEvery = 0 //default
        maxParallelForks = 1 // weigl: test on master

        useJUnitPlatform {
            includeEngines 'junit-jupiter'
        }

        // these seems to be missing starting with Gradle 9
        testClassesDirs = sourceSets.test.output.classesDirs
        classpath = sourceSets.test.runtimeClasspath
    }


    test {
        // Before we switched to JUnit 5, we used JUnit 4 with a customized discovery of test class.
        // This discovery called AutoSuite and searched in the compiled classes. AutoSuite was
        // necessary due to bugs caused in some execution order.
        // AutoSuites made the test order deterministic. A last known commit to find AutoSuite (for the case),
        // is 980294d04008f6b3798986bce218bac2753b4783.

        useJUnitPlatform {
            excludeTags "owntest", "interactive", "performance"
        }

        addTestListener(new TestListener() {
                void afterTest(TestDescriptor desc, TestResult result) {
                    logger.error("${result.getResultType()}: ${desc.getClassName()}#${desc.getName()}")
                }
            })

        addTestListener(new TestListener() {
            void beforeTest(TestDescriptor descriptor) {
                logger.error("> ${descriptor.getClassName()}#${descriptor.getName()}")
            }
        })

        testLogging {
            outputs.upToDateWhen { false }
            showStandardStreams = true
        }
    }

    tasks.register('testFast', Test) {
        group = "verification"
        useJUnitPlatform {
            excludeTags "slow", "performance", "interactive"
        }

        testLogging {
            // set options for log level LIFECYCLE
            events = ["failed"]
            exceptionFormat = "short"

            // set options for log level DEBUG
            debug {
                events "started", "skipped", "failed"
                exceptionFormat = "full"
            }

            // remove standard output/error logging from --info builds
            // by assigning only 'failed' and 'skipped' events
            info.events = ["failed", "skipped"]
        }
    }

    // The following two tasks can be used to execute main methods from the project
    // The main class is set via "gradle -DmainClass=... execute --args ..."
    // see https://stackoverflow.com/questions/21358466/gradle-to-execute-java-class-without-modifying-build-gradle
    tasks.register('execute', JavaExec) {
        description = 'Execute main method from the project. Set main class via "gradle -DmainClass=... execute --args ..."'
        group = "application"
        mainClass.set(System.getProperty('mainClass'))
        classpath = sourceSets.main.runtimeClasspath
    }

    tasks.register('executeInTests', JavaExec) {
        description = 'Execute main method from the project (tests loaded). Set main class via "gradle -DmainClass=... execute --args ..."'
        group = "application"
        mainClass.set(System.getProperty('mainClass'))
        classpath = sourceSets.test.runtimeClasspath
    }

    tasks.register('sourcesJar', Jar) {
        description = 'Create a jar file with the sources from this project'
        from sourceSets.main.allJava
        archiveClassifier = 'sources'
    }

    tasks.register('javadocJar', Jar) {
        description = 'Create a jar file with the javadocs from this project'
        from javadoc
        archiveClassifier = 'javadoc'
    }

    eclipse { //configures the generated .project and .classpath files.
        classpath {
            file {
                whenMerged { // This adds the exclude entry for every resource and antlr folder.
                    //As eclipse is so stupid, that it does not distuinguish between resource and java folder correctly.
                    entries.findAll { it.path.endsWith('src/test/antlr') }.each { it.excludes = ["**/*.java"] }
                    entries.findAll { it.path.endsWith('/resources') }.each { it.excludes = ["**/*.java"] }
                }
            }
        }
    }

    spotless {
        // see https://github.com/diffplug/spotless/tree/main/plugin-gradle

        // optional: limit format enforcement to just the files changed by this feature branch
        // ratchetFrom 'origin/master'

        format('Key') {
            // define the files to apply `misc` to
            //target '*.gradle', '*.md', '.gitignore'
            target 'src/main/resources/**/*.key'
            trimTrailingWhitespace()
            //indentWithSpaces(4)       // this does not really work
            endWithNewline()
            // TODO: license headers are problematic at the moment,
            //  see https://git.key-project.org/key/key/-/wikis/KaKeY%202022-09-30
            //licenseHeaderFile("$rootDir/gradle/header", '\\s*\\\\\\w+')
        }

        antlr4 {
            target 'src/*/antlr4/**/*.g4' // default value, you can change if you want
            //licenseHeaderFile "$rootDir/gradle/header"
        }

        java {
            //target("*.java")
            // don't need to set target, it is inferred from java

            // We ignore the build folder to avoid double checks and checks of generated code.
            targetExclude 'build/**'

            // allows us to use spotless:off / spotless:on to keep pre-formatted sections
            // MU: Only ... because of the eclipse(...) below, it is "@formatter:off" and "@formatter:on"
            // that must be used instead.
            toggleOffOn()

            removeUnusedImports()

            /* When new options are added in new versions of the Eclipse formatter, the easiest way is to export the new
             * style file from the Eclipse GUI and then use the CodeStyleMerger tool in
             * "$rootDir/scripts/tools/checkstyle/CodeStyleMerger.java" to merge the old and the new style files,
             * i.e. "java CodeStyleMerger.java <oldStyleFile> <newStyleFile> keyCodeStyle.xml". The tool adds all
             * entries with keys that were not present in the old file and optionally overwrites the old entries. The
             * file is output with ordered keys, such that the file can easily be diffed using git.
             */
            eclipse().configFile("$rootDir/scripts/tools/checkstyle/keyCodeStyle.xml")
            trimTrailingWhitespace()        // not sure how to set this in the xml file ...
            //googleJavaFormat().aosp().reflowLongStrings()

            // note: you can use an empty string for all the imports you didn't specify explicitly,
            // '|' to join group without blank line, and '\\#` prefix for static imports
            importOrder('java|javax', 'de.uka', 'org.key_project', '', '\\#')

            // specific delimiter: normally just 'package', but spotless crashes for files in default package
            // (see https://github.com/diffplug/spotless/issues/30), therefore 'import' is needed. '//' is for files
            // with completely commented out code (which would probably better just be removed in future).
            if (project.name == 'recoder') {
                licenseHeaderFile("$rootDir/gradle/header-recoder", '(package|import|//)')
            } else {
                licenseHeaderFile("$rootDir/gradle/header", '(package|import|//)')
            }
        }
    }

    afterEvaluate { // required so project.description is non-null as set by sub build.gradle
        publishing {
            publications {
                mavenJava(MavenPublication) {
                    from components.java
                    artifact sourcesJar
                    artifact javadocJar
                    pom {
                        name = projects.name
                        description = project.description
                        url = 'https://key-project.org/'

                        licenses {
                            license {
                                name = "GNU General Public License (GPL), Version 2"
                                url = "https://www.gnu.org/licenses/old-licenses/gpl-2.0.html"
                            }
                        }

                        developers {
                            developer {
                                id = 'key'
                                name = 'KeY Developers'
                                email = 'support@key-project.org'
                                url = "https://www.key-project.org/about/people/"
                            }
                        }
                        scm {
                            connection = 'scm:git:git://github.com/keyproject/key.git'
                            developerConnection = 'scm:git:git://github.com/keyproject/key.git'
                            url = 'https://github.com/keyproject/key/'
                        }
                    }
                }
            }
            repositories {
                maven {
                    name = "LOCAL"
                    url= uri("$rootDir/local")
                }

                maven { // deployment to git.key-project.org/key-public/key
                    name = "KEYLAB"
                    url = uri("https://git.key-project.org/api/v4/projects/35/packages/maven")
                    credentials(HttpHeaderCredentials) {
                        def userToken = envOrPropertyValue("GITLAB_USER_TOKEN")
                        def deployToken = envOrPropertyValue("GITLAB_DEPLOY_TOKEN")
                        def ciToken = envOrPropertyValue("GITLAB_CIJOB_TOKEN")

                        if (userToken != "") {
                            name = 'Private-Token'
                            value = userToken
                        } else if(deployToken != "") {
                            name = 'Deploy-Token'
                            value = deployToken
                        }  else {
                            name = 'Job-Token'
                            value = ciToken
                        }
                    }
                    authentication {
                        header(HttpHeaderAuthentication)
                    }
                }
            }
        }
        signing {
            //sign publishing.publications.mavenJava
        }
    }
}

signing {
    // does not work
    if(System.getenv("GPG_PRIVATE_KEY") == null) {
        useGpgCmd() // works better than the Java implementation, which requires PGP keyrings.
    } else{
        useInMemoryPgpKeys(
                System.getenv("SIGNING_KEY_ID"),
                System.getenv("GPG_PRIVATE_KEY"),
                System.getenv("GPG_PASSPHRASE")
        )
    }
}

nexusPublishing {
    repositories {
        central {
            nexusUrl = uri("https://ossrh-staging-api.central.sonatype.com/service/local/")
            snapshotRepositoryUrl = uri("https://central.sonatype.com/repository/maven-snapshots/")

            stagingProfileId.set("org.key-project")

            /**
             * To be able to publish things on Maven Central, you need two things:
             *
             * (1) a JIRA account with permission on group-id `org.key-project`
             * (2) a keyserver-published GPG (w/o sub-keys)
             *
             * Your `$HOME/.gradle/gradle.properties` should like this:
             * ```
             * signing.keyId=YourKeyId
             * signing.password=YourPublicKeyPassword
             * ossrhUsername=your-jira-id
             * ossrhPassword=your-jira-password
             * ```
             *
             * You can test signing with `gradle sign`, and publish with `gradle publish`.
             * https://central.sonatype.org/publish/publish-guide/
             */
            username = envOrPropertyValue("ossrhUsername")
            password = envOrPropertyValue("ossrhPassword")
        }
    }
}

tasks.register('start'){
    description = "Use :key.ui:run instead"
    doFirst {
        println "Use :key.ui:run instead"
    }
}

// Generation of a JavaDoc across sub projects.
tasks.register('alldoc', Javadoc){
    group = "documentation"
    description = "Generate a JavaDoc across sub projects"
    def projects = subprojects
    //key.ui javadoc is broken
    source projects.collect { it.sourceSets.main.allJava }
    classpath = files(projects.collect { it.sourceSets.main.compileClasspath })
    destinationDir = layout.buildDirectory.dir("docs/javadoc").getOrNull().getAsFile()


    configure(options) {
        showFromPrivate()
        options.addBooleanOption('html5', true)
        encoding = 'UTF-8'
        addBooleanOption 'Xdoclint:none', true
        // overview = new File( projectDir, 'src/javadoc/package.html' )
        //stylesheetFile = new File( projectDir, 'src/javadoc/stylesheet.css' )
        windowTitle = 'KeY API Documentation'
        docTitle = "KeY JavaDoc ($project.version) -- ${getDate()}"
        bottom = "Copyright &copy; 2003-2026 <a href=\"http://key-project.org\">The KeY-Project</a>."
        use = true
        links += "https://docs.oracle.com/en/java/javase/21/docs/api/"
        links += "https://www.javadoc.io/doc/org.slf4j/slf4j-api/2.0.17/"
        links += "https://www.javadoc.io/doc/org.antlr/antlr4-runtime/4.13.2/"
        links +="https://www.javadoc.io/doc/ch.qos.logback/logback-classic/1.5.32/"
        links +="https://www.javadoc.io/doc/com.formdev/flatlaf/3.7/"
        links +="https://www.javadoc.io/doc/com.miglayout/miglayout-swing/11.4.3/"
        links +="https://www.javadoc.io/doc/com.squareup/javapoet/1.13.0/"
        //links +="https://www.javadoc.io/doc/de.unruh/scala-isabelle_2.13/0.4.5/"
        links +="https://www.javadoc.io/doc/info.picocli/picocli/4.7.7/"
        links +="https://www.javadoc.io/doc/org.antlr/ST4/4.3.4/"
        links +="https://www.javadoc.io/doc/org.antlr/antlr4-runtime/4.13.2/"
        links +="https://www.javadoc.io/doc/org.jspecify/jspecify/1.0.0/"
        links +="https://www.javadoc.io/doc/org.slf4j/slf4j-api/2.0.17/"

        linkSource()
        author()
        version()

        group("key.core.infflow", "de.uka.ilkd.key.informationflow")
        group("key.core", "de.uka.ilkd.key")
        group("key.util", "org.key_project.util")
        group("key.ui", "org.key_project.util.java",
                "de.uka.ilkd.key.core", "de.uka.ilkd.key.gui",
                "de.uka.ilkd.key.proof", "de.uka.ilkd.key.ui","de.uka.ilkd.key.util")
        group("key.core.wd", "de.uka.ilkd.key.wd")
        group("key.core.testgen", "de.uka.ilkd.key.testgen")
        group("key.ncore", "org.key_project.logic")
        group("key.ncore.calculus", "org.key_project.prover")

        /*
        group("keyext.isabelletranslation", "org.key_project.isabelletranslation")
        group("keyext.proofmanagement", "org.key_project.proofmanagement")
        group("keyext.slicing", "org.key_project.slicing")
        group("keyext.ui.testgen", "de.uka.ilkd.key.gui.testgen")
        group("keyext.exploration","org.key_project.exploration")
        group("keyext.caching", "de.uka.ilkd.key.gui.plugins.caching")
        group("key.core.symbolic_execution",// "de.uka.ilkd.key.proof",
                "de.uka.ilkd.key.rule.label", "de.uka.ilkd.key.strategy",
                "de.uka.ilkd.key.symbolic_execution")
        group("key.core.proof_references", "de.uka.ilkd.key.proof_references")*/
    }
}

// Creates a jar file with the javadoc over all sub projects.
tasks.register('alldocJar', Zip){
    dependsOn alldoc
    description = 'Create a jar file with the javadoc over all sub projects'
    from alldoc
    archiveFileName = "key-api-doc-${project.version}.zip"
    destinationDirectory = layout.buildDirectory.dir("distribution").getOrNull()
}

//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")
}


def envOrPropertyValue(String key) {
    if(key in System.getenv()) {
        return System.getenv(key)
    }else{
        return project.properties.getOrDefault(key, "")
    }
}