Skip to content
Draft
Show file tree
Hide file tree
Changes from all commits
Commits
File filter

Filter by extension

Filter by extension


Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
18 changes: 9 additions & 9 deletions .github/workflows/nightlydeploy.yml
Original file line number Diff line number Diff line change
Expand Up @@ -24,8 +24,6 @@ jobs:
java-version: ${{ env.JAVA_VERSION }}
distribution: 'temurin'
cache: 'gradle'
gpg-private-key: ${{ secrets.GPG_PRIVATE_KEY }}
gpg-passphrase: ${{ secrets.GPG_PASSPHRASE }}

- name: Setup Gradle
uses: gradle/actions/setup-gradle@v6
Expand Down Expand Up @@ -57,6 +55,7 @@ jobs:
run: |
gh release delete nightly --yes --cleanup-tag


- name: Create nightly release
id: create_release
env:
Expand All @@ -66,13 +65,14 @@ jobs:
--prerelease --notes-start-tag KEY-2.12.3 \
nightly key.ui/build/libs/key-*-exe.jar key-javadoc.tar.xz

- run: export GPG_TTY=$(tty)
- name: Upload to SNAPSHOT repository
run: ./gradlew --parallel publishMavenJavaPublicationToKEYLABRepository

- name: Upload to MAVEN CENTRAL SNAPSHOT repository
run: |
./gradlew publishAndReleaseToMavenCentral publishMavenPublicationToKEYLABRepository
env:
BUILD_NUMBER: "SNAPSHOT"
GITLAB_DEPLOY_TOKEN: ${{ secrets.GITLAB_DEPLOY_TOKEN }}
# SIGNING_KEY_ID: ${{secrents.SIGNING_KEY_ID}}
# GPG_PRIVATE_KEY: ${{secrents.GPG_PRIVATE_KEY}}
# GPG_PASSPHRASE: ${{secrents.GPG_PASSPHRASE}}

ORG_GRADLE_PROJECT_signingInMemoryKey: ${{secrets.GPG_PRIVATE_KEY}}
ORG_GRADLE_PROJECT_signingInMemoryKeyPassword: ${{secrets.GPG_PASSPHRASE}}
ORG_GRADLE_PROJECT_mavenCentralUsername: ${{ secrets.SONATYPE_USERNAME }}
ORG_GRADLE_PROJECT_mavenCentralPassword: ${{ secrets.SONATYPE_PASSWORD }}
8 changes: 6 additions & 2 deletions README.md
Original file line number Diff line number Diff line change
@@ -1,6 +1,10 @@
# KeY -- Deductive Java Program Verifier

[![Tests](https://github.com/KeYProject/key/actions/workflows/tests.yml/badge.svg)](https://github.com/KeYProject/key/actions/workflows/tests.yml) [![CodeQL](https://github.com/KeYProject/key/actions/workflows/codeql.yml/badge.svg)](https://github.com/KeYProject/key/actions/workflows/codeql.yml) [![CodeQuality](https://github.com/KeYProject/key/actions/workflows/code_quality.yml/badge.svg)](https://github.com/KeYProject/key/actions/workflows/code_quality.yml)
[![Tests](https://github.com/KeYProject/key/actions/workflows/tests.yml/badge.svg)](https://github.com/KeYProject/key/actions/workflows/tests.yml) [![CodeQuality](https://github.com/KeYProject/key/actions/workflows/code_quality.yml/badge.svg)](https://github.com/KeYProject/key/actions/workflows/code_quality.yml)

![Maven metadata URL](https://img.shields.io/maven-metadata/v?metadataUrl=https%3A%2F%2Fcentral.sonatype.com%2Frepository%2Fmaven-snapshots%2Forg%2Fkey-project%2Fkey.core%2Fmaven-metadata.xml&label=maven%20snapshots)
![Maven metadata URL](https://img.shields.io/maven-metadata/v?metadataUrl=https%3A%2F%2Frepo1.maven.org%2Fmaven2%2Forg%2Fkey-project%2Fkey.core%2Fmaven-metadata.xml&label=maven%20central)


This repository is the home of the interactive theorem prover KeY for formal verification and analysis of Java programs. KeY comes as a standalone GUI application, which allows you to verify the functional correctness of Java programs with respect to formal specifications formulated in the Java Modeling Language JML. Moreover, KeY can also be used as a library e.g. for symbolic program execution, first order reasoning, or test case generation.

Expand Down Expand Up @@ -113,7 +117,7 @@ This is the KeY project - Integrated Deductive Software Design
Copyright (C) 2001-2011 Universität Karlsruhe, Germany
Universität Koblenz-Landau, Germany
and Chalmers University of Technology, Sweden
Copyright (C) 2011-2024 Karlsruhe Institute of Technology, Germany
Copyright (C) 2011-2026 Karlsruhe Institute of Technology, Germany
Technical University Darmstadt, Germany
Chalmers University of Technology, Sweden

Expand Down
203 changes: 78 additions & 125 deletions build.gradle
Original file line number Diff line number Diff line change
@@ -1,3 +1,7 @@
import com.vanniktech.maven.publish.JavaLibrary
import com.vanniktech.maven.publish.JavadocJar
import com.vanniktech.maven.publish.SourcesJar

plugins {
//Support for IntelliJ IDEA
//https://docs.gradle.org/current/userguide/idea_plugin.html
Expand All @@ -14,9 +18,7 @@ plugins {
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"
id "com.vanniktech.maven.publish" version "0.36.0" apply false
}


Expand All @@ -41,13 +43,13 @@ 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"
apply plugin: "com.vanniktech.maven.publish"
//apply plugin: "maven-publish"

group = rootProject.group
version = rootProject.version
Expand Down Expand Up @@ -81,13 +83,13 @@ subprojects {
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")))
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")
Expand Down Expand Up @@ -135,7 +137,6 @@ subprojects {
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
Expand All @@ -148,10 +149,10 @@ subprojects {
}

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

addTestListener(new TestListener() {
void beforeTest(TestDescriptor descriptor) {
Expand Down Expand Up @@ -284,130 +285,82 @@ subprojects {
// 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|//)')
}
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/'
}
}
mavenPublishing {
publishToMavenCentral()
signAllPublications()

configure(new JavaLibrary(
new JavadocJar.Javadoc(),
new SourcesJar.Sources()
))

pom {
name = it.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"
}
}
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)
}
developers {
developer {
id = 'key'
name = 'KeY Developers'
email = 'support@key-project.org'
url = "https://www.key-project.org/about/people/"
}
}
}
signing {
//sign publishing.publications.mavenJava
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/'
}
}
}
}

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")
)
}
}
publishing {
repositories {
maven {
name = "LOCAL"
url= uri("$rootDir/local")
}

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


tasks.register('start'){
description = "Use :key.ui:run instead"
doFirst {
Expand Down
Loading