chore: commit tla2tools jar to the repo

Author: roman-kashitsyn

.gitlab/CODEOWNERS

@@ -14,7 +14,6 @@
 
 # [Bazel]
 /bazel/                   @dfinity-lab/teams/idx
-/tlaplus/                 @dfinity-lab/teams/idx
 /third_party/             @dfinity-lab/teams/idx
 /toolchains/              @dfinity-lab/teams/idx
 /WORKSPACE.bazel          @dfinity-lab/teams/idx

WORKSPACE.bazel

@@ -330,12 +330,6 @@ load("@aspect_bazel_lib//lib:repositories.bzl", "aspect_bazel_lib_dependencies")
 aspect_bazel_lib_dependencies()
 
 # TLA+ tools
-http_jar(
-    name = "tlaplus",
-    sha256 = "6bd4b937968f7f80ea61891e79d171d3cccdf1f4e409fb841986656976ab9d32",
-    url = "https://github.com/tlaplus/tlaplus/releases/download/v1.8.0/tla2tools.jar",
-)
-
 http_jar(
     name = "tlaplus_community_modules",
     sha256 = "109e0828d192c33703d5cbc50b5b6e128acd816565616e27b3855949c7baba9c",

tlaplus/BUILD.bazel renamed to bazel/tlaplus/BUILD.bazel

@@ -2,7 +2,7 @@
 # description of the TLA+ command-line tools.
 
 COMMON_DEPS = [
-    "@tlaplus//jar",
+    "//third_party/tlaplus-1.8.0:tla2tools",
     "@tlaplus_community_modules//jar",
     "@tlaplus_community_modules_deps//jar",
 ]

tlaplus/defs.bzl renamed to bazel/tlaplus/defs.bzl

@@ -40,7 +40,7 @@ tla_module = rule(
 Declares a single TLA+ module.
 
 ```python
-load("//tlaplus:defs.bzl", "tla_module")
+load("//bazel/tlaplus:defs.bzl", "tla_module")
 
 tla_module(
     name = "spec",
@@ -81,14 +81,14 @@ tlc_test = rule(
     attrs = {
         "spec": attr.label(providers = [TlaModuleInfo]),
         "config": attr.label(allow_single_file = [".cfg"]),
-        "_tlc": attr.label(default = "//tlaplus:tlc", executable = True, cfg = "exec"),
+        "_tlc": attr.label(default = "//bazel/tlaplus:tlc", executable = True, cfg = "exec"),
     },
     test = True,
     doc = """\
 Defines a test that runs TLC on a specification.
 
 ```python
-load("//tlaplus:defs.bzl", "tla_module", "tlc_test")
+load("//bazel/tlaplus:defs.bzl", "tla_module", "tlc_test")
 
 tla_module(
     name = "spec",
@@ -133,7 +133,7 @@ sany_test = rule(
     attrs = {
         "module": attr.label(providers = [TlaModuleInfo]),
         "_sany": attr.label(
-            default = Label("//tlaplus:sany"),
+            default = Label("//bazel/tlaplus:sany"),
             executable = True,
             cfg = "exec",
         ),

rs/bitcoin/ckbtc/spec/BUILD.bazel

@@ -1,4 +1,4 @@
-load("//tlaplus:defs.bzl", "sany_test", "tla_module", "tlc_test")
+load("//bazel/tlaplus:defs.bzl", "sany_test", "tla_module", "tlc_test")
 
 tla_module(
     name = "tla_hash",

rs/state_manager/spec/BUILD.bazel

@@ -1,4 +1,4 @@
-load("//tlaplus:defs.bzl", "sany_test", "tla_module", "tlc_test")
+load("//bazel/tlaplus:defs.bzl", "sany_test", "tla_module", "tlc_test")
 
 tla_module(
     name = "spec",

third_party/tlaplus-1.8.0/BUILD.bazel

@@ -0,0 +1,16 @@
+"""
+This package provides a stable version of the TLA+ tools.
+Visit https://github.com/tlaplus/tlaplus/releases if you need to update the jar file.
+"""
+
+package(default_visibility = ["//visibility:public"])
+
+# NOTE: we committed the jar to the repo because version 1.8.0 is
+# in pre-release stage so its artifact hash keeps changing.
+# We should switch to the official 1.8.0 release once it's available.
+java_import(
+    name = "tla2tools",
+    jars = [
+        ":tla2tools.jar",
+    ],
+)