Fix Apalache repository URL

Apalache has recently moved from the `informalsystems` to the `apalache-mc` organization
informalsystems · Aug 19, 2024 · e25a70f · e25a70f
1 parent 7c2c3f7
commit e25a70f
Show file tree

Hide file tree

Showing 18 changed files with 26 additions and 26 deletions.
diff --git a/CONTRIBUTING.md b/CONTRIBUTING.md
@@ -294,8 +294,8 @@ Between installing the plugin from different sources, you may end up with multip
 3. `rm $HOME/.vscode/extensions/.init-default-profile-extensions`.
 4. Restart VSCode **twice**. The first time it will recreate the `extensions.json` file, the second time it will install the extensions. Reloading won't work, you need to actually close and reopen VSCode.
 
-[Apalache]: https://github.com/informalsystems/apalache
-[Contributing to Apalache]: https://github.com/informalsystems/apalache/blob/main/CONTRIBUTING.md
+[Apalache]: https://github.com/apalache-mc/apalache
+[Contributing to Apalache]: https://github.com/apalache-mc/apalache/blob/main/CONTRIBUTING.md
 [eslint]: https://eslint.org/
 [quint manual]: ./docs/pages/docs/architecture-decision-records/quint.md
 [Installing quint]: https://github.com/informalsystems/quint/blob/main/quint/README.md#how-to-install

diff --git a/Makefile b/Makefile
@@ -45,7 +45,7 @@ quint/_build:
 apalache: | $(BUILD_DIR)
 	# remove the previously downloaded archive in case it exists (required by gh)
 	rm -f $(BUILD_DIR)/apalache.tgz
-	gh release download --repo informalsystems/apalache --pattern apalache.tgz --dir $(BUILD_DIR)
+	gh release download --repo apalache-mc/apalache --pattern apalache.tgz --dir $(BUILD_DIR)
 	tar -xvzf $(BUILD_DIR)/apalache.tgz --directory $(BUILD_DIR) > /dev/null
 
 # Alias to update examples readme

