Merge branch 'main' into update/sbt-1.10.4

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

project/Dependencies.scala

@@ -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.4
+sbt.version=1.10.5

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.4"
+    "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.4
+sbt.version=1.10.5