Merge branch 'main' into update/zio-2.1.13

.github/workflows/container.yml

@@ -29,6 +29,15 @@ jobs:
       - name: Checkout repository
         uses: actions/checkout@v4
 
+      - name: Set up JDK 17
+        uses: actions/setup-java@v3
+        with:
+          distribution: temurin
+          java-version: 17
+          cache: sbt
+      # see: https://github.com/actions/runner-images/issues/10788
+      - uses: sbt/setup-sbt@v1
+
       - name: Log in to the Container registry
         uses: docker/login-action@f054a8b539a109f9f41c372932f1ae047eff08c9
         with:

.github/workflows/main.yml

@@ -36,6 +36,9 @@ jobs:
         with:
           distribution: temurin
           java-version: 17
+          cache: sbt
+      # see: https://github.com/actions/runner-images/issues/10788
+      - uses: sbt/setup-sbt@v1
       - name: Check formatting
         run: make fmt-check
 
@@ -50,6 +53,8 @@ jobs:
         with:
           distribution: temurin
           java-version: 17
+      # see: https://github.com/actions/runner-images/issues/10788
+      - uses: sbt/setup-sbt@v1
       - name: Check scaladoc
         run: sbt unidoc
 
@@ -64,6 +69,8 @@ jobs:
         with:
           distribution: temurin
           java-version: 17
+      # see: https://github.com/actions/runner-images/issues/10788
+      - uses: sbt/setup-sbt@v1
       - name: Coursier cache
         uses: coursier/cache-action@v6
       - name: Set APALACHE_HOME env
@@ -97,6 +104,8 @@ jobs:
         with:
           jvm: temurin:1.17
           apps: sbt
+      # see: https://github.com/actions/runner-images/issues/10788
+      - uses: sbt/setup-sbt@v1
       - name: Set APALACHE_HOME env
         # See https://docs.github.com/en/actions/using-workflows/workflow-commands-for-github-actions#setting-an-environment-variable
         run: echo "APALACHE_HOME=$GITHUB_WORKSPACE" >> $GITHUB_ENV
@@ -164,6 +173,8 @@ jobs:
     runs-on: ubuntu-latest
     steps:
       - uses: actions/checkout@v4
+      # see: https://github.com/actions/runner-images/issues/10788
+      - uses: sbt/setup-sbt@v1
       - name: Cache nix store
         # Workaround for cache action not playing well with permissions
         # See https://github.com/actions/cache/issues/324

.github/workflows/prepare-release.yml

@@ -26,6 +26,8 @@ jobs:
         with:
           distribution: temurin
           java-version: 17
+      # see: https://github.com/actions/runner-images/issues/10788
+      - uses: sbt/setup-sbt@v1
       - name: Configure Git
         run: |
           git config --global user.name "$GITHUB_ACTOR"

.github/workflows/release.yml

@@ -21,6 +21,8 @@ jobs:
         with:
           distribution: temurin
           java-version: 17
+      # see: https://github.com/actions/runner-images/issues/10788
+      - uses: sbt/setup-sbt@v1
       - name: Cut Release
         env:
           # NOTE: We must not use the default GITHUB_TOKEN for auth here,

CHANGES.md

@@ -1,6 +1,17 @@
 <!-- NOTE: This file is generated. Do not write release notes here.
  Notes for unreleased changes go in the .unreleased/ directory. -->
 
+## 0.47.2 - 2024-12-16
+
+## 0.47.1 - 2024-12-16
+
+### Bug fixes
+
+- Fixed a few problems on parsing Quint and pretty printing TLA, see #3041
+- Add extra protection against the SANY race conditions on the filesystem, see #3046
+- Fix source tracking in `VCGenerator` to avoid spurious diagnostic messages, see #3010
+- Fix a problem when translating Quint nullary operators used polymorphically, see #3044
+
 ## 0.47.0 - 2024-10-02
 
 ### Breaking changes

VERSION