diff --git a/README.md b/README.md
@@ -117,7 +117,7 @@ error: Invariant violated
 Check the [Getting Started](https://quint-lang.org/docs/getting-started) guide
 to see how we can fix this problem and formally verify the result.
 
-[Apalache]: https://github.com/informalsystems/apalache
+[Apalache]: https://github.com/apalache-mc/apalache
 [TLA]: https://en.wikipedia.org/wiki/Temporal_logic_of_actions
 
 ### Features
@@ -141,7 +141,7 @@ to see how we can fix this problem and formally verify the result.
   <dd>enabling tests, trace generation, and exploration of your system</dd>
 
   <dt><strong>A symbolic model checker</strong></dt>
-  <dd>to verify your specifications via <a href="https://github.com/informalsystems/apalache">Apalache</a></dd>
+  <dd>to verify your specifications via <a href="https://github.com/apalache-mc/apalache">Apalache</a></dd>
 </dl>
 
 ### Motivation

diff --git a/docs/codetour/lesson3-anatomy/coin.template.qnt b/docs/codetour/lesson3-anatomy/coin.template.qnt
@@ -926,7 +926,7 @@ known that there is always a probability of missing a bug with random search.
 
 If you are looking for better guarantees of correctness, Quint will be soon
 integrated with the
-[Apalache model checker](https://github.com/informalsystems/apalache).
+[Apalache model checker](https://github.com/apalache-mc/apalache).
 The model checker looks for counterexamples more exhaustively, by solving
 equations. In some cases, it may even give you a guarantee that there is no bug,
 if it has not found any.

diff --git a/docs/codetour/lesson3-anatomy/coin.xml b/docs/codetour/lesson3-anatomy/coin.xml
@@ -684,7 +684,7 @@ known that there is always a probability of missing a bug with random search.
 
 If you are looking for better guarantees of correctness, Quint will be soon
 integrated with the
-[Apalache model checker](https://github.com/informalsystems/apalache).
+[Apalache model checker](https://github.com/apalache-mc/apalache).
 The model checker looks for counterexamples more exhaustively, by solving
 equations. In some cases, it may even give you a guarantee that there is no bug,
 if it has not found any.

diff --git a/docs/pages/docs/architecture-decision-records/adr008-managing-apalache.md b/docs/pages/docs/architecture-decision-records/adr008-managing-apalache.md
@@ -343,7 +343,7 @@ still providing a non-managed option:
         third-party package manager binary.
       - Hardcoding the Apalache version is a tradeoff wrt the Github API rate limiting (see §3.2.4) – in principle, we would prefer to pin a minor release (§3.3.4) and use [Github's REST API endpoint][] and/or [`octokit/request.js`][] to determine the appropriate version.
    2. Apalache's JRE dependency is taken care of by adding a check for a `java`
-      executable in `$PATH` to [the `apalache-mc` runner script](https://github.com/informalsystems/apalache/blob/df7adb8b42b6487de9764162f338935121d07a3c/src/universal/bin/apalache-mc#L53).
+      executable in `$PATH` to [the `apalache-mc` runner script](https://github.com/apalache-mc/apalache/blob/df7adb8b42b6487de9764162f338935121d07a3c/src/universal/bin/apalache-mc#L53).
       - This shall print instructions for obtaining a JRE, if none is detected.
 3. Quint launches an on-demand instance of this local installation by spawning
    `apalache-mc server` in a separate process[^1].
@@ -355,9 +355,9 @@ still providing a non-managed option:
        stateful approach of interacting with Shai (e.g., via the [transition
        explorer API][]).
 
-[Apalache]: https://github.com/informalsystems/apalache
-[Shai]: https://github.com/informalsystems/apalache/tree/main/shai
-[transition explorer API]: https://github.com/informalsystems/apalache/blob/df7adb8b42b6487de9764162f338935121d07a3c/docs/src/adr/010rfc-transition-explorer.md
+[Apalache]: https://github.com/apalache-mc/apalache
+[Shai]: https://github.com/apalache-mc/apalache/tree/main/shai
+[transition explorer API]: https://github.com/apalache-mc/apalache/blob/df7adb8b42b6487de9764162f338935121d07a3c/docs/src/adr/010rfc-transition-explorer.md
 [Github's REST API endpoint]: https://docs.github.com/en/rest/releases/releases?apiVersion=2022-11-28#get-the-latest-release
 [`octokit/request.js`]: https://github.com/octokit/request.js
 [semantic versioning]: https://semver.org/

diff --git a/docs/pages/docs/lessons/coin.md b/docs/pages/docs/lessons/coin.md
@@ -966,7 +966,7 @@ known that there is always a probability of missing a bug with random search.
 
 If you are looking for better guarantees of correctness, Quint will be soon
 integrated with the
-[Apalache model checker](https://github.com/informalsystems/apalache).
+[Apalache model checker](https://github.com/apalache-mc/apalache).
 The model checker looks for counterexamples more exhaustively, by solving
 equations. In some cases, it may even give you a guarantee that there is no bug,
 if it has not found any.

diff --git a/docs/pages/docs/rfcs/rfc001-sum-types.md b/docs/pages/docs/rfcs/rfc001-sum-types.md
@@ -261,7 +261,7 @@ define properties common to all shapes like
 We have always planned to support co-products in quint: their utility is
 well known and widely appreciated by engineers with experience in modern
 programming languages. We introduced co-products to Apalache in
-<https://github.com/informalsystems/apalache/milestone/60> for the same
+<https://github.com/apalache-mc/apalache/milestone/60> for the same
 reasons. The design and implementation of the latter was worked out by
 based on the paper ["Extensible Records with Scoped
 Labels"](https://www.microsoft.com/en-us/research/publication/extensible-records-with-scoped-labels/).

diff --git a/docs/pages/docs/rfcs/rfc001-sum-types/rfc001-sum-types.org b/docs/pages/docs/rfcs/rfc001-sum-types/rfc001-sum-types.org
@@ -250,7 +250,7 @@ define properties common to all shapes like
 We have always planned to support co-products in quint: their utility is well
 known and widely appreciated by engineers with experience in modern programming
 languages. We introduced co-products to Apalache in
-[[https://github.com/informalsystems/apalache/milestone/60]] for the same reasons.
+[[https://github.com/apalache-mc/apalache/milestone/60]] for the same reasons.
 The design and implementation of the latter was worked out by [cite/t:@konnov]
 based on the paper [[https://www.microsoft.com/en-us/research/publication/extensible-records-with-scoped-labels/]["Extensible Records with Scoped Labels"]]. At the core of this
 design is a simple use of row-polymorphism that enables both extensible variants

diff --git a/docs/pages/docs/rfcs/rfc001-sum-types/rfc001-sum-types.tex b/docs/pages/docs/rfcs/rfc001-sum-types/rfc001-sum-types.tex
@@ -290,7 +290,7 @@ \subsubsection{Existing plans and previous work}
 We have always planned to support co-products in quint: their utility is well
 known and widely appreciated by engineers with experience in modern programming
 languages. We introduced co-products to Apalache in
-\url{https://github.com/informalsystems/apalache/milestone/60} for the same reasons.
+\url{https://github.com/apalache-mc/apalache/milestone/60} for the same reasons.
 The design and implementation of the latter was worked out by ?? (????)
 based on the paper \href{https://www.microsoft.com/en-us/research/publication/extensible-records-with-scoped-labels/}{``Extensible Records with Scoped Labels''}. At the core of this
 design is a simple use of row-polymorphism that enables both extensible variants

diff --git a/docs/pages/docs/rfcs/rfc007-foreign-calls.md b/docs/pages/docs/rfcs/rfc007-foreign-calls.md
@@ -219,7 +219,7 @@ space outlined by the four examples is quite large.
 [Cosmos Accounts]: https://docs.cosmos.network/v0.45/basics/accounts.html#signatures
 [ITF Format]: https://apalache.informal.systems/docs/adr/015adr-trace.html
 [Quint manual]: /docs/quint
-[Issue 2453]: https://github.com/informalsystems/apalache/issues/2453
+[Issue 2453]: https://github.com/apalache-mc/apalache/issues/2453
 [Issue 143]: https://github.com/informalsystems/quint/issues/143
 [eval]: https://developer.mozilla.org/en-US/docs/Web/JavaScript/Reference/Global_Objects/eval
 [NodeJS VM]: https://nodejs.org/api/vm.html

diff --git a/docs/roadmap.md b/docs/roadmap.md
@@ -44,7 +44,7 @@ completely implementing every pass.
 
 <!-- TODO rm unused links -->
 [Design Principles]: ./design-principles.md
-[Apalache]: https://github.com/informalsystems/apalache
+[Apalache]: https://github.com/apalache-mc/apalache
 [Lessons from Writing a Compiler]: https://borretti.me/article/lessons-writing-compiler
 [Imports]: ./lang.md#imports-1
 [Module definitions]: ./lang.md#module-definition

diff --git a/examples/classic/sequential/BinSearch/BinSearch.qnt b/examples/classic/sequential/BinSearch/BinSearch.qnt
@@ -2,7 +2,7 @@
 /**
  * A tutorial version of binary search. The original TLA+ specification:
  *
- * https://github.com/informalsystems/apalache/blob/main/test/tla/bin-search/BinSearch10.tla
+ * https://github.com/apalache-mc/apalache/blob/main/test/tla/bin-search/BinSearch10.tla
  */
 module BinSearch {
     // the input sequence

diff --git a/examples/verification/README.md b/examples/verification/README.md
@@ -1,3 +1,3 @@
 The specs in this directory demonstrate features of quint's `verify` command,
 which is based on integration with
-[Apalache](https://github.com/informalsystems/apalache).
+[Apalache](https://github.com/apalache-mc/apalache).
diff --git a/quint/src/apalache.ts b/quint/src/apalache.ts
@@ -97,7 +97,7 @@ type ApalacheError = {
 export type ApalacheResult<T> = Either<ApalacheError, T>
 
 // An object representing the Apalache configuration
-// See https://github.com/informalsystems/apalache/blob/main/mod-infra/src/main/scala/at/forsyte/apalache/infra/passes/options.scala#L255
+// See https://github.com/apalache-mc/apalache/blob/main/mod-infra/src/main/scala/at/forsyte/apalache/infra/passes/options.scala#L255
 type ApalacheConfig = any
 
 // Interface to the apalache server
@@ -176,7 +176,7 @@ type AsyncCallBack<T> = (err: any, result: T) => void
 // we therefore record the structure we require from the grpc generation
 // in the following types.
 //
-// The types reflect https://github.com/informalsystems/apalache/blob/main/shai/src/main/protobuf/cmdExecutor.proto
+// The types reflect https://github.com/apalache-mc/apalache/blob/main/shai/src/main/protobuf/cmdExecutor.proto
 
 type RunRequest = { cmd: string; config: string }
 
@@ -336,7 +336,7 @@ async function tryConnect(serverEndpoint: ServerEndpoint, retry: boolean = false
 }
 
 function downloadAndUnpackApalache(): Promise<ApalacheResult<null>> {
-  const url = `https://github.com/informalsystems/apalache/releases/download/v${APALACHE_VERSION_TAG}/apalache.tgz`
+  const url = `https://github.com/apalache-mc/apalache/releases/download/v${APALACHE_VERSION_TAG}/apalache.tgz`
   return fetch(url)
     .then(
       // unpack response body
@@ -373,7 +373,7 @@ async function fetchApalache(verbosityLevel: number): Promise<ApalacheResult<str
   // TODO: This logic makes the CLI tool extremely sensitive to environment.
   // See https://github.com/informalsystems/quint/issues/1124
   // Fetch Github releases
-  // return octokitRequest('GET /repos/informalsystems/apalache/releases').then(
+  // return octokitRequest('GET /repos/apalache-mc/apalache/releases').then(
   //   async resp => {
   //     // Find latest that satisfies `APALACHE_VERSION_TAG`
   //     const versions = resp.data.map((element: any) => element.tag_name)

diff --git a/quint/src/itf.ts b/quint/src/itf.ts
@@ -16,7 +16,7 @@ import { QuintApp, QuintStr } from './ir/quintIr'
 import { QuintEx } from './ir/quintIr'
 
 /** The type of IFT traces.
- * See https://github.com/informalsystems/apalache/blob/main/docs/src/adr/015adr-trace.md */
+ * See https://github.com/apalache-mc/apalache/blob/main/docs/src/adr/015adr-trace.md */
 export type ItfTrace = {
   '#meta'?: any
   params?: string[]

diff --git a/quint/src/quintVerifier.ts b/quint/src/quintVerifier.ts
@@ -24,7 +24,7 @@ import { ApalacheResult, ServerEndpoint, connect } from './apalache'
  *   a server endpoint
  *
  * @param config
- *   an apalache configuration. See https://github.com/informalsystems/apalache/blob/main/mod-infra/src/main/scala/at/forsyte/apalache/infra/passes/options.scala#L255
+ *   an apalache configuration. See https://github.com/apalache-mc/apalache/blob/main/mod-infra/src/main/scala/at/forsyte/apalache/infra/passes/options.scala#L255
  *
  * @returns right(void) if verification succeeds, or left(err) explaining the failure
  */

diff --git a/quint/src/static/toposort.ts b/quint/src/static/toposort.ts
@@ -6,7 +6,7 @@
  * This code is a port of the Scala code from Apalache:
  *
  * ${@link
- * https://github.com/informalsystems/apalache/blob/dd5fff8dbfe707fb450afd2319cf50ebeb568e18/tlair/src/main/scala/at/forsyte/apalache/tla/lir/transformations/impl/StableTopologicalSort.scala
+ * https://github.com/apalache-mc/apalache/blob/dd5fff8dbfe707fb450afd2319cf50ebeb568e18/tlair/src/main/scala/at/forsyte/apalache/tla/lir/transformations/impl/StableTopologicalSort.scala
  * }
  *
  * @author Igor Konnov, Informal Systems, 2023