From bbfce06450ae28cf53a2e93c329204d6d54f32c7 Mon Sep 17 00:00:00 2001 From: oliveredget <188809800+oliveredget@users.noreply.github.com> Date: Sat, 28 Dec 2024 11:57:06 +0800 Subject: [PATCH 01/11] Fix typo --- docs/codetour/.tours/coin.tour | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/docs/codetour/.tours/coin.tour b/docs/codetour/.tours/coin.tour index a630f2317..0f567c1d4 100644 --- a/docs/codetour/.tours/coin.tour +++ b/docs/codetour/.tours/coin.tour @@ -22,7 +22,7 @@ }, { "title": "Declare pure functions", - "description": "\n\nIt often happens that a protocol requires auxilliary definitions that do not\ndepend on the protocol state, but only on the values of their parameters.\nSuch computations are often called \"pure\". In the above code, we define two\npure definitions:\n \n - The pure value `MAX_UINT`.\n\n - The pure definition `isUInt` that computes if a given integer `i` is within\n the range from 0 to MAX_UINT (inclusive).\n\nThe main property of pure values is that they always return the same value.\nPure definitions always return the same value, if they are supplied with the\nsame arguments.\n\nTo see that no state is needed, evaluate these definitions in REPL\n(read-evaluate-print-loop):\n\n \n>> echo \"MAX_UINT\" | quint -r ./lesson3-anatomy/coin.qnt::coin\n\n\n>> echo \"isUInt(22)\" | quint -r ./lesson3-anatomy/coin.qnt::coin\n\n\n>> echo \"isUInt(-1)\" | quint -r ./lesson3-anatomy/coin.qnt::coin\n\n\n>> echo \"isUInt(MAX_UINT + 1)\" | quint -r ./lesson3-anatomy/coin.qnt::coin\n\n\n\nThe functional layer is actually quite powerful; a lot of protocol behavior can\nbe defined here without referring to protocol state.\n\nAs you can see, we have omitted the type of `MAX_UINT` but specified the type of\n`isUInt`. Most of the time, the type checker can infer the types of values and\noperator definitions, and giving additional type annotations is up to you. In\nrare cases, the type checker may get confused, and then explicit type\nannotations will help you in figuring out the issue.\n ", + "description": "\n\nIt often happens that a protocol requires auxiliary definitions that do not\ndepend on the protocol state, but only on the values of their parameters.\nSuch computations are often called \"pure\". In the above code, we define two\npure definitions:\n \n - The pure value `MAX_UINT`.\n\n - The pure definition `isUInt` that computes if a given integer `i` is within\n the range from 0 to MAX_UINT (inclusive).\n\nThe main property of pure values is that they always return the same value.\nPure definitions always return the same value, if they are supplied with the\nsame arguments.\n\nTo see that no state is needed, evaluate these definitions in REPL\n(read-evaluate-print-loop):\n\n \n>> echo \"MAX_UINT\" | quint -r ./lesson3-anatomy/coin.qnt::coin\n\n\n>> echo \"isUInt(22)\" | quint -r ./lesson3-anatomy/coin.qnt::coin\n\n\n>> echo \"isUInt(-1)\" | quint -r ./lesson3-anatomy/coin.qnt::coin\n\n\n>> echo \"isUInt(MAX_UINT + 1)\" | quint -r ./lesson3-anatomy/coin.qnt::coin\n\n\n\nThe functional layer is actually quite powerful; a lot of protocol behavior can\nbe defined here without referring to protocol state.\n\nAs you can see, we have omitted the type of `MAX_UINT` but specified the type of\n`isUInt`. Most of the time, the type checker can infer the types of values and\noperator definitions, and giving additional type annotations is up to you. In\nrare cases, the type checker may get confused, and then explicit type\nannotations will help you in figuring out the issue.\n ", "line": 38, "file": "lesson3-anatomy/coin.qnt" }, From 260decb9ee7b65b19af258ae53de3da25c1f3f04 Mon Sep 17 00:00:00 2001 From: oliveredget <188809800+oliveredget@users.noreply.github.com> Date: Sat, 28 Dec 2024 11:57:26 +0800 Subject: [PATCH 02/11] Fix typo --- docs/codetour/.tours/hello.tour | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/docs/codetour/.tours/hello.tour b/docs/codetour/.tours/hello.tour index f713ec19d..c77e8c319 100644 --- a/docs/codetour/.tours/hello.tour +++ b/docs/codetour/.tours/hello.tour @@ -34,7 +34,7 @@ }, { "title": "Introduce an action by the computer", - "description": "\n\nNow it's time to print the \"Hello, world!\" message. Similar to `init`, we\nintroduce the action `write`. In contrast to `init`, this action cannot be\nunconditionally executed in any state of our state machine. Similar to how the\nvariable `consoleOutput` is updated in the action `init`, you should be able to\nsee how the action `write` schedules an update of `consoleOutput` in the next\nstate. This only happens though, if the action `write` returns `true`.\n\nThe first statement of `write` may be confusing to you though:\n\n```scala\n consoleOutput == \"\"\n```\n\nIf you are familiar with C, Java, JavaScript and similar languages, this\nstatement looks useless, as in those languages such an expression would be\nevaluated and its result would be simply dropped. Moreover, in a static\nlanguage such a statement could be simply removed by the compiler as\nfruitless at the optimization stage.\n\nIn Quint, things are a bit different. Recall the discussion about the\naction `init` at the previous step. Assignments return `true` and\n`all { ... }` returns true only if all of its arguments return `true`.\nThe same principle applies to the expression `consoleOutput == \"\"`.\nIf `consoleOutput == \"\"` evaluates to `true` in the current state\nof the state machine, then the enclosing expression `all { ... }`\nevaluates to `true`, and only then the action `write` evaluates to `true`\nand it may produce the next state.\n\nFinally, the third statement may look useless to you too:\n\n```scala\n readByUser' = readByUser,\n```\n\nWhy shall we say that `readByUser` keeps its value in the next state?\nMost likely, we will be able to automatically infer this in the future.\nIn the current version of Quint, if an action is used to execute transitions,\nit has to explicitely assign values to all of the state variables.\n ", + "description": "\n\nNow it's time to print the \"Hello, world!\" message. Similar to `init`, we\nintroduce the action `write`. In contrast to `init`, this action cannot be\nunconditionally executed in any state of our state machine. Similar to how the\nvariable `consoleOutput` is updated in the action `init`, you should be able to\nsee how the action `write` schedules an update of `consoleOutput` in the next\nstate. This only happens though, if the action `write` returns `true`.\n\nThe first statement of `write` may be confusing to you though:\n\n```scala\n consoleOutput == \"\"\n```\n\nIf you are familiar with C, Java, JavaScript and similar languages, this\nstatement looks useless, as in those languages such an expression would be\nevaluated and its result would be simply dropped. Moreover, in a static\nlanguage such a statement could be simply removed by the compiler as\nfruitless at the optimization stage.\n\nIn Quint, things are a bit different. Recall the discussion about the\naction `init` at the previous step. Assignments return `true` and\n`all { ... }` returns true only if all of its arguments return `true`.\nThe same principle applies to the expression `consoleOutput == \"\"`.\nIf `consoleOutput == \"\"` evaluates to `true` in the current state\nof the state machine, then the enclosing expression `all { ... }`\nevaluates to `true`, and only then the action `write` evaluates to `true`\nand it may produce the next state.\n\nFinally, the third statement may look useless to you too:\n\n```scala\n readByUser' = readByUser,\n```\n\nWhy shall we say that `readByUser` keeps its value in the next state?\nMost likely, we will be able to automatically infer this in the future.\nIn the current version of Quint, if an action is used to execute transitions,\nit has to explicitly assign values to all of the state variables.\n ", "line": 25, "file": "lesson0-helloworld/hello.qnt" }, From 1769bd2af89cfd5814ee937f660f44e7a83eeece Mon Sep 17 00:00:00 2001 From: oliveredget <188809800+oliveredget@users.noreply.github.com> Date: Sat, 28 Dec 2024 11:59:11 +0800 Subject: [PATCH 03/11] Fix typo --- docs/codetour/lesson0-helloworld/hello.template.qnt | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/docs/codetour/lesson0-helloworld/hello.template.qnt b/docs/codetour/lesson0-helloworld/hello.template.qnt index d204a7bfe..dcd3182a6 100644 --- a/docs/codetour/lesson0-helloworld/hello.template.qnt +++ b/docs/codetour/lesson0-helloworld/hello.template.qnt @@ -181,7 +181,7 @@ Finally, the third statement may look useless to you too: Why shall we say that `readByUser` keeps its value in the next state? Most likely, we will be able to automatically infer this in the future. In the current version of Quint, if an action is used to execute transitions, -it has to explicitely assign values to all of the state variables. +it has to explicitly assign values to all of the state variables. !*/ From 980ee039ffce9ea15417192cf0b888ff14943a63 Mon Sep 17 00:00:00 2001 From: oliveredget <188809800+oliveredget@users.noreply.github.com> Date: Sat, 28 Dec 2024 11:59:11 +0800 Subject: [PATCH 04/11] Fix typo --- docs/codetour/lesson0-helloworld/hello.xml | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/docs/codetour/lesson0-helloworld/hello.xml b/docs/codetour/lesson0-helloworld/hello.xml index 991e96d05..8fdec224a 100644 --- a/docs/codetour/lesson0-helloworld/hello.xml +++ b/docs/codetour/lesson0-helloworld/hello.xml @@ -145,7 +145,7 @@ Finally, the third statement may look useless to you too: Why shall we say that `readByUser` keeps its value in the next state? Most likely, we will be able to automatically infer this in the future. In the current version of Quint, if an action is used to execute transitions, -it has to explicitely assign values to all of the state variables. +it has to explicitly assign values to all of the state variables. From 3fb5eb8e6b5b9e2660a7395dee7a1c27d44c3a59 Mon Sep 17 00:00:00 2001 From: oliveredget <188809800+oliveredget@users.noreply.github.com> Date: Sat, 28 Dec 2024 11:59:11 +0800 Subject: [PATCH 05/11] Fix typo --- docs/codetour/lesson3-anatomy/coin.template.qnt | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/docs/codetour/lesson3-anatomy/coin.template.qnt b/docs/codetour/lesson3-anatomy/coin.template.qnt index 5fa122909..b75afe6a7 100644 --- a/docs/codetour/lesson3-anatomy/coin.template.qnt +++ b/docs/codetour/lesson3-anatomy/coin.template.qnt @@ -143,7 +143,7 @@ different kinds of "integers", when they are referred to via different type alia Declare pure functions -It often happens that a protocol requires auxilliary definitions that do not +It often happens that a protocol requires auxiliary definitions that do not depend on the protocol state, but only on the values of their parameters. Such computations are often called "pure". In the above code, we define two pure definitions: From f87116851b899e92ebef563002b380d02af8d251 Mon Sep 17 00:00:00 2001 From: oliveredget <188809800+oliveredget@users.noreply.github.com> Date: Sat, 28 Dec 2024 11:59:11 +0800 Subject: [PATCH 06/11] Fix typo --- docs/codetour/lesson3-anatomy/coin.xml | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/docs/codetour/lesson3-anatomy/coin.xml b/docs/codetour/lesson3-anatomy/coin.xml index 9c713f2c3..3c8832a11 100644 --- a/docs/codetour/lesson3-anatomy/coin.xml +++ b/docs/codetour/lesson3-anatomy/coin.xml @@ -98,7 +98,7 @@ different kinds of "integers", when they are referred to via different type alia Declare pure functions -It often happens that a protocol requires auxilliary definitions that do not +It often happens that a protocol requires auxiliary definitions that do not depend on the protocol state, but only on the values of their parameters. Such computations are often called "pure". In the above code, we define two pure definitions: From 13a29e4a851852a1b7d51493a229c812db568b59 Mon Sep 17 00:00:00 2001 From: oliveredget <188809800+oliveredget@users.noreply.github.com> Date: Sat, 28 Dec 2024 11:59:11 +0800 Subject: [PATCH 07/11] Fix typo --- .../adr008-managing-apalache.md | 8 ++++---- 1 file changed, 4 insertions(+), 4 deletions(-) diff --git a/docs/pages/docs/architecture-decision-records/adr008-managing-apalache.md b/docs/pages/docs/architecture-decision-records/adr008-managing-apalache.md index c3a4146a8..c0c85c098 100644 --- a/docs/pages/docs/architecture-decision-records/adr008-managing-apalache.md +++ b/docs/pages/docs/architecture-decision-records/adr008-managing-apalache.md @@ -138,7 +138,7 @@ Pros: Cons: - Requires differing per-platform docs/instructions. -- Requires maintaining per-platfrom packages; unclear who could provide and maintain these. +- Requires maintaining per-platform packages; unclear who could provide and maintain these. - Quint is already available from npm. #### 3.2.2 Using an ecosystem package manager (npm, coursier, ...) @@ -227,7 +227,7 @@ Cons: - Assumes that the JRE is installed on the local system. *Note: We did a prototype implementation querying the GitHub REST API in [#1115](https://github.com/informalsystems/quint/issues/1115). -However, we observed CI issues due to the Github API's rate limiting as described in [#1124](https://github.com/informalsystems/quint/issues/1124). In pratice, the same issues can affect users (e.g., behind a shared IP) and may segnificantly impact UX of the `verify` command. As a countermeasure, we reverted to a hardcoded Apalache version in [`4ceb7d8`](https://github.com/informalsystems/quint/commit/4ceb7d8be824ddc0a2c2a14e105baff446f71e72).* +However, we observed CI issues due to the Github API's rate limiting as described in [#1124](https://github.com/informalsystems/quint/issues/1124). In practice, the same issues can affect users (e.g., behind a shared IP) and may segnificantly impact UX of the `verify` command. As a countermeasure, we reverted to a hardcoded Apalache version in [`4ceb7d8`](https://github.com/informalsystems/quint/commit/4ceb7d8be824ddc0a2c2a14e105baff446f71e72).* #### 3.2.5 Apalache as cloud-hosted SaaS @@ -237,7 +237,7 @@ is necessary. Pros: - No installation or server management issues. -- Versioning and backwards-compatiblity could be exposed via separate endpoints. +- Versioning and backwards-compatibility could be exposed via separate endpoints. Cons: @@ -248,7 +248,7 @@ Cons: ### 3.3 Version dependencies between Quint and Apalache -We want to maintain compatiblity between Quint and Apalache, therefore we need +We want to maintain compatibility between Quint and Apalache, therefore we need some mode of linking compatible versions of both tools. Both tools follow [semantic versioning][]. From 7e3bad01cb5cb71e9490390bccfa59e7897c3398 Mon Sep 17 00:00:00 2001 From: oliveredget <188809800+oliveredget@users.noreply.github.com> Date: Sat, 28 Dec 2024 11:59:11 +0800 Subject: [PATCH 08/11] Fix typo --- docs/pages/docs/getting-started.mdx | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/docs/pages/docs/getting-started.mdx b/docs/pages/docs/getting-started.mdx index 712da90c9..40c8ba5ad 100644 --- a/docs/pages/docs/getting-started.mdx +++ b/docs/pages/docs/getting-started.mdx @@ -16,7 +16,7 @@ npm i @informalsystems/quint -g ### Setup your code editor -For the best experience writting Quint, you should set up your code editor with the Quint tools. The VSCode setup is, by far, the easiest, so you might want to use it if you want a quick start. +For the best experience writing Quint, you should set up your code editor with the Quint tools. The VSCode setup is, by far, the easiest, so you might want to use it if you want a quick start. From ab5a8ce6299711f0adae949543171d8ad7dcb797 Mon Sep 17 00:00:00 2001 From: oliveredget <188809800+oliveredget@users.noreply.github.com> Date: Sat, 28 Dec 2024 11:59:11 +0800 Subject: [PATCH 09/11] Fix typo --- docs/pages/docs/lessons/coin.md | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/docs/pages/docs/lessons/coin.md b/docs/pages/docs/lessons/coin.md index 1390b225b..d4f38b4f4 100644 --- a/docs/pages/docs/lessons/coin.md +++ b/docs/pages/docs/lessons/coin.md @@ -130,7 +130,7 @@ different kinds of "integers", when they are referred to via different type alia -It often happens that a protocol requires auxilliary definitions that do not +It often happens that a protocol requires auxiliary definitions that do not depend on the protocol state, but only on the values of their parameters. Such computations are often called "pure". In the above code, we define two pure definitions: From b31af47515f9ddd9f92aabeee3342fb7202bed15 Mon Sep 17 00:00:00 2001 From: oliveredget <188809800+oliveredget@users.noreply.github.com> Date: Sat, 28 Dec 2024 11:59:11 +0800 Subject: [PATCH 10/11] Fix typo --- docs/pages/docs/lessons/hello.md | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/docs/pages/docs/lessons/hello.md b/docs/pages/docs/lessons/hello.md index b1b6ec190..3aac84a88 100644 --- a/docs/pages/docs/lessons/hello.md +++ b/docs/pages/docs/lessons/hello.md @@ -182,7 +182,7 @@ Finally, the third statement may look useless to you too: Why shall we say that `readByUser` keeps its value in the next state? Most likely, we will be able to automatically infer this in the future. In the current version of Quint, if an action is used to execute transitions, -it has to explicitely assign values to all of the state variables. +it has to explicitly assign values to all of the state variables. ## 7. Introduce an action by the user From 94a88e5a1c87a406cb37cfbdc3cda8cbe1edfe66 Mon Sep 17 00:00:00 2001 From: oliveredget <188809800+oliveredget@users.noreply.github.com> Date: Sat, 28 Dec 2024 11:59:11 +0800 Subject: [PATCH 11/11] Fix typo --- docs/theme.config.jsx | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/docs/theme.config.jsx b/docs/theme.config.jsx index 2a3975074..be2bc4924 100644 --- a/docs/theme.config.jsx +++ b/docs/theme.config.jsx @@ -39,11 +39,11 @@ export default {