@@ -1 +1 @@
-0.47.1-SNAPSHOT
+0.47.3-SNAPSHOT

project/Dependencies.scala

@@ -21,7 +21,7 @@ object Dependencies {
     val commonsBeanutils =
       "commons-beanutils" % "commons-beanutils" % "1.9.4" // Apparently an untracked dependency of commonsConfiguration2
     val commonsConfiguration2 = "org.apache.commons" % "commons-configuration2" % "2.11.0"
-    val commonsIo = "commons-io" % "commons-io" % "2.17.0"
+    val commonsIo = "commons-io" % "commons-io" % "2.18.0"
     val guice = "com.google.inject" % "guice" % "7.0.0"
     val kiama = "org.bitbucket.inkytonik.kiama" %% "kiama" % "2.5.1"
     val logbackClassic = "ch.qos.logback" % "logback-classic" % logbackVersion
@@ -40,7 +40,7 @@ object Dependencies {
     val zio = "dev.zio" %% "zio" % zioVersion
     // Keep up to sync with version in plugins.sbt
     val zioGrpcCodgen = "com.thesamet.scalapb.zio-grpc" %% "zio-grpc-codegen" % "0.6.0-test3" % "provided"
-    val grpcNetty = "io.grpc" % "grpc-netty" % "1.68.1"
+    val grpcNetty = "io.grpc" % "grpc-netty" % "1.68.2"
     val scalapbRuntimGrpc =
       "com.thesamet.scalapb" %% "scalapb-runtime-grpc" % scalapb.compiler.Version.scalapbVersion
     // Ensures we have access to commonly used protocol buffers (e.g., google.protobuf.Struct)
@@ -54,7 +54,7 @@ object Dependencies {
     // Libraries
     val junit = "junit" % "junit" % "4.13.2" % Test
     val scalacheck = "org.scalacheck" %% "scalacheck" % "1.18.1" % Test
-    val easymock = "org.easymock" % "easymock" % "5.4.0" % Test
+    val easymock = "org.easymock" % "easymock" % "5.5.0" % Test
 
     val scalaTestVersion = "3.2.15"
     val scalatest = "org.scalatest" %% "scalatest" % scalaTestVersion % Test

project/build.properties

@@ -1 +1 @@
-sbt.version=1.10.5
+sbt.version=1.10.6

project/plugins.sbt

@@ -5,9 +5,9 @@ addSbtPlugin("com.eed3si9n" % "sbt-assembly" % "1.2.0")
 // https://github.com/marcuslonnberg/sbt-docker
 addSbtPlugin("se.marcuslonnberg" % "sbt-docker" % "1.11.0")
 // https://github.com/scoverage/sbt-scoverage
-addSbtPlugin("org.scoverage" % "sbt-scoverage" % "2.2.1")
+addSbtPlugin("org.scoverage" % "sbt-scoverage" % "2.2.2")
 // https://github.com/sbt/sbt-buildinfo
-addSbtPlugin("com.eed3si9n" % "sbt-buildinfo" % "0.13.0")
+addSbtPlugin("com.eed3si9n" % "sbt-buildinfo" % "0.13.1")
 // https://github.com/sbt/sbt-native-packager
 addSbtPlugin("com.github.sbt" % "sbt-native-packager" % "1.10.4")
 // https://scalacenter.github.io/scalafix/docs/users/installation.html

project/sbt-changeling/build.sbt

@@ -2,7 +2,7 @@ ThisBuild / version := "0.1.0-SNAPSHOT"
 ThisBuild / organization := "systems.informal"
 
 libraryDependencies ++= Seq(
-    "org.scala-sbt" % "sbt" % "1.10.5"
+    "org.scala-sbt" % "sbt" % "1.10.6"
 )
 
 lazy val sbt_changeling = (project in file("."))

project/sbt-changeling/project/build.properties

@@ -1 +1 @@
-sbt.version=1.10.5
+sbt.version=1.10.6

src/universal/bin/apalache-mc

@@ -38,16 +38,24 @@ then
     JVM_ARGS="${JVM_ARGS} -Xmx4096m"
 fi
 
+# Avoid SANY concurrency issues: https://github.com/tlaplus/tlaplus/issues/688
+if [ -z "${TMPDIR:-}" ]; then
+    TMPDIR="$(pwd)/tmp"
+    mkdir -p "$TMPDIR"
+fi
+JAVA_IO_TMPDIR=`mktemp -d -t SANYXXXXXXXXXX`
+
 # Check whether the CLI args contains the debug flag
 if [[ "$*" =~ '--debug' ]]
 then
     echo "# Tool home: $DIR"
     echo "# Package:   $APALACHE_JAR"
     echo "# JVM args: $JVM_ARGS"
+    echo "# -Djava.io.tmpdir: $JAVA_IO_TMPDIR"
     echo "#"
 fi
 
 # Run with `exec` to replace the PID, rather than running in a subshell.
 # This saves one process, and ensures signals are sent to the replacement process
 # C.f. https://github.com/sbt/sbt-native-packager/blob/e72f2f45b8cab5881add1cd62743bfc69c2b9b4d/src/main/resources/com/typesafe/sbt/packager/archetypes/scripts/bash-template#L141-L142
-exec java $JVM_ARGS -jar "$APALACHE_JAR" "$@"
+exec java $JVM_ARGS -Djava.io.tmpdir=$JAVA_IO_TMPDIR -jar "$APALACHE_JAR" "$@"

tla-io/src/main/scala/at/forsyte/apalache/io/lir/PrettyWriter.scala

@@ -297,14 +297,6 @@ class PrettyWriter(
             text("{") <> nest(line <> binding <> ":" <> nest(line <> filter)) <> line <> text("}")
         ) ///
 
-      // a function of multiple arguments that are packed into a tuple: don't print the angular brackets <<...>>
-      case OperEx(op @ TlaFunOper.app, funEx, OperEx(TlaFunOper.tuple, args @ _*)) =>
-        val argDocs = args.map(exToDoc(op.precedence, _, nameResolver))
-        val commaSeparatedArgs = folddoc(argDocs.toList, _ <> text(",") <@> _)
-        group(
-            exToDoc(TlaFunOper.app.precedence, funEx, nameResolver) <> brackets(commaSeparatedArgs)
-        ) ///
-
       // a function of a single argument
       case OperEx(TlaFunOper.app, funEx, argEx) =>
         group(
@@ -473,14 +465,19 @@ class PrettyWriter(
         wrapWithParen(parentPrecedence, op.precedence, group(doc))
 
       case OperEx(op @ TlaOper.apply, NameEx(name), args @ _*) =>
+        val (decls, newArgs) = extractDecls(args)
+
         // apply an operator by its name, e.g., F(x)
-        val argDocs = args.map(exToDoc(op.precedence, _, nameResolver)).toList
+        val argDocs = newArgs.map(exToDoc(op.precedence, _, nameResolver)).toList
         val commaSeparated = ssep(argDocs, "," <> softline)
+
         val doc =
           if (args.isEmpty) {
             text(parseableName(name))
-          } else {
+          } else if (decls.isEmpty) {
             group(parseableName(name) <> parens(commaSeparated))
+          } else {
+            group(ssep(decls, line) <> line <> parseableName(name) <> parens(commaSeparated))
           }
 
         wrapWithParen(parentPrecedence, op.precedence, doc)
@@ -494,16 +491,20 @@ class PrettyWriter(
         wrapWithParen(parentPrecedence, op.precedence, doc)
 
       case OperEx(op, args @ _*) =>
-        val argDocs = args.map(exToDoc(op.precedence, _, nameResolver)).toList
+        val (decls, newArgs) = extractDecls(args)
+        val argDocs = newArgs.map(exToDoc(op.precedence, _, nameResolver)).toList
         val commaSeparated = ssep(argDocs, "," <> softline)
         // The standard operators may contain a '!' that refers to the standard module. Remove it.
         val lastIndexOfBang = op.name.lastIndexOf("!")
         val unqualifiedName = if (lastIndexOfBang < 0) op.name else (op.name.substring(lastIndexOfBang + 1))
+
         val doc =
           if (args.isEmpty) {
             text(unqualifiedName)
-          } else {
+          } else if (decls.isEmpty) {
             group(unqualifiedName <> parens(commaSeparated))
+          } else {
+            group(ssep(decls, line) <> line <> unqualifiedName <> parens(commaSeparated))
           }
 
         wrapWithParen(parentPrecedence, op.precedence, doc)
@@ -527,6 +528,25 @@ class PrettyWriter(
     }
   }
 
+  /**
+   * On TLA+ files, we can't have LET..IN expressions as arguments. This is a helper function to extract the
+   * declarations so they can be printed before the operator application that would use them as arguments.
+   */
+  def extractDecls(exprs: Seq[TlaEx]): (List[Doc], Seq[TlaEx]) = {
+    val decls = exprs.collect {
+      case LetInEx(_, TlaOperDecl("LAMBDA", _, _)) => Nil
+      case LetInEx(_, decls @ _*)                  => decls
+      case _                                       => Nil
+    }
+    val newArgs = exprs.collect {
+      case expr @ LetInEx(_, TlaOperDecl("LAMBDA", _, _)) => expr
+      case LetInEx(body, _)                               => body
+      case expr                                           => expr
+    }
+
+    (decls.flatten.map(d => group("LET" <> space <> declToDoc(d) <> line <> "IN")).toList, newArgs)
+  }
+
   /**
    * Pretty-writes the given decl, while replacing names with the values in the NameReplacementMap. Then, wrap the
    * result as a comment, since the substituted names might not be valid TLA.

tla-io/src/main/scala/at/forsyte/apalache/io/quint/Quint.scala

@@ -4,16 +4,14 @@ import at.forsyte.apalache.io.quint.QuintEx._
 import at.forsyte.apalache.io.quint.QuintType._
 import at.forsyte.apalache.tla.lir._
 import at.forsyte.apalache.tla.typecomp._
+import at.forsyte.apalache.tla.typecomp.unsafe.UnsafeLiteralAndNameBuilder
 import at.forsyte.apalache.tla.types.tla
 
 // scalaz is brought in For the Reader monad, which we use for
 // append-only, context local state for tracking reference to nullary TLA
 // operators
 import scalaz._
-// list and traverse give us monadic mapping over lists
-// see https://github.com/scalaz/scalaz/blob/88fc7de1c439d152d40fce6b20d90aea33cbb91b/example/src/main/scala-2/scalaz/example/TraverseUsage.scala
-import scalaz.std.list._
-import scalaz.syntax.traverse._
+import Scalaz._
 
 import scala.util.{Failure, Success, Try}
 import at.forsyte.apalache.tla.lir.values.TlaStr
@@ -31,6 +29,8 @@ import at.forsyte.apalache.tla.lir.values.TlaStr
 class Quint(quintOutput: QuintOutput) {
   private val nameGen = new QuintNameGen // name generator, reused across the entire spec
   private val typeConv = new QuintTypeConverter
+  private val unsafeBuilder = new UnsafeLiteralAndNameBuilder {}
+
   private val table = quintOutput.table
   private val types = quintOutput.types
 
@@ -446,7 +446,7 @@ class Quint(quintOutput: QuintOutput) {
             case ValEx(TlaStr("_")) =>
               // We have a default case, which is always paired with an eliminator that
               // can be applied to the unit value (an empty record).
-              (cs, Some(tla.appOp(defaultElim, tla.rowRec(None))))
+              (cs, Some(tla.appOp(defaultElim, tla.emptySet(IntT1))))
             case _ =>
               // All cases have match expressions
               (allCases, None)
@@ -573,7 +573,7 @@ class Quint(quintOutput: QuintOutput) {
         case "Tup" =>
           if (quintArgs.isEmpty) {
             // Translate empty tuples to values of type UNIT
-            (_) => Reader((_) => tla.const("U", ConstT1(("UNIT"))))
+            (_) => Reader((_) => tla.rowRec(None, "tag" -> tla.str("UNIT")))
           } else {
             variadicApp(args => tla.tuple(args: _*))
           }
@@ -727,7 +727,12 @@ class Quint(quintOutput: QuintOutput) {
             val t = typeConv.convert(types(id).typ)
             Reader { nullaryOpNames =>
               if (nullaryOpNames.contains(name)) {
-                tla.appOp(tla.name(name, OperT1(Seq(), t)))
+                // Name can be a polymorphic operator, but we need to give it the
+                // specialized type inferred by Quint to avoid type errors in
+                // Apalache. So we use the unsafe builder instead, as the safe
+                // builder enforces that same names have the same types under
+                // the scope.
+                tla.appOp(unsafeBuilder.name(name, OperT1(Seq(), t)).point[TBuilderInternalState])
               } else {
                 tla.name(name, t)
               }

tla-io/src/main/scala/at/forsyte/apalache/io/quint/QuintTypeConverter.scala

@@ -96,8 +96,11 @@ private class QuintTypeConverter extends LazyLogging {
     case QuintSeqT(elem)       => SeqT1(convert(elem))
     case QuintFunT(arg, res)   => FunT1(convert(arg), convert(res))
     case QuintOperT(args, res) => OperT1(args.map(convert), convert(res))
+    // Use the Unit type for empty tuples, since they are the unit type in Quint
+    // The unit type is a record like [ "tag" |-> "UNIT" ] so it can be compared to other constructed types.
+    // This is relevant when we produce a TLA+ file to be used with TLC.
     case QuintTupleT(Row.Nil() | Row.Cell(Seq(), _)) =>
-      ConstT1("UNIT") // Use the Unit type for empty tuples, since they are the unit type in Quint
+      RecRowT1(RowT1("tag" -> StrT1))
     case QuintTupleT(row)  => rowToTupleT1(row)
     case QuintRecordT(row) => RecRowT1(rowToRowT1(row))
     case QuintSumT(row)    => VariantT1(rowToRowT1(row))

tla-io/src/test/scala/at/forsyte/apalache/io/lir/TestPrettyWriter.scala

@@ -844,6 +844,24 @@ class TestPrettyWriter extends AnyFunSuite with BeforeAndAfterEach {
     assert(expected == stringWriter.toString)
   }
 
+  test("operator application with LET-IN as argument") {
+    val writer = new PrettyWriter(printWriter, layout40)
+    val decl1 =
+      TlaOperDecl("A", List(OperParam("param1"), OperParam("param2")), plus(name("param1"), name("param2")))
+    val letInEx = letIn(appDecl(decl1, int(1), int(2)), decl1)
+    // Foo(LET A(param1, param2) == param1 + param2 IN A(1, 2))
+    val expr = OperEx(TlaOper.apply, NameEx("Foo"), letInEx)
+
+    writer.write(expr)
+    printWriter.flush()
+    // LET declaration needs to be printed before the application
+    val expected =
+      """LET A(param1, param2) == param1 + param2
+        |IN
+        |Foo((A(1, 2)))""".stripMargin
+    assert(expected == stringWriter.toString)
+  }
+
   test("a LAMBDA as LET-IN") {
     val writer = new PrettyWriter(printWriter, layout40)
     val aDecl = TlaOperDecl("LAMBDA", List(OperParam("x")), NameEx("x"))
@@ -989,7 +1007,7 @@ class TestPrettyWriter extends AnyFunSuite with BeforeAndAfterEach {
     writer.write(fDecl)
     printWriter.flush()
     val expected =
-      """f[x \in S, y \in S] == f[y, x]
+      """f[x \in S, y \in S] == f[<<y, x>>]
         |
         |""".stripMargin
     assert(expected == stringWriter.toString)