diff --git a/docs/pages/docs/development-docs/architecture-decision-records/adr001-transpiler-architecture.md b/docs/pages/docs/development-docs/architecture-decision-records/adr001-transpiler-architecture.md index c9e35f412..f481eac89 100644 --- a/docs/pages/docs/development-docs/architecture-decision-records/adr001-transpiler-architecture.md +++ b/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 diff --git a/docs/pages/docs/development-docs/architecture-decision-records/adr005-type-system.md b/docs/pages/docs/development-docs/architecture-decision-records/adr005-type-system.md index 4f8ee6070..34c38776d 100644 --- a/docs/pages/docs/development-docs/architecture-decision-records/adr005-type-system.md +++ b/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. diff --git a/docs/pages/docs/development-docs/architecture-decision-records/adr008-managing-apalache.md b/docs/pages/docs/development-docs/architecture-decision-records/adr008-managing-apalache.md index c0c85c098..4cfb676b0 100644 --- a/docs/pages/docs/development-docs/architecture-decision-records/adr008-managing-apalache.md +++ b/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. \ No newline at end of file + plugin. diff --git a/docs/pages/docs/development-docs/rfcs/rfc007-foreign-calls.md b/docs/pages/docs/development-docs/rfcs/rfc007-foreign-calls.md index 320fc9cba..032aedfa1 100644 --- a/docs/pages/docs/development-docs/rfcs/rfc007-foreign-calls.md +++ b/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 diff --git a/docs/pages/docs/quint.md b/docs/pages/docs/quint.md index 0fe0796cb..54cc8ab1a 100644 --- a/docs/pages/docs/quint.md +++ b/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/ diff --git a/docs/roadmap.md b/docs/roadmap.md index 46aa8176a..f74eb7896 100644 --- a/docs/roadmap.md +++ b/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 diff --git a/quint/README.md b/quint/README.md index 934028173..53fa8a6ff 100644 --- a/quint/README.md +++ b/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 diff --git a/quint/src/cliCommands.ts b/quint/src/cliCommands.ts index c12edb650..76ce0683d 100644 --- a/quint/src/cliCommands.ts +++ b/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(), diff --git a/quint/src/itf.ts b/quint/src/itf.ts index 6cc199be3..6d70109a3 100644 --- a/quint/src/itf.ts +++ b/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) }