Merge branch 'main' into gabriela/quint-to-tla-improvements

README.md

@@ -145,7 +145,6 @@ Related reports and publications can be found at the
 [releases page]: https://github.com/apalache-mc/apalache/releases
 [master]: https://github.com/apalache-mc/apalache/tree/master
 [main branch]: https://github.com/apalache-mc/apalache/tree/main
-[apalache zulip stream]: https://informal-systems.zulipchat.com/#narrow/stream/265309-apalache
 [tendermint specs]: https://github.com/tendermint/tendermint/tree/master/spec/light-client/accountability
 [tendermint blockchain]: https://github.com/tendermint
 [standard repository of tla+ examples]: https://github.com/tlaplus/Examples

docs/src/adr/006rfc-unit-testing.md

@@ -621,14 +621,14 @@ By having all test options specified directly in tests, we reach two goals:
 
 Let us know:
 
- - At [Apalache Zulip stream][],
+ - At [Apalache Discourse][],
 
  - On [ApalacheTLA Twitter][],
 
  - email: igor at informal.systems.
 
 
-[Apalache Zulip stream]: https://informal-systems.zulipchat.com/#narrow/stream/265309-apalache
+[Apalache Discourse]: https://apalache.discourse.group/
 [ApalacheTLA Twitter]: https://twitter.com/ApalacheTLA
 [Unit testing]: https://en.wikipedia.org/wiki/Unit_testing
 [Property-based testing]: https://en.wikipedia.org/wiki/QuickCheck

docs/src/lang/variants.md

@@ -73,12 +73,12 @@ To make it easier to represent the fruits, we can introduce variants together wi
 user-defined constructors for each option::
 
 ```tla
-\* @typeAlias: FRUIT = Apple(Str) | Orange(Bool);
+\* @typeAlias: fruit = Apple(Str) | Orange(Bool);
 
-\* @type: Str => FRUIT;
+\* @type: Str => $fruit;
 Apple(color) == Variant("Apple", color)
 
-\* @type: Bool => FRUIT;
+\* @type: Bool => $fruit;
 Orange(seedless) == Variant("Orange", seedless)
 ```
 
@@ -92,20 +92,20 @@ Orange(TRUE)
 Variants can wrap records, for when we want to represent compound data with named fields:
 
 ```tla
-\* @typeAlias: DRINK =
+\* @typeAlias: drink =
 \*     Water({ sparkling: Bool })
 \*   | Beer({ malt: Str, strength: Int });
 \*
-\* @type: Bool => DRINK;
+\* @type: Bool => $drink;
 Water(sparkling) == Variant("Water", [ sparkling |-> sparkling ])
 
-\* @type: (Str, Int) => DRINK;
+\* @type: (Str, Int) => $drink;
 Beer(malt, strength) == Variant("Beer", [ malt |-> malt, strength |-> strength ])
 ```
 
 Once a variant is constructed, it becomes opaque to the type checker, that is,
 the type checker only knows that `Water(TRUE)` and `Beer("Dark", 5)` are both
-of type `DRINK`. This is exactly what we want, in order to combine these values
+of type `drink`. This is exactly what we want, in order to combine these values
 in a single set. However, we have lost the ability to access the fields of
 these values. To deconstruct values of a variant type, we have to use other
 operators, presented below.
@@ -115,7 +115,7 @@ untyped TLA+, we can filter a set of variants:
 
 ```tla
 LET Drinks == { Water(TRUE), Water(FALSE), Beer("Radler", 2) } IN
-\E d \in VariantFilter("Beer", Drink):
+\E d \in VariantFilter("Beer", Drinks):
     d.strength < 3
 ```
 
@@ -195,14 +195,14 @@ type variable that captures other options in the variant type.
 **Example in TLA+:**
 
 ```tla
-\* @typeAlias: DRINK =
+\* @typeAlias: drink =
 \*     Water({ sparkling: Bool })
 \*   | Beer({ malt: Str, strength: Int });
 \*
-\* @type: Bool => DRINK;
+\* @type: Bool => $drink;
 Water(sparkling) == Variant("Water", [ sparkling |-> sparkling ])
 
-\* @type: (Str, Int) => DRINK;
+\* @type: (Str, Int) => $drink;
 Beer(malt, strength) == Variant("Beer", [ malt |-> malt, strength |-> strength ])
 ```
 
@@ -260,14 +260,14 @@ values that were packed with `Variant`.
 **Example in TLA+:**
 
 ```tla
-\* @typeAlias: DRINK =
+\* @typeAlias: drink =
 \*     Water({ sparkling: Bool })
 \*   | Beer({ malt: Str, strength: Int });
 \*
-\* @type: Bool => DRINK;
+\* @type: Bool => $drink;
 Water(sparkling) == Variant("Water", [ sparkling |-> sparkling ])
 
-\* @type: (Str, Int) => DRINK;
+\* @type: (Str, Int) => $drink;
 Beer(malt, strength) == Variant("Beer", [ malt |-> malt, strength |-> strength ])
 
 LET Drinks == { Water(TRUE), Water(FALSE), Beer("Radler", 2) } IN
@@ -303,14 +303,14 @@ Otherwise, the operator returns `defaultValue`.
 **Example in TLA+:**
 
 ```tla
-\* @typeAlias: DRINK =
+\* @typeAlias: drink =
 \*     Water({ sparkling: Bool })
 \*   | Beer({ malt: Str, strength: Int });
 \*
