From b92708b9e7b4cef656d969d245b12ede7dec6538 Mon Sep 17 00:00:00 2001 From: Alejandro Serrano Date: Sun, 30 Apr 2023 10:19:21 +0200 Subject: [PATCH] Update Kotlin and Arrow versions (#60) Co-authored-by: Simon Vergauwen --- analysis/common/build.gradle.kts | 3 ++ .../analysis/solver/check/EntryPoint.kt | 2 +- .../solver/collect/FromAnnotations.kt | 4 +- .../phases/analysis/solver/errors/ErrorIds.kt | 48 +++++++++---------- .../analysis/solver/errors/ErrorMessages.kt | 48 ++++++++----------- analysis/example/build.gradle.kts | 5 ++ analysis/java-gradle-plugin/build.gradle.kts | 7 +++ analysis/java-plugin/build.gradle.kts | 3 ++ .../kotlin-gradle-plugin/build.gradle.kts | 7 +++ analysis/kotlin-plugin/build.gradle.kts | 3 ++ .../meta/plugins/analysis/phases/ir/Hints.kt | 4 +- analysis/laws/build.gradle.kts | 4 ++ analysis/types/build.gradle.kts | 4 ++ build.gradle.kts | 18 +------ gradle/projects.libs.versions.toml | 16 +++---- gradle/wrapper/gradle-wrapper.properties | 2 +- 16 files changed, 95 insertions(+), 83 deletions(-) diff --git a/analysis/common/build.gradle.kts b/analysis/common/build.gradle.kts index d85ec320..dbaf91f0 100644 --- a/analysis/common/build.gradle.kts +++ b/analysis/common/build.gradle.kts @@ -10,6 +10,9 @@ plugins { kotlin { explicitApi = null + jvmToolchain { + (this as JavaToolchainSpec).languageVersion.set(JavaLanguageVersion.of(11)) + } } dependencies { diff --git a/analysis/common/src/main/kotlin/arrow/meta/plugins/analysis/phases/analysis/solver/check/EntryPoint.kt b/analysis/common/src/main/kotlin/arrow/meta/plugins/analysis/phases/analysis/solver/check/EntryPoint.kt index a6e2e0c0..6aad5f6b 100644 --- a/analysis/common/src/main/kotlin/arrow/meta/plugins/analysis/phases/analysis/solver/check/EntryPoint.kt +++ b/analysis/common/src/main/kotlin/arrow/meta/plugins/analysis/phases/analysis/solver/check/EntryPoint.kt @@ -143,7 +143,7 @@ public fun SolverState.checkDeclarationConstraints( /** * Only elements which are not * - inside another "callable declaration" (function, property, etc.) (b/c this is not yet - * supported) + * supported) * - or constructors (b/c they are handled at the level of class) */ private fun Declaration.shouldBeAnalyzed() = !(this.parents.any { it is CallableDeclaration }) diff --git a/analysis/common/src/main/kotlin/arrow/meta/plugins/analysis/phases/analysis/solver/collect/FromAnnotations.kt b/analysis/common/src/main/kotlin/arrow/meta/plugins/analysis/phases/analysis/solver/collect/FromAnnotations.kt index 3bbc6276..3015220e 100644 --- a/analysis/common/src/main/kotlin/arrow/meta/plugins/analysis/phases/analysis/solver/collect/FromAnnotations.kt +++ b/analysis/common/src/main/kotlin/arrow/meta/plugins/analysis/phases/analysis/solver/collect/FromAnnotations.kt @@ -143,8 +143,8 @@ internal fun SolverState.parseFormula( """ (declare-fun this () $VALUE_TYPE) (declare-fun $RESULT_VAR_NAME () $VALUE_TYPE) - """.trimIndent( - ) + """ + .trimIndent() val fullString = "$params\n$deps\n$rest\n(assert $formula)" return solver.parse(fullString) } diff --git a/analysis/common/src/main/kotlin/arrow/meta/plugins/analysis/phases/analysis/solver/errors/ErrorIds.kt b/analysis/common/src/main/kotlin/arrow/meta/plugins/analysis/phases/analysis/solver/errors/ErrorIds.kt index cf59800b..f9501eea 100644 --- a/analysis/common/src/main/kotlin/arrow/meta/plugins/analysis/phases/analysis/solver/errors/ErrorIds.kt +++ b/analysis/common/src/main/kotlin/arrow/meta/plugins/analysis/phases/analysis/solver/errors/ErrorIds.kt @@ -44,8 +44,8 @@ sealed interface ErrorIds { The compiler won't catch these errors in its own analysis phase (like it would do with a type error), since this is perfectly good code. However, it seems desirable for the programmer to know that a particular language feature cannot be used in these blocks. - """.trimIndent( - ) + """ + .trimIndent() } enum class Laws : ErrorIds { @@ -64,8 +64,8 @@ sealed interface ErrorIds { - It must call **exactly one** function at the end, - The call must use the parameters **in order**. - """.trimIndent( - ) + """ + .trimIndent() } enum class Unsupported : ErrorIds { @@ -92,8 +92,8 @@ sealed interface ErrorIds { ```kotlin val wrong = 1 / 0 // does not satisfy '0 != 0' in Int.div law ``` - """.trimIndent( - ) + """ + .trimIndent() }, UnsatBodyPost { override val shortDescription: String @@ -113,8 +113,8 @@ sealed interface ErrorIds { // does not satisfy 'x + x > 1' } ``` - """.trimIndent( - ) + """ + .trimIndent() }, UnsatInvariants { override val shortDescription: String @@ -133,8 +133,8 @@ sealed interface ErrorIds { ... } ``` - """.trimIndent( - ) + """ + .trimIndent() } } @@ -154,8 +154,8 @@ sealed interface ErrorIds { ... } ``` - """.trimIndent( - ) + """ + .trimIndent() }, InconsistentDefaultValues { override val fullDescription: String @@ -170,8 +170,8 @@ sealed interface ErrorIds { ... } ``` - """.trimIndent( - ) + """ + .trimIndent() }, InconsistentConditions { override val fullDescription: String @@ -192,8 +192,8 @@ sealed interface ErrorIds { } } ``` - """.trimIndent( - ) + """ + .trimIndent() override val level: SeverityLevel get() = SeverityLevel.Warning @@ -205,8 +205,8 @@ sealed interface ErrorIds { The post-conditions gathered after calling a function imply that this function could not be called at all. _This is really uncommon in practice_. - """.trimIndent( - ) + """ + .trimIndent() override val level: SeverityLevel get() = SeverityLevel.Warning @@ -225,8 +225,8 @@ sealed interface ErrorIds { } ``` - """.trimIndent( - ) + """ + .trimIndent() }; override val shortDescription: String @@ -245,8 +245,8 @@ sealed interface ErrorIds { the one declared in its parent. This guarantees that we can always replace a call to the parent with a call to the child (Liskov Substitution Principle). - """.trimIndent( - ) + """ + .trimIndent() }, NotStrongerPostcondition { override val shortDescription: String @@ -259,8 +259,8 @@ sealed interface ErrorIds { the one declared in its parent. This guarantees that we can always replace a call to the parent with a call to the child (Liskov Substitution Principle). - """.trimIndent( - ) + """ + .trimIndent() } } diff --git a/analysis/common/src/main/kotlin/arrow/meta/plugins/analysis/phases/analysis/solver/errors/ErrorMessages.kt b/analysis/common/src/main/kotlin/arrow/meta/plugins/analysis/phases/analysis/solver/errors/ErrorMessages.kt index a443cc3b..7ee25be0 100644 --- a/analysis/common/src/main/kotlin/arrow/meta/plugins/analysis/phases/analysis/solver/errors/ErrorMessages.kt +++ b/analysis/common/src/main/kotlin/arrow/meta/plugins/analysis/phases/analysis/solver/errors/ErrorMessages.kt @@ -31,6 +31,7 @@ import org.sosy_lab.java_smt.api.Model * // c -> h() * // d -> f(g(2), h()) * ``` + * * We can leverage this information to write better error messages. If we have a constraint which * states b > 0, we can replace it with g(2) > 0. */ @@ -41,7 +42,6 @@ object ErrorMessages { * SMT formulae. * * For example, we cannot translate method calls to SMT: - * * ```kotlin * fun f(xs: List[String]): String { * pre({ !xs.get(0).isEmpty() }) { ... } @@ -95,14 +95,13 @@ object ErrorMessages { * * See [arrow.meta.plugins.analysis.phases.analysis.solver.checkImplicationOf] for the code which * produces the errors. - * * - The _one_ constraint name and Boolean formula which could not be satisfied. * - A _counter-example_ (also called a _model_), which is an assignment of values to - * variableswhich show a specific instance in which the constraint is false. + * variableswhich show a specific instance in which the constraint is false. * - In the `f` function above in the `UnsatBodyPost` epigraph, one such counter-example is `x == - * 0`, since in that case `0 + 0 > 1` is false. + * 0`, since in that case `0 + 0 > 1` is false. * - By looking at the values of the model for the arguments, we can derive one specific trace for - * which the function fails. + * which the function fails. */ object Unsatisfiability { @@ -111,7 +110,6 @@ object ErrorMessages { * property, function) call are not satisfied. * * For example: - * * ```kotlin * val wrong = 1 / 0 // does not satisfy '0 != 0' in Int.div law * ``` @@ -126,8 +124,8 @@ object ErrorMessages { | -> unsatisfiable constraint: `${callPreCondition.formula.dumpKotlinLike()}` | -> ${template(callPreCondition, this)} | -> ${branch(branch)} - """.trimMargin( - ) + """ + .trimMargin() /** * (attached to the return value) @@ -135,7 +133,6 @@ object ErrorMessages { * the post-condition declared in a function body is not true. * * For example: - * * ```kotlin * fun f(x: Int): Int { * pre(x >= 0) { "non-negative" } @@ -152,15 +149,14 @@ object ErrorMessages { ): String = """|declaration `${declaration.name}` fails to satisfy the post-condition: ${postCondition.formula.dumpKotlinLike()} | -> ${branch(branch)} - """.trimMargin( - ) + """ + .trimMargin() /** * (attached to the new value): the invariant declared for a mutable variable is not satisfied * by the new value. * * For example: - * * ```kotlin * fun g(): Int { * var r = 1.invariant({ it > 0 }) { "it > 0" } @@ -179,8 +175,8 @@ object ErrorMessages { """|invariants are not satisfied in `${expression.text}` | -> unsatisfiable constraint: `${constraint.formula.dumpKotlinLike()}` | -> ${branch(branch)} - """.trimMargin( - ) + """ + .trimMargin() } /** @@ -205,7 +201,6 @@ object ErrorMessages { * The set of pre-conditions given to the function leaves no possible way to call the function. * * For example: - * * ```kotlin * fun h(x: Int): Int { * pre({ x > 0 }) { "greater than 0" } @@ -226,7 +221,6 @@ object ErrorMessages { * The default values do not satisfy the pre-conditions. * * For example: - * * ```kotlin * fun h(x: Int = 0): Int { * pre({ x > 0 }) { "greater than 0" } @@ -245,7 +239,6 @@ object ErrorMessages { * condition it hangs upon conflicts with the rest of the information about the function. * * For example, if a condition goes against a pre-condition: - * * ```kotlin * fun i(x: Int): Int { * pre({ x > 0 }) { "greater than 0" } @@ -265,8 +258,8 @@ object ErrorMessages { ): String = """|unreachable code due to conflicting conditions: ${unsatCore.dumpKotlinLike()} | -> ${branch(branch)} - """.trimMargin( - ) + """ + .trimMargin() /** * (attached to the function call): the post-conditions gathered after calling a function imply @@ -278,15 +271,14 @@ object ErrorMessages { ): String = """|unreachable code due to post-conditions: ${unsatCore.dumpKotlinLike()} | -> ${branch(branch)} - """.trimMargin( - ) + """ + .trimMargin() /** * (attached to a local declaration): there is no way in which the invariant attached to a * declaration may be satisfied. * * For example: - * * ```kotlin * fun j(x: Int): Int { * pre({ x > 0 }) { "greater than 0" } @@ -301,22 +293,22 @@ object ErrorMessages { ): String = """|invariants are inconsistent: ${it.dumpKotlinLike()} | -> ${branch(branch)} - """.trimMargin( - ) + """ + .trimMargin() } object Liskov { internal fun KotlinPrinter.notWeakerPrecondition(constraint: NamedConstraint): String = """|pre-condition `${constraint.msg}` is not weaker than those from overridden members | -> problematic constraint: `${constraint.formula.dumpKotlinLike()}` - """.trimMargin( - ) + """ + .trimMargin() internal fun KotlinPrinter.notStrongerPostcondition(constraint: NamedConstraint): String = """|post-condition `${constraint.msg}` from overridden member is not satisfied | -> problematic constraint: `${constraint.formula.dumpKotlinLike()}` - """.trimMargin( - ) + """ + .trimMargin() } object Exception { diff --git a/analysis/example/build.gradle.kts b/analysis/example/build.gradle.kts index 61a6624c..4d9b402e 100644 --- a/analysis/example/build.gradle.kts +++ b/analysis/example/build.gradle.kts @@ -4,12 +4,17 @@ plugins { id(libs.plugins.kotlin.multiplatform.get().pluginId) alias(libs.plugins.arrowGradleConfig.kotlin) alias(libs.plugins.arrowGradleConfig.formatter) + alias(libs.plugins.arrowGradleConfig.versioning) } kotlin { explicitApi = null + jvmToolchain { + (this as JavaToolchainSpec).languageVersion.set(JavaLanguageVersion.of(11)) + } + sourceSets { commonMain { dependencies { diff --git a/analysis/java-gradle-plugin/build.gradle.kts b/analysis/java-gradle-plugin/build.gradle.kts index fa84d345..b6726ad7 100644 --- a/analysis/java-gradle-plugin/build.gradle.kts +++ b/analysis/java-gradle-plugin/build.gradle.kts @@ -16,6 +16,13 @@ tasks.processResources { } } +kotlin { + explicitApi = null + jvmToolchain { + (this as JavaToolchainSpec).languageVersion.set(JavaLanguageVersion.of(11)) + } +} + dependencies { api(libs.arrowGradlePluginCommons) runtimeOnly(libs.classgraph) diff --git a/analysis/java-plugin/build.gradle.kts b/analysis/java-plugin/build.gradle.kts index 7db84249..41e8bcfa 100644 --- a/analysis/java-plugin/build.gradle.kts +++ b/analysis/java-plugin/build.gradle.kts @@ -9,6 +9,9 @@ plugins { kotlin { explicitApi = null + jvmToolchain { + (this as JavaToolchainSpec).languageVersion.set(JavaLanguageVersion.of(11)) + } } dependencies { diff --git a/analysis/kotlin-gradle-plugin/build.gradle.kts b/analysis/kotlin-gradle-plugin/build.gradle.kts index 5db74668..c2151c82 100644 --- a/analysis/kotlin-gradle-plugin/build.gradle.kts +++ b/analysis/kotlin-gradle-plugin/build.gradle.kts @@ -16,6 +16,13 @@ tasks.processResources { } } +kotlin { + explicitApi = null + jvmToolchain { + (this as JavaToolchainSpec).languageVersion.set(JavaLanguageVersion.of(11)) + } +} + dependencies { api(libs.arrowGradlePluginCommons) runtimeOnly(libs.classgraph) diff --git a/analysis/kotlin-plugin/build.gradle.kts b/analysis/kotlin-plugin/build.gradle.kts index a2ea89e4..c99d8858 100644 --- a/analysis/kotlin-plugin/build.gradle.kts +++ b/analysis/kotlin-plugin/build.gradle.kts @@ -10,6 +10,9 @@ plugins { kotlin { explicitApi = null + jvmToolchain { + (this as JavaToolchainSpec).languageVersion.set(JavaLanguageVersion.of(11)) + } } dependencies { diff --git a/analysis/kotlin-plugin/src/main/kotlin/arrow/meta/plugins/analysis/phases/ir/Hints.kt b/analysis/kotlin-plugin/src/main/kotlin/arrow/meta/plugins/analysis/phases/ir/Hints.kt index 52d26b16..0c2e0e51 100644 --- a/analysis/kotlin-plugin/src/main/kotlin/arrow/meta/plugins/analysis/phases/ir/Hints.kt +++ b/analysis/kotlin-plugin/src/main/kotlin/arrow/meta/plugins/analysis/phases/ir/Hints.kt @@ -32,8 +32,8 @@ fun hints(descriptor: ModuleDescriptor, packages: Set): String { | |@PackagesWithLaws([$packageList]) |class hints_$hintPackageName { } - |""".trimMargin( - ) + |""" + .trimMargin() } enum class HintState { diff --git a/analysis/laws/build.gradle.kts b/analysis/laws/build.gradle.kts index 99abad76..8c1875ee 100644 --- a/analysis/laws/build.gradle.kts +++ b/analysis/laws/build.gradle.kts @@ -12,6 +12,10 @@ plugins { kotlin { explicitApi = null + jvmToolchain { + (this as JavaToolchainSpec).languageVersion.set(JavaLanguageVersion.of(11)) + } + sourceSets { commonMain { dependencies { diff --git a/analysis/types/build.gradle.kts b/analysis/types/build.gradle.kts index 4a0a1e62..46fc442f 100644 --- a/analysis/types/build.gradle.kts +++ b/analysis/types/build.gradle.kts @@ -11,6 +11,10 @@ plugins { kotlin { explicitApi = null + jvmToolchain { + (this as JavaToolchainSpec).languageVersion.set(JavaLanguageVersion.of(11)) + } + sourceSets { commonMain { dependencies { diff --git a/build.gradle.kts b/build.gradle.kts index 2bba330a..d43eee8b 100644 --- a/build.gradle.kts +++ b/build.gradle.kts @@ -1,6 +1,3 @@ -import org.jetbrains.kotlin.gradle.dsl.JvmTarget -import org.jetbrains.kotlin.gradle.tasks.KotlinCompile - @Suppress("DSL_SCOPE_VIOLATION") plugins { @@ -52,6 +49,7 @@ allprojects { ) systemProperty("CURRENT_VERSION", "$version") systemProperty("arrowVersion", libs.versions.arrow.get()) + systemProperty("jvmTargetVersion", "11") jvmArgs = listOf( """-Dkotlin.compiler.execution.strategy="in-process"""", "--add-opens=jdk.compiler/com.sun.tools.javac.api=ALL-UNNAMED", @@ -64,17 +62,3 @@ allprojects { ) } } - -val toolchain = project.extensions.getByType() -allprojects { - tasks.withType().configureEach { - javaCompiler.set( - toolchain.compilerFor { - languageVersion.set(JavaLanguageVersion.of(8)) - } - ) - } - tasks.withType().configureEach { - compilerOptions.jvmTarget.set(JvmTarget.JVM_1_8) - } -} diff --git a/gradle/projects.libs.versions.toml b/gradle/projects.libs.versions.toml index d525bb8e..af18a90d 100644 --- a/gradle/projects.libs.versions.toml +++ b/gradle/projects.libs.versions.toml @@ -1,21 +1,21 @@ [versions] -arrow = "1.1.5" -arrowMeta = "1.6.2-alpha.5" -arrowGradleConfig = "0.11.0" +arrow = "1.2.0-RC" +arrowMeta = "1.6.2" +arrowGradleConfig = "0.12.0-rc.3" classgraph = "4.8.157" dokka = "1.8.10" junit = "5.9.2" junitLauncher = "1.9.2" -kotlin = "1.8.10" -kotest = "5.5.5" +kotlin = "1.8.21" +kotest = "5.6.1" javaSmt = "3.14.3" javaCompileTesting = "0.21.0" -apacheCommonsText = "1.9" +apacheCommonsText = "1.10.0" sarif4k = "0.3.0" kotlinBinaryCompatibilityValidator = "0.13.0" detekt = "1.22.0" -kotlinxSerialization = "1.5.0-RC" -ksp = "1.8.10-1.0.9" +kotlinxSerialization = "1.5.0" +ksp = "1.8.21-1.0.11" [libraries] arrowAnnotations = { module = "io.arrow-kt:arrow-annotations", version.ref = "arrow" } diff --git a/gradle/wrapper/gradle-wrapper.properties b/gradle/wrapper/gradle-wrapper.properties index e1bef7e8..fae08049 100644 --- a/gradle/wrapper/gradle-wrapper.properties +++ b/gradle/wrapper/gradle-wrapper.properties @@ -1,5 +1,5 @@ distributionBase=GRADLE_USER_HOME distributionPath=wrapper/dists -distributionUrl=https\://services.gradle.org/distributions/gradle-8.0.2-bin.zip +distributionUrl=https\://services.gradle.org/distributions/gradle-8.1.1-bin.zip zipStoreBase=GRADLE_USER_HOME zipStorePath=wrapper/dists