Update Kotlin and Arrow versions (#60)

Co-authored-by: Simon Vergauwen <[email protected]>
arrow-kt · Apr 30, 2023 · b92708b · b92708b
1 parent edd4ca7
commit b92708b
Show file tree

Hide file tree

Showing 16 changed files with 95 additions and 83 deletions.
diff --git 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/...on/src/main/kotlin/arrow/meta/plugins/analysis/phases/analysis/solver/check/EntryPoint.kt b/...on/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/...main/kotlin/arrow/meta/plugins/analysis/phases/analysis/solver/collect/FromAnnotations.kt b/...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/...mon/src/main/kotlin/arrow/meta/plugins/analysis/phases/analysis/solver/errors/ErrorIds.kt b/...mon/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/...rc/main/kotlin/arrow/meta/plugins/analysis/phases/analysis/solver/errors/ErrorMessages.kt b/...rc/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,16 +124,15 @@ object ErrorMessages {
          |  -> unsatisfiable constraint: `${callPreCondition.formula.dumpKotlinLike()}`
          |  -> ${template(callPreCondition, this)}
          |  -> ${branch(branch)}
-      """.trimMargin(
-      )
+      """
+        .trimMargin()
 
     /**
      * (attached to the return value)
      *
      * 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
@@ -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
@@ -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
@@ -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
@@ -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
@@ -10,6 +10,9 @@ plugins {
 
 kotlin {
   explicitApi = null
+  jvmToolchain {
+    (this as JavaToolchainSpec).languageVersion.set(JavaLanguageVersion.of(11))
+  }
 }
 
 dependencies {