-\* @type: Bool => DRINK;
+\* @type: Bool => $drink;
 Water(sparkling) == Variant("Water", [ sparkling |-> sparkling ])
 
-\* @type: (Str, Int) => DRINK;
+\* @type: (Str, Int) => $drink;
 Beer(malt, strength) == Variant("Beer", [ malt |-> malt, strength |-> strength ])
 
 LET water == Water(TRUE) IN
@@ -348,14 +348,14 @@ is always constructed via `Variant`, unless the operator is used with the right
 **Example in TLA+:**
 
 ```tla
-\* @typeAlias: DRINK =
+\* @typeAlias: drink =
 \*     Water({ sparkling: Bool })
 \*   | Beer({ malt: Str, strength: Int });
 \*
-\* @type: Bool => DRINK;
+\* @type: Bool => $drink;
 Water(sparkling) == Variant("Water", [ sparkling |-> sparkling ])
 
-\* @type: (Str, Int) => DRINK;
+\* @type: (Str, Int) => $drink;
 Beer(malt, strength) == Variant("Beer", [ malt |-> malt, strength |-> strength ])
 
 LET drink == Beer("Dunkles", 4) IN

docs/src/tutorials/entry-tutorial.md

@@ -1175,7 +1175,7 @@ did not discuss non-determinism, as our specification is entirely
 deterministic. We will demonstrate advanced features in future tutorials.
 
 If you are experiencing a problem with Apalache, feel free to [open an issue]
-or drop us a message on [Zulip chat].
+or drop us a message on [Discourse].
 
 
 [HOWTO on writing type annotations]: ../HOWTOs/howto-write-type-annotations.md
@@ -1205,5 +1205,5 @@ or drop us a message on [Zulip chat].
 [Specifying Systems]: http://lamport.azurewebsites.net/tla/book.html?back-link=learning.html
 [Test-driven development]: https://en.wikipedia.org/wiki/Test-driven_development
 [TLC]: https://github.com/tlaplus/tlaplus/
-[Zulip chat]: https://informal-systems.zulipchat.com/login/#narrow/stream/265309-apalache
+[Discourse]: https://apalache.discourse.group/
 [ZIP archive]: https://download-directory.github.io/?url=https://github.com/informalsystems/apalache/tree/main/test/tla/bin-search

docs/src/tutorials/pluscal-tutorial.md

@@ -256,7 +256,7 @@ In this tutorial, we have shown how to:
    `N=4`).
 
 If you are experiencing a problem with Apalache, feel free to [open an issue]
-or drop us a message on [Zulip chat].
+or drop us a message on [Discourse].
 
 ## Further reading
 
@@ -284,6 +284,6 @@ or drop us a message on [Zulip chat].
 [Specifying Systems]: http://lamport.azurewebsites.net/tla/book.html?back-link=learning.html
 [TLC]: https://github.com/tlaplus/tlaplus/
 [TLAPS]: https://tla.msr-inria.inria.fr/tlaps/content/Home.html
-[Zulip chat]: https://informal-systems.zulipchat.com/login/#narrow/stream/265309-apalache
+[Discourse]: https://apalache.discourse.group/
 [Bakery algorithm]: https://en.wikipedia.org/wiki/Lamport%27s_bakery_algorithm
 [ZIP archive]: https://download-directory.github.io/?url=https://github.com/informalsystems/apalache/tree/main/test/tla/bakery-pluscal

docs/src/tutorials/snowcat-tutorial.md

@@ -292,7 +292,7 @@ type checker. To learn about type aliases, see [HOWTO on writing type
 annotations][].
 
 If you are experiencing a problem with Snowcat, feel free to [open an issue][]
-or drop us a message on [Zulip chat][].
+or drop us a message on [Discourse][].
 
 
 [ADR002]: ../adr/002adr-types.md
@@ -312,5 +312,5 @@ or drop us a message on [Zulip chat][].
 [CarTalkPuzzleTyped.tla]: https://github.com/informalsystems/apalache/blob/main/test/tla/CarTalkPuzzleTyped.tla
 [QueensTyped.tla]: https://github.com/informalsystems/apalache/blob/main/test/tla/QueensTyped.tla
 [open an issue]: https://github.com/informalsystems/apalache/issues
-[Zulip chat]: https://informal-systems.zulipchat.com/login/#narrow/stream/265309-apalache
+[Discourse]: https://apalache.discourse.group/
 [Idiom 15]: ../idiomatic/003record-sets.md

project/Dependencies.scala

@@ -12,7 +12,7 @@ object Dependencies {
 
   object Deps {
     // Versions
-    lazy val logbackVersion = "1.5.8"
+    lazy val logbackVersion = "1.5.12"
     lazy val clistVersion = "3.5.1"
 
     // Libraries
@@ -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.0"
+    val grpcNetty = "io.grpc" % "grpc-netty" % "1.68.1"
     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)

project/build.properties

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

project/plugins.sbt

@@ -7,7 +7,7 @@ addSbtPlugin("se.marcuslonnberg" % "sbt-docker" % "1.11.0")
 // https://github.com/scoverage/sbt-scoverage
 addSbtPlugin("org.scoverage" % "sbt-scoverage" % "2.2.1")
 // https://github.com/sbt/sbt-buildinfo
-addSbtPlugin("com.eed3si9n" % "sbt-buildinfo" % "0.12.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.3"
+    "org.scala-sbt" % "sbt" % "1.10.5"
 )
 
 lazy val sbt_changeling = (project in file("."))

project/sbt-changeling/project/build.properties

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