From b0a2559091103bed4b4ed3c5e605f0ce897f68bd Mon Sep 17 00:00:00 2001 From: bugarela Date: Tue, 10 Dec 2024 09:42:56 -0300 Subject: [PATCH 01/26] Fix conversion of Quint nullary polymorphic operators --- .../at/forsyte/apalache/io/quint/Quint.scala | 2 +- .../apalache/io/quint/TestQuintEx.scala | 18 +++++++++++++++--- .../subbuilder/LiteralAndNameBuilder.scala | 8 ++++++++ .../typecomp/TestLiteralAndNameBuilder.scala | 8 ++++++++ 4 files changed, 32 insertions(+), 4 deletions(-) diff --git a/tla-io/src/main/scala/at/forsyte/apalache/io/quint/Quint.scala b/tla-io/src/main/scala/at/forsyte/apalache/io/quint/Quint.scala index 91ef87fbea..2fb7dbb19b 100644 --- a/tla-io/src/main/scala/at/forsyte/apalache/io/quint/Quint.scala +++ b/tla-io/src/main/scala/at/forsyte/apalache/io/quint/Quint.scala @@ -727,7 +727,7 @@ 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))) + tla.appOp(tla.polymorphicName(name, OperT1(Seq(), t))) } else { tla.name(name, t) } diff --git a/tla-io/src/test/scala/at/forsyte/apalache/io/quint/TestQuintEx.scala b/tla-io/src/test/scala/at/forsyte/apalache/io/quint/TestQuintEx.scala index 9245bca5e1..a1b880f9dc 100644 --- a/tla-io/src/test/scala/at/forsyte/apalache/io/quint/TestQuintEx.scala +++ b/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) == """<>""") + } + 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)) diff --git a/tlair/src/main/scala/at/forsyte/apalache/tla/typecomp/subbuilder/LiteralAndNameBuilder.scala b/tlair/src/main/scala/at/forsyte/apalache/tla/typecomp/subbuilder/LiteralAndNameBuilder.scala index 5fd4178efe..ca3123d7dd 100644 --- a/tlair/src/main/scala/at/forsyte/apalache/tla/typecomp/subbuilder/LiteralAndNameBuilder.scala +++ b/tlair/src/main/scala/at/forsyte/apalache/tla/typecomp/subbuilder/LiteralAndNameBuilder.scala @@ -77,6 +77,14 @@ trait LiteralAndNameBuilder { (mi.copy(freeNameScope = scope + (exprName -> finalT), usedNames = mi.usedNames + exprName), ret) } + /** + * {{{exprName: t}}} + * @param exprName + * can take different types under the same scope (polymorphic operator). + */ + def polymorphicName(exprName: String, t: TlaType1): TBuilderInstruction = + unsafeBuilder.name(exprName, t).point[TBuilderInternalState] + /** Attempt to infer the type from the scope. Fails if exprName is not in scope. */ def nameWithInferredType(exprName: String): TBuilderInstruction = get[TBuilderContext].map { mi: TBuilderContext => val scope = mi.freeNameScope diff --git a/tlair/src/test/scala/at/forsyte/apalache/tla/typecomp/TestLiteralAndNameBuilder.scala b/tlair/src/test/scala/at/forsyte/apalache/tla/typecomp/TestLiteralAndNameBuilder.scala index 70c2d6c303..63fc3252cd 100644 --- a/tlair/src/test/scala/at/forsyte/apalache/tla/typecomp/TestLiteralAndNameBuilder.scala +++ b/tlair/src/test/scala/at/forsyte/apalache/tla/typecomp/TestLiteralAndNameBuilder.scala @@ -152,5 +152,13 @@ class TestLiteralAndNameBuilder extends BuilderTest { } yield () ) } + + // Should not throw with polymorphic names + build( + for { + _ <- builder.polymorphicName("x", IntT1) + _ <- builder.polymorphicName("x", BoolT1) + } yield () + ) } } From afff4366a03ab6fc3b10f1ef5b9b529de0e9d6e1 Mon Sep 17 00:00:00 2001 From: bugarela Date: Tue, 10 Dec 2024 09:51:11 -0300 Subject: [PATCH 02/26] Add CHANGELOG entry --- .unreleased/bug-fixes/quint-nullary-operators.md | 1 + 1 file changed, 1 insertion(+) create mode 100644 .unreleased/bug-fixes/quint-nullary-operators.md diff --git a/.unreleased/bug-fixes/quint-nullary-operators.md b/.unreleased/bug-fixes/quint-nullary-operators.md new file mode 100644 index 0000000000..046a7265a9 --- /dev/null +++ b/.unreleased/bug-fixes/quint-nullary-operators.md @@ -0,0 +1 @@ +Fix a problem when translating Quint nullary operators used polymorphically, see #3044 From e1c2d85343a16e4e74c78ef69e6196747e5b518e Mon Sep 17 00:00:00 2001 From: bugarela Date: Fri, 13 Dec 2024 10:07:31 -0300 Subject: [PATCH 03/26] Use unsafe builder --- .../at/forsyte/apalache/io/quint/Quint.scala | 15 ++++++++++----- .../subbuilder/LiteralAndNameBuilder.scala | 8 -------- .../tla/typecomp/TestLiteralAndNameBuilder.scala | 8 -------- 3 files changed, 10 insertions(+), 21 deletions(-) diff --git a/tla-io/src/main/scala/at/forsyte/apalache/io/quint/Quint.scala b/tla-io/src/main/scala/at/forsyte/apalache/io/quint/Quint.scala index 2fb7dbb19b..a9b42ff71e 100644 --- a/tla-io/src/main/scala/at/forsyte/apalache/io/quint/Quint.scala +++ b/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.polymorphicName(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) } diff --git a/tlair/src/main/scala/at/forsyte/apalache/tla/typecomp/subbuilder/LiteralAndNameBuilder.scala b/tlair/src/main/scala/at/forsyte/apalache/tla/typecomp/subbuilder/LiteralAndNameBuilder.scala index ca3123d7dd..5fd4178efe 100644 --- a/tlair/src/main/scala/at/forsyte/apalache/tla/typecomp/subbuilder/LiteralAndNameBuilder.scala +++ b/tlair/src/main/scala/at/forsyte/apalache/tla/typecomp/subbuilder/LiteralAndNameBuilder.scala @@ -77,14 +77,6 @@ trait LiteralAndNameBuilder { (mi.copy(freeNameScope = scope + (exprName -> finalT), usedNames = mi.usedNames + exprName), ret) } - /** - * {{{exprName: t}}} - * @param exprName - * can take different types under the same scope (polymorphic operator). - */ - def polymorphicName(exprName: String, t: TlaType1): TBuilderInstruction = - unsafeBuilder.name(exprName, t).point[TBuilderInternalState] - /** Attempt to infer the type from the scope. Fails if exprName is not in scope. */ def nameWithInferredType(exprName: String): TBuilderInstruction = get[TBuilderContext].map { mi: TBuilderContext => val scope = mi.freeNameScope diff --git a/tlair/src/test/scala/at/forsyte/apalache/tla/typecomp/TestLiteralAndNameBuilder.scala b/tlair/src/test/scala/at/forsyte/apalache/tla/typecomp/TestLiteralAndNameBuilder.scala index 63fc3252cd..70c2d6c303 100644 --- a/tlair/src/test/scala/at/forsyte/apalache/tla/typecomp/TestLiteralAndNameBuilder.scala +++ b/tlair/src/test/scala/at/forsyte/apalache/tla/typecomp/TestLiteralAndNameBuilder.scala @@ -152,13 +152,5 @@ class TestLiteralAndNameBuilder extends BuilderTest { } yield () ) } - - // Should not throw with polymorphic names - build( - for { - _ <- builder.polymorphicName("x", IntT1) - _ <- builder.polymorphicName("x", BoolT1) - } yield () - ) } } From 1c67973b19bfc0a1368756fbb2ad5443a2c47a38 Mon Sep 17 00:00:00 2001 From: Igor Konnov Date: Fri, 13 Dec 2024 17:16:23 +0100 Subject: [PATCH 04/26] protect against SANY race conditions on the filesystem --- src/universal/bin/apalache-mc | 4 ++++ 1 file changed, 4 insertions(+) diff --git a/src/universal/bin/apalache-mc b/src/universal/bin/apalache-mc index 45b2f28f73..5689e8028f 100755 --- a/src/universal/bin/apalache-mc +++ b/src/universal/bin/apalache-mc @@ -38,6 +38,10 @@ then JVM_ARGS="${JVM_ARGS} -Xmx4096m" fi +# Avoid SANY concurrency issues: https://github.com/tlaplus/tlaplus/issues/688 +TD=`mktemp -d "$TMPDIR"/SANYXXXXXXXXXX` +JVM_ARGS="${JVM_ARGS} -Djava.io.tmpdir=$TD" + # Check whether the CLI args contains the debug flag if [[ "$*" =~ '--debug' ]] then From d4cd6e147865cc1ed881e48374ff1e8b2e2449cc Mon Sep 17 00:00:00 2001 From: Igor Konnov Date: Fri, 13 Dec 2024 17:30:18 +0100 Subject: [PATCH 05/26] add release notes --- .unreleased/bug-fixes/sany-tmpdir.md | 1 + 1 file changed, 1 insertion(+) create mode 100644 .unreleased/bug-fixes/sany-tmpdir.md diff --git a/.unreleased/bug-fixes/sany-tmpdir.md b/.unreleased/bug-fixes/sany-tmpdir.md new file mode 100644 index 0000000000..8cce6d77c8 --- /dev/null +++ b/.unreleased/bug-fixes/sany-tmpdir.md @@ -0,0 +1 @@ +Add extra protection against the SANY race conditions on the filesystem, see #3046 From ce176b022a83df5e20c86d435adf98559de84ee2 Mon Sep 17 00:00:00 2001 From: Igor Konnov Date: Fri, 13 Dec 2024 17:48:58 +0100 Subject: [PATCH 06/26] handle TMPDIR for docker --- src/universal/bin/apalache-mc | 6 +++++- 1 file changed, 5 insertions(+), 1 deletion(-) diff --git a/src/universal/bin/apalache-mc b/src/universal/bin/apalache-mc index 5689e8028f..d75083b0cf 100755 --- a/src/universal/bin/apalache-mc +++ b/src/universal/bin/apalache-mc @@ -39,7 +39,11 @@ then fi # Avoid SANY concurrency issues: https://github.com/tlaplus/tlaplus/issues/688 -TD=`mktemp -d "$TMPDIR"/SANYXXXXXXXXXX` +if [ -z "$TMPDIR" ]; then + TMPDIR="$(pwd)/tmp" + mkdir -p "$TMPDIR" +fi +TD=`mktemp -d -p $TMPDIR -t SANYXXXXXXXXXX` JVM_ARGS="${JVM_ARGS} -Djava.io.tmpdir=$TD" # Check whether the CLI args contains the debug flag From c30a20df18dffde6411e70e85aa4ff6b14a4fb4a Mon Sep 17 00:00:00 2001 From: Igor Konnov Date: Fri, 13 Dec 2024 17:55:16 +0100 Subject: [PATCH 07/26] refactor a bit to avoid fuzzy output in the integration tests --- src/universal/bin/apalache-mc | 6 +++--- 1 file changed, 3 insertions(+), 3 deletions(-) diff --git a/src/universal/bin/apalache-mc b/src/universal/bin/apalache-mc index d75083b0cf..0bf1985b99 100755 --- a/src/universal/bin/apalache-mc +++ b/src/universal/bin/apalache-mc @@ -43,8 +43,7 @@ if [ -z "$TMPDIR" ]; then TMPDIR="$(pwd)/tmp" mkdir -p "$TMPDIR" fi -TD=`mktemp -d -p $TMPDIR -t SANYXXXXXXXXXX` -JVM_ARGS="${JVM_ARGS} -Djava.io.tmpdir=$TD" +JAVA_IO_TMPDIR=`mktemp -d -p $TMPDIR -t SANYXXXXXXXXXX` # Check whether the CLI args contains the debug flag if [[ "$*" =~ '--debug' ]] @@ -52,10 +51,11 @@ 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" "$@" From f73b53136a81420ef4de1cac0c462017c9f9759c Mon Sep 17 00:00:00 2001 From: Igor Konnov Date: Fri, 13 Dec 2024 18:35:31 +0100 Subject: [PATCH 08/26] fix an error on empty TMPDIR --- src/universal/bin/apalache-mc | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/universal/bin/apalache-mc b/src/universal/bin/apalache-mc index 0bf1985b99..e530d42661 100755 --- a/src/universal/bin/apalache-mc +++ b/src/universal/bin/apalache-mc @@ -39,7 +39,7 @@ then fi # Avoid SANY concurrency issues: https://github.com/tlaplus/tlaplus/issues/688 -if [ -z "$TMPDIR" ]; then +if [ -z "${TMPDIR:-}" ]; then TMPDIR="$(pwd)/tmp" mkdir -p "$TMPDIR" fi From 4e6279d749abbd5a47f99b8488f1abe5c5a92197 Mon Sep 17 00:00:00 2001 From: Igor Konnov Date: Fri, 13 Dec 2024 18:58:36 +0100 Subject: [PATCH 09/26] try it without -p --- src/universal/bin/apalache-mc | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/universal/bin/apalache-mc b/src/universal/bin/apalache-mc index e530d42661..e9e5dfc32f 100755 --- a/src/universal/bin/apalache-mc +++ b/src/universal/bin/apalache-mc @@ -43,7 +43,7 @@ if [ -z "${TMPDIR:-}" ]; then TMPDIR="$(pwd)/tmp" mkdir -p "$TMPDIR" fi -JAVA_IO_TMPDIR=`mktemp -d -p $TMPDIR -t SANYXXXXXXXXXX` +JAVA_IO_TMPDIR=`mktemp -d -t SANYXXXXXXXXXX` # Check whether the CLI args contains the debug flag if [[ "$*" =~ '--debug' ]] From 7e78e08fa01c702c6fd60f8bb4df8495e1abd1f6 Mon Sep 17 00:00:00 2001 From: Igor Konnov Date: Fri, 13 Dec 2024 20:17:06 +0100 Subject: [PATCH 10/26] add git pull --- script/release-prepare.sh | 1 + 1 file changed, 1 insertion(+) diff --git a/script/release-prepare.sh b/script/release-prepare.sh index be5d5d9bda..ed85f32b44 100755 --- a/script/release-prepare.sh +++ b/script/release-prepare.sh @@ -67,6 +67,7 @@ fi DEV_VERSION=$("$DIR"/get-version.sh) git add --update git commit -m "Bump version to ${DEV_VERSION}" +git pull instructions=" # Reviewer instructions From cbdfc39e43f9d976d580c12a158f005afaff84a0 Mon Sep 17 00:00:00 2001 From: Igor Konnov Date: Fri, 13 Dec 2024 20:51:32 +0100 Subject: [PATCH 11/26] add branch --- script/release-prepare.sh | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/script/release-prepare.sh b/script/release-prepare.sh index ed85f32b44..2ad835beeb 100755 --- a/script/release-prepare.sh +++ b/script/release-prepare.sh @@ -67,7 +67,7 @@ fi DEV_VERSION=$("$DIR"/get-version.sh) git add --update git commit -m "Bump version to ${DEV_VERSION}" -git pull +git pull "release/${RELEASE_VERSION}" instructions=" # Reviewer instructions From 2c19b451ac2d57b7056e958d22e6dd555539d863 Mon Sep 17 00:00:00 2001 From: Igor Konnov Date: Mon, 16 Dec 2024 14:26:21 +0100 Subject: [PATCH 12/26] remove git pull --- script/release-prepare.sh | 1 - 1 file changed, 1 deletion(-) diff --git a/script/release-prepare.sh b/script/release-prepare.sh index 2ad835beeb..be5d5d9bda 100755 --- a/script/release-prepare.sh +++ b/script/release-prepare.sh @@ -67,7 +67,6 @@ fi DEV_VERSION=$("$DIR"/get-version.sh) git add --update git commit -m "Bump version to ${DEV_VERSION}" -git pull "release/${RELEASE_VERSION}" instructions=" # Reviewer instructions From 74fa4e6565a9aae14892b704b8e6508851970913 Mon Sep 17 00:00:00 2001 From: Igor Konnov Date: Mon, 16 Dec 2024 14:37:24 +0100 Subject: [PATCH 13/26] rename sbt to sbtn --- .github/workflows/main.yml | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/.github/workflows/main.yml b/.github/workflows/main.yml index 2b765ef796..47b63a346e 100644 --- a/.github/workflows/main.yml +++ b/.github/workflows/main.yml @@ -96,7 +96,7 @@ jobs: uses: coursier/setup-action@v1 with: jvm: temurin:1.17 - apps: sbt + apps: sbtn - 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 From c5275d6d45cb75ce55d370d8496b6844112b92d8 Mon Sep 17 00:00:00 2001 From: Igor Konnov Date: Mon, 16 Dec 2024 14:43:24 +0100 Subject: [PATCH 14/26] fixing sbt? --- .github/workflows/main.yml | 1 + 1 file changed, 1 insertion(+) diff --git a/.github/workflows/main.yml b/.github/workflows/main.yml index 47b63a346e..4d33397e8f 100644 --- a/.github/workflows/main.yml +++ b/.github/workflows/main.yml @@ -36,6 +36,7 @@ jobs: with: distribution: temurin java-version: 17 + cache: sbt - name: Check formatting run: make fmt-check From 61473a12d13344f86a1a6c2ec0bd18f9b39bcb47 Mon Sep 17 00:00:00 2001 From: Igor Konnov Date: Mon, 16 Dec 2024 14:46:26 +0100 Subject: [PATCH 15/26] install sbt --- .github/workflows/main.yml | 2 ++ 1 file changed, 2 insertions(+) diff --git a/.github/workflows/main.yml b/.github/workflows/main.yml index 4d33397e8f..b33c3e11ac 100644 --- a/.github/workflows/main.yml +++ b/.github/workflows/main.yml @@ -37,6 +37,8 @@ jobs: distribution: temurin java-version: 17 cache: sbt + - name: Install sbt + run: sudo apt-get install -y sbt - name: Check formatting run: make fmt-check From 8448c840bb8219381233ab78ff1790dff77e627d Mon Sep 17 00:00:00 2001 From: Igor Konnov Date: Mon, 16 Dec 2024 14:48:35 +0100 Subject: [PATCH 16/26] fix sbt again? --- .github/workflows/main.yml | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/.github/workflows/main.yml b/.github/workflows/main.yml index b33c3e11ac..6d33971adb 100644 --- a/.github/workflows/main.yml +++ b/.github/workflows/main.yml @@ -37,8 +37,8 @@ jobs: distribution: temurin java-version: 17 cache: sbt - - name: Install sbt - run: sudo apt-get install -y sbt + # see: https://github.com/actions/runner-images/issues/10788 + - uses: sbt/setup-sbt@v1 - name: Check formatting run: make fmt-check From b45605e85286ff715d3f65382192afc088f368fa Mon Sep 17 00:00:00 2001 From: Igor Konnov Date: Mon, 16 Dec 2024 14:51:20 +0100 Subject: [PATCH 17/26] add explicit uses for the new ubuntu image --- .github/workflows/main.yml | 6 ++++++ 1 file changed, 6 insertions(+) diff --git a/.github/workflows/main.yml b/.github/workflows/main.yml index 6d33971adb..f91d6b3f1e 100644 --- a/.github/workflows/main.yml +++ b/.github/workflows/main.yml @@ -53,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 @@ -67,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 @@ -100,6 +104,8 @@ jobs: with: jvm: temurin:1.17 apps: sbtn + # 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 From 92d259c8dc709ebd2741186f85353742e86e52a3 Mon Sep 17 00:00:00 2001 From: Igor Konnov Date: Mon, 16 Dec 2024 14:55:43 +0100 Subject: [PATCH 18/26] s/apps: sbt/apps: sbtn/ --- .github/workflows/main.yml | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/.github/workflows/main.yml b/.github/workflows/main.yml index f91d6b3f1e..4e0ab20e74 100644 --- a/.github/workflows/main.yml +++ b/.github/workflows/main.yml @@ -103,7 +103,7 @@ jobs: uses: coursier/setup-action@v1 with: jvm: temurin:1.17 - apps: sbtn + apps: sbt # see: https://github.com/actions/runner-images/issues/10788 - uses: sbt/setup-sbt@v1 - name: Set APALACHE_HOME env From 4406c88c30065f285042aa38af461d7c9dcc1186 Mon Sep 17 00:00:00 2001 From: Igor Konnov Date: Mon, 16 Dec 2024 14:59:35 +0100 Subject: [PATCH 19/26] fix sbt in docker-tests --- .github/workflows/main.yml | 2 ++ 1 file changed, 2 insertions(+) diff --git a/.github/workflows/main.yml b/.github/workflows/main.yml index 4e0ab20e74..be4e511bf0 100644 --- a/.github/workflows/main.yml +++ b/.github/workflows/main.yml @@ -173,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 From 1c12ee4f6218bd8c19880cadc67777e51854b5fe Mon Sep 17 00:00:00 2001 From: Igor Konnov Date: Mon, 16 Dec 2024 20:46:14 +0100 Subject: [PATCH 20/26] fix sbt --- .github/workflows/prepare-release.yml | 2 ++ 1 file changed, 2 insertions(+) diff --git a/.github/workflows/prepare-release.yml b/.github/workflows/prepare-release.yml index fa189eb981..c7b197d213 100644 --- a/.github/workflows/prepare-release.yml +++ b/.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" From 0afa53d9a5ca98044d350755b5d7c0d8d4c842d5 Mon Sep 17 00:00:00 2001 From: konnov Date: Mon, 16 Dec 2024 20:43:19 +0000 Subject: [PATCH 21/26] [release] 0.47.1 --- RELEASE.md | 8 ++++++++ VERSION | 2 +- 2 files changed, 9 insertions(+), 1 deletion(-) create mode 100644 RELEASE.md diff --git a/RELEASE.md b/RELEASE.md new file mode 100644 index 0000000000..599c68953a --- /dev/null +++ b/RELEASE.md @@ -0,0 +1,8 @@ +## 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 diff --git a/VERSION b/VERSION index 3e9b4751ef..650298f4f7 100644 --- a/VERSION +++ b/VERSION @@ -1 +1 @@ -0.47.1-SNAPSHOT +0.47.1 From 5c3fa9a1ab59ecc49334d1c3bc9ddb0e1a690e74 Mon Sep 17 00:00:00 2001 From: konnov Date: Mon, 16 Dec 2024 20:43:28 +0000 Subject: [PATCH 22/26] Bump version to 0.47.2-SNAPSHOT --- .unreleased/bug-fixes/quint-nullary-operators.md | 1 - .unreleased/bug-fixes/quint-to-tla-transpilation.md | 1 - .unreleased/bug-fixes/sany-tmpdir.md | 1 - .unreleased/bug-fixes/source-tracking-in-vcgen.md | 1 - CHANGES.md | 9 +++++++++ RELEASE.md | 8 -------- VERSION | 2 +- 7 files changed, 10 insertions(+), 13 deletions(-) delete mode 100644 .unreleased/bug-fixes/quint-nullary-operators.md delete mode 100644 .unreleased/bug-fixes/quint-to-tla-transpilation.md delete mode 100644 .unreleased/bug-fixes/sany-tmpdir.md delete mode 100644 .unreleased/bug-fixes/source-tracking-in-vcgen.md delete mode 100644 RELEASE.md diff --git a/.unreleased/bug-fixes/quint-nullary-operators.md b/.unreleased/bug-fixes/quint-nullary-operators.md deleted file mode 100644 index 046a7265a9..0000000000 --- a/.unreleased/bug-fixes/quint-nullary-operators.md +++ /dev/null @@ -1 +0,0 @@ -Fix a problem when translating Quint nullary operators used polymorphically, see #3044 diff --git a/.unreleased/bug-fixes/quint-to-tla-transpilation.md b/.unreleased/bug-fixes/quint-to-tla-transpilation.md deleted file mode 100644 index 217cbaabed..0000000000 --- a/.unreleased/bug-fixes/quint-to-tla-transpilation.md +++ /dev/null @@ -1 +0,0 @@ -Fixed a few problems on parsing Quint and pretty printing TLA, see #3041 diff --git a/.unreleased/bug-fixes/sany-tmpdir.md b/.unreleased/bug-fixes/sany-tmpdir.md deleted file mode 100644 index 8cce6d77c8..0000000000 --- a/.unreleased/bug-fixes/sany-tmpdir.md +++ /dev/null @@ -1 +0,0 @@ -Add extra protection against the SANY race conditions on the filesystem, see #3046 diff --git a/.unreleased/bug-fixes/source-tracking-in-vcgen.md b/.unreleased/bug-fixes/source-tracking-in-vcgen.md deleted file mode 100644 index 04e361c2de..0000000000 --- a/.unreleased/bug-fixes/source-tracking-in-vcgen.md +++ /dev/null @@ -1 +0,0 @@ -Fix source tracking in `VCGenerator` to avoid spurious diagnostic messages, see #3010 diff --git a/CHANGES.md b/CHANGES.md index 8c5b563969..83f77162ae 100644 --- a/CHANGES.md +++ b/CHANGES.md @@ -1,6 +1,15 @@ +## 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 diff --git a/RELEASE.md b/RELEASE.md deleted file mode 100644 index 599c68953a..0000000000 --- a/RELEASE.md +++ /dev/null @@ -1,8 +0,0 @@ -## 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 diff --git a/VERSION b/VERSION index 650298f4f7..e9612abce3 100644 --- a/VERSION +++ b/VERSION @@ -1 +1 @@ -0.47.1 +0.47.2-SNAPSHOT From af3f1e3355a8bb45750f45599f9b3d72a5bdb262 Mon Sep 17 00:00:00 2001 From: Igor Konnov Date: Mon, 16 Dec 2024 22:07:42 +0100 Subject: [PATCH 23/26] add sbt in release :facepaaalm --- .github/workflows/release.yml | 2 ++ 1 file changed, 2 insertions(+) diff --git a/.github/workflows/release.yml b/.github/workflows/release.yml index 1894d3a52d..449b9d2966 100644 --- a/.github/workflows/release.yml +++ b/.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, From c8641031a9e61cf51b4af29aea7884348c858026 Mon Sep 17 00:00:00 2001 From: Igor Konnov Date: Mon, 16 Dec 2024 22:12:29 +0100 Subject: [PATCH 24/26] install sbt in container.yml --- .github/workflows/container.yml | 9 +++++++++ 1 file changed, 9 insertions(+) diff --git a/.github/workflows/container.yml b/.github/workflows/container.yml index 8a67106a92..59e36163ee 100644 --- a/.github/workflows/container.yml +++ b/.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: From def5e8e5e3882e43fece04487e3745a94dcbf109 Mon Sep 17 00:00:00 2001 From: konnov Date: Mon, 16 Dec 2024 23:27:16 +0000 Subject: [PATCH 25/26] [release] 0.47.2 --- RELEASE.md | 1 + VERSION | 2 +- 2 files changed, 2 insertions(+), 1 deletion(-) create mode 100644 RELEASE.md diff --git a/RELEASE.md b/RELEASE.md new file mode 100644 index 0000000000..909b91cebd --- /dev/null +++ b/RELEASE.md @@ -0,0 +1 @@ +## 0.47.2 - 2024-12-16 diff --git a/VERSION b/VERSION index e9612abce3..55a0216801 100644 --- a/VERSION +++ b/VERSION @@ -1 +1 @@ -0.47.2-SNAPSHOT +0.47.2 From a641ab54842e8be633d60b32fd1cabf734075ae6 Mon Sep 17 00:00:00 2001 From: konnov Date: Mon, 16 Dec 2024 23:27:24 +0000 Subject: [PATCH 26/26] Bump version to 0.47.3-SNAPSHOT --- CHANGES.md | 2 ++ RELEASE.md | 1 - VERSION | 2 +- 3 files changed, 3 insertions(+), 2 deletions(-) delete mode 100644 RELEASE.md diff --git a/CHANGES.md b/CHANGES.md index 83f77162ae..547c82a453 100644 --- a/CHANGES.md +++ b/CHANGES.md @@ -1,6 +1,8 @@ +## 0.47.2 - 2024-12-16 + ## 0.47.1 - 2024-12-16 ### Bug fixes diff --git a/RELEASE.md b/RELEASE.md deleted file mode 100644 index 909b91cebd..0000000000 --- a/RELEASE.md +++ /dev/null @@ -1 +0,0 @@ -## 0.47.2 - 2024-12-16 diff --git a/VERSION b/VERSION index 55a0216801..b792f13349 100644 --- a/VERSION +++ b/VERSION @@ -1 +1 @@ -0.47.2 +0.47.3-SNAPSHOT