From cee63da181b30463e2b6dcd815e0788a1b35c611 Mon Sep 17 00:00:00 2001 From: Shon Feder Date: Mon, 21 Nov 2022 14:28:49 -0500 Subject: [PATCH 1/5] Fix link in readme Relative link will work on github but also for navigating around locally. --- CONTRIBUTING.md | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/CONTRIBUTING.md b/CONTRIBUTING.md index 45456b4c5..35c602265 100644 --- a/CONTRIBUTING.md +++ b/CONTRIBUTING.md @@ -123,7 +123,7 @@ true [Installing the VSCode plugin]: https://github.com/informalsystems/tnt/blob/main/vscode/tnt/README.md#temp-how-to-run-it-locally [Language server protocol]: https://microsoft.github.io/language-server-protocol/ [tntc unit tests]: https://github.com/informalsystems/tnt/blob/main/tntc/README.md#unit-tests -[tntc integration tests]: https://github.com/informalsystems/tnt/blob/main/tntc/README.md#integration-tests +[tntc integration tests]: ./tntc/README.md#integration-tests [Mocha]: https://mochajs.org/ [Chai]: https://www.chaijs.com/ [txm]: https://www.npmjs.com/package/txm From f0ccb72333f772578e447b7c9fb5b720ddfc15bd Mon Sep 17 00:00:00 2001 From: Shon Feder Date: Mon, 21 Nov 2022 14:29:15 -0500 Subject: [PATCH 2/5] Add error handling for file loading Closes #215 This is introduced in a way to suggest turning to sweet-monads/either for sequencing our error-prone computations. The sequencing and composition of our top-level routines exposed by CLI is currently done via imperative early exits. This makes it hard to reason about the code in general, but also breaks our ability to compose these routines. Looking towards #345, we'll need typecheck to receive the output of parse, then add it's typing information, before finally printing to the `--out` location. This requires composing the routines while handling possible error states, and just bailing with exit codes won't work for that. Since we are already using `Either`, and since it is designed for facilitating the composition of error-prone code, I think we can massage these routines into shape with a few well-placed Either's. ;) --- tntc/src/cli.ts | 31 +++++++++++++++++++++++++------ 1 file changed, 25 insertions(+), 6 deletions(-) diff --git a/tntc/src/cli.ts b/tntc/src/cli.ts index 1c67b926c..579518e19 100755 --- a/tntc/src/cli.ts +++ b/tntc/src/cli.ts @@ -9,7 +9,7 @@ * @author Igor Konnov, Gabriela Moreira, Informal Systems, 2021-2022 */ -import { readFileSync, writeFileSync } from 'fs' +import { existsSync, PathLike, readFileSync, writeFileSync } from 'fs' import { resolve } from 'path' import { cwd } from 'process' import { lf } from 'eol' @@ -29,6 +29,7 @@ import { tntRepl } from './repl' import { inferTypes } from './types/inferrer' import { effectToString } from './effects/printing' import { typeSchemeToString } from './types/printing' +import { Either, right, left } from '@sweet-monads/either' /** * Parse a TNT specification. @@ -103,10 +104,28 @@ function runRepl(_argv: any) { tntRepl(process.stdin, process.stdout) } +// Load a file into a string +function loadFile(p: PathLike): Either { + if (existsSync(p)) { + try { + return right(readFileSync(p, 'utf8')) + } catch (err: unknown) { + return left(`error: file ${p} could not be opened due to ${err}`) + } + } else { + return left(`error: file ${p} does not exist`) + } +} + // read either the standard input or an input file function parseModule(argv: any): [Phase1Result, LookupTableByModule, string] { - const data = readFileSync(argv.input, 'utf8') - return parseText(argv, lf(data)) + const res = loadFile(argv.input) + if (res.isRight()) { + return parseText(argv, res.value) + } else { + console.error(res.value) + process.exit(1) + } } // a callback to parse the text that we get from readFile @@ -114,7 +133,7 @@ function parseText(argv: any, text: string): [Phase1Result, LookupTableByModule, const path = resolve(cwd(), argv.input) const phase1Result = parsePhase1(text, path) if (phase1Result.kind === 'error') { - reportError(argv, text, phase1Result) + reportParseError(argv, text, phase1Result) process.exit(1) } @@ -125,7 +144,7 @@ function parseText(argv: any, text: string): [Phase1Result, LookupTableByModule, const phase2Result = parsePhase2(phase1Result.module, phase1Result.sourceMap) if (phase2Result.kind === 'error') { - reportError(argv, text, phase2Result) + reportParseError(argv, text, phase2Result) process.exit(1) } @@ -141,7 +160,7 @@ function parseText(argv: any, text: string): [Phase1Result, LookupTableByModule, return [phase1Result, phase2Result.table, text] } -function reportError(argv: any, sourceCode: string, result: { kind: 'error', messages: ErrorMessage[] }) { +function reportParseError(argv: any, sourceCode: string, result: { kind: 'error', messages: ErrorMessage[] }) { if (argv.out) { // write the errors to the output file writeToJson(argv.out, result) From b9cce5d9ddca6c2fe167369abee696538c852820 Mon Sep 17 00:00:00 2001 From: Shon Feder Date: Mon, 21 Nov 2022 14:33:34 -0500 Subject: [PATCH 3/5] Fix txm invocation `txm` does not support a `--no-color` flag as far as I can tell: indeed, we don't call it with this flag in our CI. --- tntc/package.json | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/tntc/package.json b/tntc/package.json index f77c87a7e..ba281e935 100644 --- a/tntc/package.json +++ b/tntc/package.json @@ -64,7 +64,7 @@ "compile": "tsc", "test": "mocha -r ts-node/register test/*.test.ts test/**/*.test.ts", "coverage": "nyc npm run test", - "integration": "txm --no-color cli-tests.md", + "integration": "txm cli-tests.md", "antlr": "antlr4ts -visitor ./src/generated/Tnt.g4 && antlr4ts -visitor ./src/generated/Effect.g4", "format": "eslint --fix '**/*.ts'" }, From 2047dba8597b0c511474537aea037d31f7984d77 Mon Sep 17 00:00:00 2001 From: Shon Feder Date: Mon, 21 Nov 2022 14:34:16 -0500 Subject: [PATCH 4/5] Add regression test for #215 --- tntc/cli-tests.md | 7 ++++++- tntc/io-cli-tests.md | 30 ++++++++++++++++++++++++++++++ tntc/package.json | 2 +- tntc/runner.sh | 33 +++++++++++++++++++++++++++++++++ 4 files changed, 70 insertions(+), 2 deletions(-) create mode 100644 tntc/io-cli-tests.md create mode 100755 tntc/runner.sh diff --git a/tntc/cli-tests.md b/tntc/cli-tests.md index 86582552f..83edaff64 100644 --- a/tntc/cli-tests.md +++ b/tntc/cli-tests.md @@ -7,6 +7,11 @@ installed: npm install -g txm ``` +*NOTE*: these tests only check that particular invocations succeed or fail. For +tests that examine particular output, use +[./io-cli-tests.md](./io-cli-tests.md). + + ### OK on parse Paxos This command parses the Paxos example. @@ -352,4 +357,4 @@ tntc typecheck ../examples/tuples.tnt ``` - expect exit code 0 \ No newline at end of file + expect exit code 0 diff --git a/tntc/io-cli-tests.md b/tntc/io-cli-tests.md new file mode 100644 index 000000000..64123a330 --- /dev/null +++ b/tntc/io-cli-tests.md @@ -0,0 +1,30 @@ +This is a suite of blackbox integration tests for the `tntc` executable. +The tests in this file check that particular output is produced when +particular input is received. + +These tests require [`txm`](https://www.npmjs.com/package/txm) to be installed: + +```sh +npm install -g txm +``` + +All of the test inputs in the following test cases are commands executed by `bash`. + + + +### User error on parse with non-existent file + +Regression test for [#215](https://github.com/informalsystems/tnt/issues/215). +We want to ensure we do not throw uncaught exceptions when the input file is +doesn't exist. + + + tntc parse ../examples/non-existent.file + + + + error: file ../examples/non-existent.file does not exist + + diff --git a/tntc/package.json b/tntc/package.json index ba281e935..300c80d48 100644 --- a/tntc/package.json +++ b/tntc/package.json @@ -64,7 +64,7 @@ "compile": "tsc", "test": "mocha -r ts-node/register test/*.test.ts test/**/*.test.ts", "coverage": "nyc npm run test", - "integration": "txm cli-tests.md", + "integration": "txm cli-tests.md && txm io-cli-tests.md", "antlr": "antlr4ts -visitor ./src/generated/Tnt.g4 && antlr4ts -visitor ./src/generated/Effect.g4", "format": "eslint --fix '**/*.ts'" }, diff --git a/tntc/runner.sh b/tntc/runner.sh new file mode 100755 index 000000000..ecf6890d6 --- /dev/null +++ b/tntc/runner.sh @@ -0,0 +1,33 @@ +#!/usr/bin/env bash + +# This runner script just reads each line from stdin and executes it, stripping off any +# trailing `\r` to normalize output on windows. +# +# The runner script ensures that the "program" run by txm is consistent between OSs: +# I.e. that it is always run with bash +# +# We use it in ./cli-tests.md to run our black box CLI commands. + +set -euo pipefail + +export LANG="C.UTF-8" +export LANGUAGE= +export LC_CTYPE="C.UTF-8" +export LC_NUMERIC="C.UTF-8" +export LC_TIME="C.UTF-8" +export LC_COLLATE="C.UTF-8" +export LC_MONETARY="C.UTF-8" +export LC_MESSAGES="C.UTF-8" +export LC_PAPER="C.UTF-8" +export LC_NAME="C.UTF-8" +export LC_ADDRESS="C.UTF-8" +export LC_TELEPHONE="C.UTF-8" +export LC_MEASUREMENT="C.UTF-8" +export LC_IDENTIFICATION="C.UTF-8" +export LC_ALL= + +while IFS= read -r cmd; do + # All the noise here with FDs is to filter both stdout and stderr + # See https://stackoverflow.com/a/31151808/1187277 + bash -c "$cmd" +done From a0cb9cb57a2fc1b14bbb20fd88bf57172f78336f Mon Sep 17 00:00:00 2001 From: Shon Feder Date: Tue, 22 Nov 2022 17:05:24 -0500 Subject: [PATCH 5/5] Run io-cli-tests.md only on windows --- .github/workflows/main.yml | 17 +++++++++++------ tntc/runner.sh | 33 --------------------------------- 2 files changed, 11 insertions(+), 39 deletions(-) delete mode 100755 tntc/runner.sh diff --git a/.github/workflows/main.yml b/.github/workflows/main.yml index 098f18f0e..dfca2c851 100644 --- a/.github/workflows/main.yml +++ b/.github/workflows/main.yml @@ -10,7 +10,7 @@ on: push: branches: - main - + name: build jobs: @@ -24,7 +24,7 @@ jobs: - uses: actions/checkout@v2 - uses: actions/setup-node@v2 with: - node-version: '17' + node-version: "17" - run: cd ./tntc && npm install - run: cd ./tntc && npm run compile - run: cd ./tntc && npm test @@ -39,11 +39,17 @@ jobs: - uses: actions/checkout@v2 - uses: actions/setup-node@v2 with: - node-version: '17' + node-version: "17" - run: npm install -g txm - run: cd ./tntc && npm install - run: cd ./tntc && npm run compile && npm link - - run: cd ./tntc && txm cli-tests.md + - name: Blackbox integration tests + run: cd ./tntc && txm cli-tests.md + - name: Blackbox integration tests with I/O + # This tests fail on windows currently + # See https://github.com/anko/txm/issues/10 + run: cd ./tntc && txm io-cli-tests.md + if: matrix.operating-system != 'windows-latest' tntc-antlr-grammar: runs-on: ubuntu-latest @@ -51,7 +57,6 @@ jobs: - uses: actions/checkout@v2 - uses: actions/setup-node@v2 with: - node-version: '17' + node-version: "17" - run: cd ./tntc && npm install - run: cd ./tntc && npm run antlr - diff --git a/tntc/runner.sh b/tntc/runner.sh deleted file mode 100755 index ecf6890d6..000000000 --- a/tntc/runner.sh +++ /dev/null @@ -1,33 +0,0 @@ -#!/usr/bin/env bash - -# This runner script just reads each line from stdin and executes it, stripping off any -# trailing `\r` to normalize output on windows. -# -# The runner script ensures that the "program" run by txm is consistent between OSs: -# I.e. that it is always run with bash -# -# We use it in ./cli-tests.md to run our black box CLI commands. - -set -euo pipefail - -export LANG="C.UTF-8" -export LANGUAGE= -export LC_CTYPE="C.UTF-8" -export LC_NUMERIC="C.UTF-8" -export LC_TIME="C.UTF-8" -export LC_COLLATE="C.UTF-8" -export LC_MONETARY="C.UTF-8" -export LC_MESSAGES="C.UTF-8" -export LC_PAPER="C.UTF-8" -export LC_NAME="C.UTF-8" -export LC_ADDRESS="C.UTF-8" -export LC_TELEPHONE="C.UTF-8" -export LC_MEASUREMENT="C.UTF-8" -export LC_IDENTIFICATION="C.UTF-8" -export LC_ALL= - -while IFS= read -r cmd; do - # All the noise here with FDs is to filter both stdout and stderr - # See https://stackoverflow.com/a/31151808/1187277 - bash -c "$cmd" -done