Fix broken links globally

CHANGES.md

@@ -317,7 +317,7 @@
 ### Breaking changes
 
 - Invalid configuration keys found in configuration sources (e.g., `apalache.cfg` files) will now produce a configuration error on load (see #2125).
-- The structure of the apalache.cfg has changed. All configuration keys that were previously supported have been moved under the `common` key. You can update your config files by prefixing each key from the previous versions with `commong.key-name`. For an example config file, see https://apalache.informal.systems/docs/apalache/config.html#file-format-and-supported-parameters. See #2065.
+- The structure of the apalache.cfg has changed. All configuration keys that were previously supported have been moved under the `common` key. You can update your config files by prefixing each key from the previous versions with `commong.key-name`. For an example config file, see https://apalache-mc.org/docs/apalache/config.html#file-format-and-supported-parameters. See #2065.
 - Introduce --features=no-rows for the old record syntax and switch to `--features=rows` by default
 
 ### Features
@@ -737,7 +737,7 @@
 ### Documentation
 
  * Restructure and update the Apalache manual:
-   https://apalache.informal.systems/docs/index.html
+   https://apalache-mc.org/docs/index.html
 
 ## 0.17.5
 

CONTRIBUTING.md

@@ -149,7 +149,7 @@ contributors and maintainers to make sure:
 ## Dependencies
 
 For setting up the local build, see the [instructions on building from
-source](https://apalache.informal.systems/docs/apalache/installation/source.html).
+source](https://apalache-mc.org/docs/apalache/installation/source.html).
 
 ### Environment
 

docs/README.md

@@ -3,7 +3,7 @@
 The Apalache documentation is written in markdown files in the [./src](./src)
 directory and compiled using [mdbook](https://github.com/rust-lang/mdBook).
 
-To view the documentation, visit https://apalache.informal.systems/docs/.
+To view the documentation, visit https://apalache-mc.org/docs/.
 
 ## Building and previewing the documentation
 

docs/src/adr/002adr-types.md

@@ -598,8 +598,8 @@ AtMostOne ==
 =============================================================================
 ```
 
-[Snowcat tutorial]: https://apalache.informal.systems/docs/tutorials/snowcat-tutorial.html
-[Snowcat HOWTO]: https://apalache.informal.systems/docs/HOWTOs/howto-write-type-annotations.html
+[Snowcat tutorial]: https://apalache-mc.org/docs/tutorials/snowcat-tutorial.html
+[Snowcat HOWTO]: https://apalache-mc.org/docs/HOWTOs/howto-write-type-annotations.html
 [ADR014]: https://github.com/informalsystems/apalache/blob/main/docs/src/adr/014adr-precise-records.md
 [Issue 401]: https://github.com/informalsystems/apalache/issues/401
 [Row polymorphism]: https://en.wikipedia.org/wiki/Row_polymorphism

docs/src/adr/003adr-trex.md

@@ -116,4 +116,4 @@ explain how the parallel checker is working. This is a subject to another ADR.
 To sum up, this layer is offering you a nice abstraction to write different
 model checking strategies.
 
-[KerA+]: https://apalache.informal.systems/docs/apalache/kera.html
+[KerA+]: https://apalache-mc.org/docs/apalache/kera.html

docs/src/adr/004adr-annotations.md

@@ -158,7 +158,7 @@ This is done because the SANY parser is pruning the linefeed character `\n`,
 so it would be otherwise impossible to find the end of an annotation.
 
 
-[ADR-002]: https://apalache.informal.systems/docs/adr/002adr-types.html
+[ADR-002]: https://apalache-mc.org/docs/adr/002adr-types.html
 [JavaTokenParsers]: https://www.scala-lang.org/api/2.12.2/scala-parser-combinators/scala/util/parsing/combinator/JavaTokenParsers.html
 
 [Java identifier]: https://docs.oracle.com/javase/specs/jls/se7/html/jls-3.html#jls-3.8

docs/src/adr/005adr-json.md

@@ -201,9 +201,9 @@ In general, for any given `oper: TlaOper` of `OperEx`, the value of the `oper` f
 The implementation of the serialization can be found in the class
 `at.forsyte.apalache.io.json.TlaToJson` of the module `tla-import`, see [TlaToJson][].
 
-[ADR-002]: https://apalache.informal.systems/docs/adr/002adr-types.html
+[ADR-002]: https://apalache-mc.org/docs/adr/002adr-types.html
 
-[ADR-004]: https://apalache.informal.systems/docs/adr/004adr-annotations.html
+[ADR-004]: https://apalache-mc.org/docs/adr/004adr-annotations.html
 
 [TlaToJson]: https://github.com/informalsystems/apalache/blob/main/tla-io/src/main/scala/at/forsyte/apalache/io/json/TlaToJson.scala#L54
 [TlaEx]: https://github.com/informalsystems/apalache/blob/main/tlair/src/main/scala/at/forsyte/apalache/tla/lir/TlaEx.scala#L10

docs/src/adr/011adr-smt-arrays.md

@@ -308,14 +308,14 @@ The following changes will be made to implement the new encoding of functions:
 The use of SMT arrays will be restricted to TLA+ sets and functions for the moment. The encoding of
 additional features using SMT arrays, or potentially ADTs, will be left for the future.
 
-[KerA+]: https://apalache.informal.systems/docs/apalache/kera.html
+[KerA+]: https://apalache-mc.org/docs/apalache/kera.html
 [core theory]: http://smtlib.cs.uiowa.edu/theories-Core.shtml
 [arrays with extensionality]: http://smtlib.cs.uiowa.edu/theories-ArraysEx.shtml
 [Z3]: https://github.com/Z3Prover/z3
 [SMT-LIB Standard]: http://smtlib.cs.uiowa.edu/index.shtml
 [Version 2.6]: https://smtlib.cs.uiowa.edu/papers/smt-lib-reference-v2.6-r2017-07-18.pdf
 [TLA+ Model Checking Made Symbolic]: https://dl.acm.org/doi/10.1145/3360549
 [Symbolic Model Checking for TLA+ Made Faster]: https://doi.org/10.1007/978-3-031-30823-9_7
-[model checking parameters]: https://apalache.informal.systems/docs/apalache/running.html#model-checker-command-line-parameters
+[model checking parameters]: https://apalache-mc.org/docs/apalache/running.html#model-checker-command-line-parameters
 [represented internally in Z3]: https://theory.stanford.edu/~nikolaj/programmingz3.html#sec-arrays
 [PR 2027]: https://github.com/informalsystems/apalache/pull/2027

docs/src/adr/014adr-precise-records.md

@@ -15,7 +15,7 @@
 ## 1. Summary
 
 This ADR extends
-[ADR-002](https://apalache.informal.systems/docs/adr/002adr-types.html) on
+[ADR-002](https://apalache-mc.org/docs/adr/002adr-types.html) on
 types and type annotations.
 
 Virtually every user of Snowcat has faced the issue of record type checking
@@ -665,7 +665,7 @@ default untyped implementation for the operators.
 
 
 
-[ADR002]: https://apalache.informal.systems/docs/adr/002adr-types.html
+[ADR002]: https://apalache-mc.org/docs/adr/002adr-types.html
 [#401]: https://github.com/informalsystems/apalache/issues/401
 [#789]: https://github.com/informalsystems/apalache/discussions/789
 [Raft]: https://github.com/ongardie/raft.tla/blob/master/raft.tla

docs/src/adr/015adr-trace.md

@@ -467,8 +467,8 @@ write a parser of custom ITF traces. Hence, we have decided to keep only the obj
 as the more general of the two representations. 
 
 
-[ADR005]: https://apalache.informal.systems/docs/adr/005adr-json.html
-[ADR002]: https://apalache.informal.systems/docs/adr/002adr-types.html
+[ADR005]: https://apalache-mc.org/docs/adr/005adr-json.html
+[ADR002]: https://apalache-mc.org/docs/adr/002adr-types.html
 [MissionariesAndCannibalsTyped]: https://github.com/informalsystems/apalache/blob/main/test/tla/MissionariesAndCannibalsTyped.tla
 [JSON]: https://en.wikipedia.org/wiki/JSON
 [RFC7159]: https://datatracker.ietf.org/doc/html/rfc7159.html

docs/src/adr/023adr-trace-evaluation.md

@@ -137,7 +137,7 @@ and trace `testTrace.json` (length 5, `x=1 -> ... -> x=5`).
 {
   "name": "ApalacheIR",
   "version": "1.0",
-  "description": "https://apalache.informal.systems/docs/adr/005adr-json.html",
+  "description": "https://apalache-mc.org/docs/adr/005adr-json.html",
   "modules": [
     {
       "kind": "TlaModule",

docs/src/apalache/features.md

@@ -4,7 +4,7 @@ Here is the list of the TLA+ language features that are currently supported by A
 
 At the moment, Apalache is able to check state invariants, action invariants,
 temporal properties, trace invariants, as well as inductive invariants. (See the [page on
-invariants](https://apalache.informal.systems/docs/apalache/principles/invariants.html) in
+invariants](https://apalache-mc.org/docs/apalache/principles/invariants.html) in
 the manual.) To check liveness/temporal properties, we employ a [liveness-to-safety][] transformation.
 
 ## Language
@@ -66,7 +66,7 @@ replaced with a constant.
 #### Records
 
 *Use [type
-annotations](https://apalache.informal.systems/docs/tutorials/snowcat-tutorial.html)
+annotations](https://apalache-mc.org/docs/tutorials/snowcat-tutorial.html)
 to help the model checker in finding the right types.* Note that our type
 system distinguishes records from general functions.
 
@@ -81,14 +81,14 @@ system distinguishes records from general functions.
 #### Tuples
 
 *Use [type
-annotations](https://apalache.informal.systems/docs/tutorials/snowcat-tutorial.html)
+annotations](https://apalache-mc.org/docs/tutorials/snowcat-tutorial.html)
 to help the model checker in finding the right types.* Note that our type
 system distinguishes records from general functions.
 
 | Operator               | Supported? | Milestone | Comment                                                                                                                                        |
 |------------------------|:----------:|:---------:|------------------------------------------------------------------------------------------------------------------------------------------------|
 | `e[i]`                 |   ✔ / ✖    |     -     | Provided that `i` is a constant expression                                                                                                     |
-| `<< e1, ..., e_n >>`   |     ✔      |     -     | Use a [type annotation](https://apalache.informal.systems/docs/tutorials/snowcat-tutorial.html) to distinguish between a tuple and a sequence. |
+| `<< e1, ..., e_n >>`   |     ✔      |     -     | Use a [type annotation](https://apalache-mc.org/docs/tutorials/snowcat-tutorial.html) to distinguish between a tuple and a sequence. |
 | `S1 \X ... \X S_n`     |     ✔      |     -     |                                                                                                                                                |
 | `[ t EXCEPT ![i] = e]` |    ✔/✖     |     -     | Provided that `i` is a constant expression                                                                                                     |
 
@@ -158,7 +158,7 @@ For the moment, the model checker does not differentiate between integers and na
 
 | Operator                                                 | Supported? | Milestone | Comment                                                                                                  |
 |----------------------------------------------------------|:----------:|:---------:|----------------------------------------------------------------------------------------------------------|
-| `<<...>>`                                                |     ✔      |           | Often needs a [type annotation](https://apalache.informal.systems/docs/tutorials/snowcat-tutorial.html). |
+| `<<...>>`                                                |     ✔      |           | Often needs a [type annotation](https://apalache-mc.org/docs/tutorials/snowcat-tutorial.html). |
 | `Head`, `Tail`, `Len``, `SubSeq`, `Append`, `\o`, `f[e]` |     ✔      |     -     |                                                                                                          |
 | `EXCEPT`                                                 |     ✔      |           |                                                                                                          |
 | `SelectSeq`                                              |     ✔      |     -     | Not as efficient, as it could be, see [#1350](https://github.com/informalsystems/apalache/issues/1350).  |

docs/src/apalache/principles/apalache-mod.md

@@ -9,4 +9,4 @@ See the detailed description of the [Apalache operators][].
 
 [Apalache.tla]: https://github.com/informalsystems/apalache/tree/main/src/tla/Apalache.tla
 
-[Apalache operators]: https://apalache.informal.systems/docs/lang/apalache-operators.html
+[Apalache operators]: https://apalache-mc.org/docs/lang/apalache-operators.html

docs/src/apalache/principles/assignments.md

@@ -71,7 +71,7 @@ Apalache reports an error as follows:
 ...
 PASS #9: TransitionFinderPass
 To understand the error, [check the
-manual](https://apalache.informal.systems/docs/apalache/principles/assignments.html):
+manual](https://apalache-mc.org/docs/apalache/principles/assignments.html):
 Assignment error: No assignments found for: a
 It took me 0 days  0 hours  0 min  1 sec
 Total time: 1.88 sec

docs/src/apalache/running.md

@@ -22,7 +22,7 @@ The most important commands are as follows:
    the types of all expressions in the parsed specification. It terminates successfully if there are no type errors.
 
  - `simulate` performs all of the operations of `typecheck` and additionally runs the model checker in simulation mode,
-   which *randomly* picks a sequence of [actions](https://apalache.informal.systems/docs/apalache/assignments-in-depth.html#slices)
+   which *randomly* picks a sequence of [actions](https://apalache-mc.org/docs/apalache/assignments-in-depth.html#slices)
    and checks the invariants for the subset of all executions which only admit actions in the selected order. 
    It terminates successfully if there are no invariant violations. 
    This command usually checks randomized symbolic runs much faster than the `check` command.
@@ -32,7 +32,7 @@ The most important commands are as follows:
    the length of which does not exceed the value specified by the `--length` parameter. 
    It terminates successfully if there are no invariant violations.
 
- - `test` performs all of the operations of `check` in a mode that is designed to [test a single action](https://apalache.informal.systems/docs/adr/006rfc-unit-testing.html#32-testing-actions).
+ - `test` performs all of the operations of `check` in a mode that is designed to [test a single action](https://apalache-mc.org/docs/adr/006rfc-unit-testing.html#32-testing-actions).
 
 ## 1. Model checker and simulator command-line parameters
 

docs/src/lang/user/top-level-operators.md

@@ -225,5 +225,5 @@ expression to SMT.
 [Call by macro expansion]: https://en.wikipedia.org/wiki/Evaluation_strategy#Call_by_macro_expansion
 [Alpha conversion]: https://en.wikipedia.org/wiki/Lambda_calculus#%CE%B1-conversion
 [Beta reduction]: https://en.wikipedia.org/wiki/Lambda_calculus#%CE%B2-reduction
-[Apalache]: https://apalache.informal.systems
+[Apalache]: https://apalache-mc.org
 

docs/src/tutorials/entry-tutorial.md

@@ -386,7 +386,7 @@ If it is your first TLA+ specification, you may be surprised by this error:
 ...
 PASS #13: BoundedChecker
 This error may show up when CONSTANTS are not initialized.
-Check the manual: https://apalache.informal.systems/docs/apalache/parameters.html
+Check the manual: https://apalache-mc.org/docs/apalache/parameters.html
 Input error (see the manual): SubstRule: Variable INPUT_SEQ is not assigned a value
 ...
 ```

docs/src/tutorials/pluscal-tutorial.md

@@ -276,7 +276,7 @@ or drop us a message on [Zulip chat].
 [Issue 1412]: https://github.com/informalsystems/apalache/issues/1412
 [open an issue]: https://github.com/informalsystems/apalache/issues
 [Tutorial on Snowcat]: ./snowcat-tutorial.md
-[Checking inductive invariants]: https://apalache.informal.systems/docs/apalache/running.html#checking-an-inductive-invariant
+[Checking inductive invariants]: https://apalache-mc.org/docs/apalache/running.html#checking-an-inductive-invariant
 [TLA+ Cheatsheet in HTML]: https://mbt.informal.systems/docs/tla_basics_tutorials/tla+cheatsheet.html
 [Summary of TLA+]: https://lamport.azurewebsites.net/tla/summary-standalone.pdf
 [TLA+ Video Course]: http://lamport.azurewebsites.net/video/videos.html

mod-infra/src/main/scala/at/forsyte/apalache/infra/ExceptionAdapter.scala

@@ -36,7 +36,7 @@ trait ExceptionAdapter extends LazyLogging {
   def toMessage: PartialFunction[Throwable, ErrorMessage] = { case err: OutOfMemoryError =>
     logger.error(s"Ran out of heap memory (max JVM memory: ${Runtime.getRuntime.maxMemory})")
     logger.error(s"To increase available heap memory, see the manual:")
-    logger.error("  [https://apalache.informal.systems/docs/apalache/running.html#supplying-jvm-arguments]")
+    logger.error("  [https://apalache-mc.org/docs/apalache/running.html#supplying-jvm-arguments]")
     NormalErrorMessage(s"Ran out of heap memory: ${err.getMessage}")
   }
 }

mod-infra/src/main/scala/at/forsyte/apalache/infra/tlc/TlcConfigParser.scala

@@ -9,7 +9,7 @@ import at.forsyte.apalache.infra.tlc.config.TlcConfig
  * href="http://research.microsoft.com/users/lamport/tla/book.html">Specifying Systems</a>, Ch. 14] by Leslie Lamport.
  * TLC configuration files have a rich assignment syntax, e.g., one can write a parameter assignment. The syntax
  * supported by Apalache is described in [<a
- * href="https://apalache.informal.systems/docs/apalache/tlc-config.html">tlc-config</a>].
+ * href="https://apalache-mc.org/docs/apalache/tlc-config.html">tlc-config</a>].
  *
  * @author
  *   Igor Konnov

mod-tool/src/main/scala/at/forsyte/apalache/tla/Tool.scala

@@ -44,7 +44,7 @@ object Tool extends LazyLogging {
         // If it is caught here, logging has not been set up yet, so print directly to `Console.err`.
         Console.err.println(s"Error: Ran out of heap memory (max JVM memory: ${Runtime.getRuntime.maxMemory})")
         Console.err.println(s"To increase available heap memory, see the manual:")
-        Console.err.println("  [https://apalache.informal.systems/docs/apalache/running.html#supplying-jvm-arguments]")
+        Console.err.println("  [https://apalache-mc.org/docs/apalache/running.html#supplying-jvm-arguments]")
         Console.out.println(s"EXITCODE: ERROR (${ExitCodes.ERROR})")
         System.exit(ExitCodes.ERROR)
     }

mod-tool/src/main/scala/at/forsyte/apalache/tla/tooling/opt/ConfigCmd.scala

@@ -19,7 +19,7 @@ class ConfigCmd extends ApalacheCommand(name = "config", description = "Configur
 
   var submitStats: Option[Boolean] = opt[Option[Boolean]](name = "enable-stats",
       description = "Let Apalache submit usage statistics to tlapl.us\n"
-        + "(shared with TLC and TLA+ Toolbox)\nSee: https://apalache.informal.systems/docs/apalache/statistics.html")
+        + "(shared with TLC and TLA+ Toolbox)\nSee: https://apalache-mc.org/docs/apalache/statistics.html")
 
   def run() = {
     logger.info("Configuring Apalache")

test/tla/Antipatterns.tla

@@ -1,7 +1,7 @@
 ---- MODULE Antipatterns ----
 (* Contains a collection of known-to-be-inefficient Apalache constructs, a.k.a. "antipatterns".
 We explain why these constructs are inefficient in 
-https://apalache.informal.systems/docs/apalache/antipatterns.html
+https://apalache-mc.org/docs/apalache/antipatterns.html
 
 The purpose of this file is to collect known antipatterns, so we can measure just how 
 much they affect performance, across various versions of Apalache.

test/tla/MC_ERC20.tla

@@ -4,7 +4,7 @@ EXTENDS Integers, ERC20_typedefs
 
 \* Use the set of three addresses.
 \* We are using uninterpreted values, similar to TLC's model values.
-\* See: https://apalache.informal.systems/docs/HOWTOs/uninterpretedTypes.html
+\* See: https://apalache-mc.org/docs/HOWTOs/uninterpretedTypes.html
 ADDR == { "Alice_OF_ADDR", "Bob_OF_ADDR", "Eve_OF_ADDR" }
 
 \* Apalache can draw constants from the set of all integers