Merge branch 'main' into update/grpc-netty-1.69.0

.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

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/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
 
@@ -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/test/scala/at/forsyte/apalache/io/quint/TestQuintEx.scala

@@ -205,7 +205,7 @@ class TestQuintEx extends AnyFunSuite {
 
   def translate(qex: QuintEx): TlaEx = {
     val translator = new Quint(Q.quintOutput)
-    val nullaryOps = Set[String]()
+    val nullaryOps = Set[String]("None")
     val tlaEx = build(translator.tlaExpression(qex).run(nullaryOps))
     tlaEx
   }
@@ -793,13 +793,13 @@ class TestQuintEx extends AnyFunSuite {
     val polyConst1 = "polyConst1"
 
     // We want to test that we can use this polymorphic operator by applying it to two
-    // different values of the same type.
+    // different values of different types.
     val appliedToStr = Q.app(polyConst1, Q.s)(QuintIntT(), oper.id)
     val appliedToBool = Q.app(polyConst1, Q.tt)(QuintIntT(), oper.id)
     // We'll combine these two applications using addition, just to form a compound expression that includes both
     val body = Q.app("iadd", appliedToStr, appliedToBool)(QuintIntT())
 
-    // Putting it all to gether, we have the let expression
+    // Putting it all together, we have the let expression
     //
     // ```
     // def polyConst1(x): a => int = 1;
@@ -811,6 +811,18 @@ class TestQuintEx extends AnyFunSuite {
     assert(convert(expr) == """LET polyConst1(x) ≜ 1 IN (polyConst1("s")) + (polyConst1(TRUE))""")
   }
 
+  test("can convert nullary polymorphic operator used polymorphically") {
+    val optionInt = QuintSumT.ofVariantTypes("Some" -> QuintIntT(), "None" -> QuintRecordT.ofFieldTypes())
+    val noneInt = Q.nam("None", optionInt)
+
+    val optionBool = QuintSumT.ofVariantTypes("Some" -> QuintBoolT(), "None" -> QuintRecordT.ofFieldTypes())
+    val noneBool = Q.nam("None", optionBool)
+
+    val expr = Q.app("Tup", noneInt, noneBool)(QuintTupleT.ofTypes(optionInt, optionBool))
+
+    assert(convert(expr) == """<<None(), None()>>""")
+  }
+
   test("oneOf operator occuring outside of a nondet binding is an error") {
     // See https://github.com/informalsystems/apalache/issues/2774
     val err = intercept[QuintIRParseError](convert(Q.oneOfSet))