From 90348e663779493d4585c37d620ace4a4a753d40 Mon Sep 17 00:00:00 2001 From: vuittont60 <81072379+vuittont60@users.noreply.github.com> Date: Wed, 1 Nov 2023 15:15:30 +0800 Subject: [PATCH] Fix typos --- doc/adr001-transpiler-architecture.md | 2 +- doc/adr007-flattening.md | 4 ++-- doc/design-principles.md | 4 ++-- doc/quint.md | 4 ++-- doc/rfcs/rfc001-sum-types/rfc001-erc-sum-types-example.qnt | 2 +- quint/src/cli.ts | 4 ++-- quint/src/cliCommands.ts | 4 ++-- 7 files changed, 12 insertions(+), 12 deletions(-) diff --git a/doc/adr001-transpiler-architecture.md b/doc/adr001-transpiler-architecture.md index efd68745f..e491d1cff 100644 --- a/doc/adr001-transpiler-architecture.md +++ b/doc/adr001-transpiler-architecture.md @@ -8,7 +8,7 @@ This document describes a preliminary architecture of the Quint transpiler. As rule, we are using a data-flow approach to parsing, in contrast to the pipeline approach, which can be found in textbooks. Our main assumption is that external contributors should be able to plug-in their code/passes to our pipeline. -Hence, we have to be very careful when definining our assumptions about the +Hence, we have to be very careful when defining our assumptions about the input and output of every pass. The use cases of this architecture are as follows: diff --git a/doc/adr007-flattening.md b/doc/adr007-flattening.md index df568800a..19f5bb594 100644 --- a/doc/adr007-flattening.md +++ b/doc/adr007-flattening.md @@ -6,7 +6,7 @@ ## 1. Summary -This document describes a new strategy for flattening modules, that is, replacing imports, instances and exports with the actual definitions. This is a necessary step for compilation and integration with apalache, since both the compiler and apalache cannnot handle imports, instances and exports. +This document describes a new strategy for flattening modules, that is, replacing imports, instances and exports with the actual definitions. This is a necessary step for compilation and integration with apalache, since both the compiler and apalache cannot handle imports, instances and exports. ## 2. Context @@ -15,7 +15,7 @@ Our current strategy for flattening has intrinsic problems, and some issues that The existing flattener takes import/instance/export statements and replaces them with a copy of the definitions from that module, assigning new ids to those definitions and its inner IR components and adding namespaces when necessary. With this, there are two possible scenarios: 1. All imports, instances and exports include all definitions (i.e. there is no `import A.foo`). In this case, we will end up with a module with all of the definitions from all used modules. -2. There is some statement refering to a specific definition like `import A.foo`. In this case, the other definitions from `A` won't be copied, and if `foo` depends on something else, the flattened module won't be valid. +2. There is some statement referring to a specific definition like `import A.foo`. In this case, the other definitions from `A` won't be copied, and if `foo` depends on something else, the flattened module won't be valid. Therefore, it is clear that we need some way of looking into the dependencies of definitions when copying them over, both to avoid (1) by copying only the necessary definitions, and to avoid (2) and ensure the flattened module has all the definitions it needs. diff --git a/doc/design-principles.md b/doc/design-principles.md index 5cc87c077..518b1997e 100644 --- a/doc/design-principles.md +++ b/doc/design-principles.md @@ -57,5 +57,5 @@ - *Quint is CLI-first*: - The users should be able to parse and transpile Quint in the command-line. - - The intermediate transpiler outputs are avaiable in JSON. - - IDE support (such as a VSCode plugin) is a beatiful opt-in, not a requirement. + - The intermediate transpiler outputs are available in JSON. + - IDE support (such as a VSCode plugin) is a beautiful opt-in, not a requirement. diff --git a/doc/quint.md b/doc/quint.md index 393c0e905..598a50d47 100644 --- a/doc/quint.md +++ b/doc/quint.md @@ -174,7 +174,7 @@ Options: [string] --out output file (suppresses all console output) [string] --out-itf output the trace in the Informal Trace Format to file - (supresses all console output) [string] + (suppresses all console output) [string] --max-samples the maximum on the number of traces to try [number] [default: 10000] --max-steps the maximum on the number of steps in every trace @@ -269,7 +269,7 @@ Options: filename) [string] --out output file (suppresses all console output) [string] --out-itf output the trace in the Informal Trace Format to file - (supresses all console output) [string] + (suppresses all console output) [string] --max-steps the maximum number of steps in every trace [number] [default: 10] --init name of the initializer action [string] [default: "init"] diff --git a/doc/rfcs/rfc001-sum-types/rfc001-erc-sum-types-example.qnt b/doc/rfcs/rfc001-sum-types/rfc001-erc-sum-types-example.qnt index 27ae76fa1..f811bb88e 100644 --- a/doc/rfcs/rfc001-sum-types/rfc001-erc-sum-types-example.qnt +++ b/doc/rfcs/rfc001-sum-types/rfc001-erc-sum-types-example.qnt @@ -50,7 +50,7 @@ module erc20 { | Error(_) => r } - // An auxilliary definition similar to Solidity's require + // An auxiliary definition similar to Solidity's require pure def require(r: Erc20Result, cond: bool, msg: str): Erc20Result = match r { | Error(_) => r diff --git a/quint/src/cli.ts b/quint/src/cli.ts index 80049b4fe..21df3eb7d 100755 --- a/quint/src/cli.ts +++ b/quint/src/cli.ts @@ -149,7 +149,7 @@ const runCmd = { type: 'string', }) .option('out-itf', { - desc: 'output the trace in the Informal Trace Format to file (supresses all console output)', + desc: 'output the trace in the Informal Trace Format to file (suppresses all console output)', type: 'string', }) .option('max-samples', { @@ -212,7 +212,7 @@ const verifyCmd = { type: 'string', }) .option('out-itf', { - desc: 'output the trace in the Informal Trace Format to file (supresses all console output)', + desc: 'output the trace in the Informal Trace Format to file (suppresses all console output)', type: 'string', }) .option('max-steps', { diff --git a/quint/src/cliCommands.ts b/quint/src/cliCommands.ts index 8233702e5..a069d7292 100644 --- a/quint/src/cliCommands.ts +++ b/quint/src/cliCommands.ts @@ -67,7 +67,7 @@ interface OutputStage { // Test names output produced by 'run' status?: 'ok' | 'violation' | 'failure' trace?: QuintEx[] - /* Docstrings by defintion name by module name */ + /* Docstrings by definition name by module name */ documentation?: Map> errors?: ErrorMessage[] warnings?: any[] // TODO it doesn't look like this is being used for anything. Should we remove it? @@ -639,7 +639,7 @@ export async function verifySpec(prev: TypecheckedStage): Promise