Merge pull request #1597 from dramarereg/main

docs: fix broken links across multiple documentation files

docs/pages/docs/development-docs/architecture-decision-records/adr001-transpiler-architecture.md

@@ -397,4 +397,4 @@ it may emit an error, see [Errors][].
 
 
 [Errors]: ./adr002-errors
-[Apalache JSON]: https://apalache.informal.systems/docs/adr/005adr-json.html
+[Apalache JSON]: https://apalache-mc.org/docs/adr/005adr-json.html

docs/pages/docs/development-docs/architecture-decision-records/adr005-type-system.md

@@ -18,9 +18,9 @@ be used for:
 Quint's type system should be simple, in consequence of the language design
 decisions that avoid ambiguity present in TLA+, eliminating the need for ad-hoc
 polymorphism. Using [Apalache's type
-system](https://apalache.informal.systems/docs/adr/002adr-types.html) and its
+system](https://apalache-mc.org/docs/adr/002adr-types.html) and its
 [extension for precise
-records](https://apalache.informal.systems/docs/adr/014adr-precise-records.html)
+records](https://apalache-mc.org/docs/adr/014adr-precise-records.html)
 as basis, the proposed type system should be able to infer simple types, match
 annotations and handle row types from records and tuples variants.
 

docs/pages/docs/development-docs/architecture-decision-records/adr008-managing-apalache.md

@@ -161,7 +161,7 @@ Cons:
 
 #### 3.2.3 Using the Github release directly (xcopy-deploy the JAR file)
 
-This is currently the [recommended way for obtaining Apalache](https://apalache.informal.systems/docs/apalache/installation/jvm.html):
+This is currently the [recommended way for obtaining Apalache](https://apalache-mc.org/docs/apalache/installation/jvm.html):
 Download the Github release, and unpack Apalache's JAR file to the target system.
 
 Pros:
@@ -364,4 +364,4 @@ still providing a non-managed option:
 
 [^1]: We should also consider launching a long-running Apalache server from the
       language server, at latest when we're able to run Quint from the VSCode
-      plugin.
+      plugin.

docs/pages/docs/development-docs/rfcs/rfc007-foreign-calls.md

@@ -217,7 +217,7 @@ space outlined by the four examples is quite large.
 [IBC denominations]: https://github.com/cosmos/ibc/blob/main/spec/app/ics-020-fungible-token-transfer/README.md#data-structures
 [SHA-2]: https://en.wikipedia.org/wiki/SHA-2
 [Cosmos Accounts]: https://docs.cosmos.network/v0.45/basics/accounts.html#signatures
-[ITF Format]: https://apalache.informal.systems/docs/adr/015adr-trace.html
+[ITF Format]: https://apalache-mc.org/docs/adr/015adr-trace.html
 [Quint manual]: /docs/quint
 [Issue 2453]: https://github.com/apalache-mc/apalache/issues/2453
 [Issue 143]: https://github.com/informalsystems/quint/issues/143

docs/pages/docs/quint.md

@@ -358,12 +358,12 @@ prerequisite is a [compatible installation of OpenJDK](../quint/README.md).
 You may also manually obtain and run a distribution of Apalache, following these
 steps:
 
-1. Install a distribution of [Apalache](https://apalache.informal.systems/docs/apalache/installation/jvm.html).
+1. Install a distribution of [Apalache](https://apalache-mc.org/docs/apalache/installation/jvm.html).
 2. Start the Apalache server `apalache-mc server` and ensure that it is running.
 
 Apalache uses bounded model checking. This technique checks *all runs* up to
 `--max-steps` steps via [z3][]. Apalache is highly configurable. See [Apalache
-configuration](https://apalache.informal.systems/docs/apalache/config.html?highlight=configuration#apalache-configuration)
+configuration](https://apalache-mc.org/docs/apalache/config.html#apalache-configuration)
 for guidance.
 
 - If there are no critical errors (e.g., in parsing, typechecking, etc.), this
@@ -451,8 +451,8 @@ exact format is to be specified in the future.
 [Source map]: https://docs.google.com/document/d/1U1RGAehQwRypUTovF1KRlpiOFze0b-_2gc6fAH0KY0k/edit
 [Quint IR]: https://github.com/informalsystems/quint/blob/main/quint/src/quintIr.ts
 [REPL]: https://en.wikipedia.org/wiki/Read%E2%80%93eval%E2%80%93print_loop
-[Informal Trace Format]: https://apalache.informal.systems/docs/adr/015adr-trace.html
+[Informal Trace Format]: https://apalache-mc.org/docs/adr/015adr-trace.html
 [ITF Trace Viewer]: https://marketplace.visualstudio.com/items?itemName=informal.itf-trace-viewer
 [jq]: https://stedolan.github.io/jq/
 [z3]: https://github.com/z3prover/z3
-[Apalache]: https://apalache.informal.systems/
+[Apalache]: https://apalache-mc.org/

docs/roadmap.md

@@ -87,6 +87,6 @@ completely implementing every pass.
 [Tutorials]: ./tutorials/README.md
 [Quint zulip stream]: https://informal-systems.zulipchat.com/#narrow/stream/378959-quint
 [Quint discussions]: https://github.com/informalsystems/quint/discussions
-[ITF traces]: https://apalache.informal.systems/docs/adr/015adr-trace.html
+[ITF traces]: https://apalache-mc.org/docs/adr/015adr-trace.html
 [ITF Trace Viewer]: https://marketplace.visualstudio.com/items?itemName=informal.itf-trace-viewer
 [15 minute intro to Quint]: https://youtu.be/OZIX8rs-kOA

quint/README.md

@@ -148,7 +148,7 @@ npm run apalache-integration
 ```
 
 It is required that you have a Java version meeting [Apalache's minimum
-requirements](https://apalache.informal.systems/docs/apalache/installation/jvm.html).
+requirements](https://apalache-mc.org/docs/apalache/installation/jvm.html).
 
 ### Parser
 

quint/src/cliCommands.ts

@@ -959,7 +959,7 @@ function addItfHeader(source: string, status: string, traceInJson: any): any {
   return {
     '#meta': {
       format: 'ITF',
-      'format-description': 'https://apalache.informal.systems/docs/adr/015adr-trace.html',
+      'format-description': 'https://apalache-mc.org/docs/adr/015adr-trace.html',
       source,
       status,
       description: 'Created by Quint on ' + new Date(),

quint/src/itf.ts

@@ -1,6 +1,6 @@
 /*
  * Support for the Informal Trace Format (ITF):
- * https://apalache.informal.systems/docs/adr/015adr-trace.html
+ * https://apalache-mc.org/docs/adr/015adr-trace.html
  *
  * Igor Konnov, Shon Feder, Informal Systems, 2023
  *
@@ -202,7 +202,7 @@ export function ofItf(itf: ItfTrace): QuintEx[] {
     } else if (typeof value === 'number') {
       // We never encode an integer as a JS number,
       // but we consume it for backwards compatibility with older ITF traces.
-      // See: https://apalache.informal.systems/docs/adr/015adr-trace.html
+      // See: https://apalache-mc.org/docs/adr/015adr-trace.html
       return { id, kind: 'int', value: BigInt(value) }
     } else if (Array.isArray(value)) {
       return { id, kind: 'app', opcode: 'List', args: value.map(ofItfValue) }