From 26ed2f9e6da3f3d0ed73a37a2aada44ef10f4138 Mon Sep 17 00:00:00 2001 From: Romain Ruetschi Date: Fri, 30 Aug 2024 16:35:12 +0200 Subject: [PATCH 1/4] Add progress bar to `quint test` --- quint/package-lock.json | 24 ++++++++++++++++++++++++ quint/package.json | 6 ++++-- quint/src/runtime/testing.ts | 21 +++++++++++++++++++-- 3 files changed, 47 insertions(+), 4 deletions(-) diff --git a/quint/package-lock.json b/quint/package-lock.json index 36380b5c1..6b974e15c 100644 --- a/quint/package-lock.json +++ b/quint/package-lock.json @@ -19,6 +19,7 @@ "@types/seedrandom": "^3.0.4", "antlr4ts": "^0.5.0-alpha.4", "chalk": "^4.1.2", + "cli-progress": "^3.12.0", "eol": "^0.9.1", "immutable": "^4.3.0", "json-bigint": "^1.0.0", @@ -35,6 +36,7 @@ }, "devDependencies": { "@types/chai": "^4.2.18", + "@types/cli-progress": "^3.11.6", "@types/json-bigint": "^1.0.1", "@types/lodash.isequal": "^4.5.6", "@types/mocha": "^8.2.3", @@ -1049,6 +1051,16 @@ "integrity": "sha512-zNKDHG/1yxm8Il6uCCVsm+dRdEsJlFoDu73X17y09bId6UwoYww+vFBsAcRzl8knM1sab3Dp1VRikFQwDOtDDw==", "dev": true }, + "node_modules/@types/cli-progress": { + "version": "3.11.6", + "resolved": "https://registry.npmjs.org/@types/cli-progress/-/cli-progress-3.11.6.tgz", + "integrity": "sha512-cE3+jb9WRlu+uOSAugewNpITJDt1VF8dHOopPO4IABFc3SXYL5WE/+PTz/FCdZRRfIujiWW3n3aMbv1eIGVRWA==", + "dev": true, + "license": "MIT", + "dependencies": { + "@types/node": "*" + } + }, "node_modules/@types/debug": { "version": "4.1.12", "resolved": "https://registry.npmjs.org/@types/debug/-/debug-4.1.12.tgz", @@ -2083,6 +2095,18 @@ "node": ">=8" } }, + "node_modules/cli-progress": { + "version": "3.12.0", + "resolved": "https://registry.npmjs.org/cli-progress/-/cli-progress-3.12.0.tgz", + "integrity": "sha512-tRkV3HJ1ASwm19THiiLIXLO7Im7wlTuKnvkYaTkyoAPefqjNg7W7DHKUlGRxy9vxDvbyCYQkQozvptuMkGCg8A==", + "license": "MIT", + "dependencies": { + "string-width": "^4.2.3" + }, + "engines": { + "node": ">=4" + } + }, "node_modules/cli-width": { "version": "3.0.0", "resolved": "https://registry.npmjs.org/cli-width/-/cli-width-3.0.0.tgz", diff --git a/quint/package.json b/quint/package.json index 6557c08c9..a7a539e43 100644 --- a/quint/package.json +++ b/quint/package.json @@ -54,17 +54,18 @@ "@sweet-monads/either": "~3.2.0", "@sweet-monads/maybe": "~3.2.0", "@types/line-column": "^1.0.0", + "@types/lodash.clonedeep": "4.5.0", "@types/seedrandom": "^3.0.4", "antlr4ts": "^0.5.0-alpha.4", "chalk": "^4.1.2", + "cli-progress": "^3.12.0", "eol": "^0.9.1", "immutable": "^4.3.0", "json-bigint": "^1.0.0", "line-column": "^1.0.2", "lodash": "^4.17.21", - "lodash.isequal": "^4.5.0", "lodash.clonedeep": "4.5.0", - "@types/lodash.clonedeep": "4.5.0", + "lodash.isequal": "^4.5.0", "seedrandom": "^3.0.5", "tar": "^6.1.14", "yargs": "^17.2.1" @@ -89,6 +90,7 @@ }, "devDependencies": { "@types/chai": "^4.2.18", + "@types/cli-progress": "^3.11.6", "@types/json-bigint": "^1.0.1", "@types/lodash.isequal": "^4.5.6", "@types/mocha": "^8.2.3", diff --git a/quint/src/runtime/testing.ts b/quint/src/runtime/testing.ts index 25cf87ea9..99ddc86c6 100644 --- a/quint/src/runtime/testing.ts +++ b/quint/src/runtime/testing.ts @@ -9,6 +9,7 @@ */ import { Either, left, mergeInMany, right } from '@sweet-monads/either' +import { Presets, SingleBar } from 'cli-progress' import { QuintEx, QuintOpDef } from '../ir/quintIr' @@ -128,9 +129,22 @@ export function compileAndTest( // save the initial seed let seed = options.rng.getState() + const bar = new SingleBar( + { + clearOnComplete: true, + forceRedraw: true, + format: ' {test} [{bar}] {percentage}% | ETA: {eta}s | {value}/{total} samples', + }, + Presets.rect + ) + + bar.start(options.maxSamples, 0, { test: name }) + let nsamples = 1 // run up to maxSamples, stop on the first failure for (; nsamples <= options.maxSamples; nsamples++) { + bar.update(nsamples, { test: name }) + // record the seed value seed = options.rng.getState() recorder.onRunCall() @@ -144,8 +158,6 @@ export function compileAndTest( if (trace.length > 0) { recorder.onRunReturn(toMaybe(result), trace) } else { - // Report a non-critical error - console.error('Missing a trace') recorder.onRunReturn(toMaybe(result), []) } @@ -153,6 +165,7 @@ export function compileAndTest( // evaluate the result if (result.isLeft()) { // if the test failed, return immediately + bar.stop() return { name, status: 'failed', @@ -166,6 +179,7 @@ export function compileAndTest( const ex = result.value.toQuintEx(zerog) if (ex.kind !== 'bool') { // if the test returned a malformed result, return immediately + bar.stop() return { name, status: 'ignored', @@ -184,6 +198,7 @@ export function compileAndTest( reference: def.id, } saveTrace(bestTrace, index, name, 'failed') + bar.stop() return { name, status: 'failed', @@ -197,6 +212,7 @@ export function compileAndTest( // This successful test did not use non-determinism. // Running it one time is sufficient. saveTrace(bestTrace, index, name, 'passed') + bar.stop() return { name, status: 'passed', @@ -212,6 +228,7 @@ export function compileAndTest( // the test was run maxSamples times, and no errors were found const bestTrace = recorder.bestTraces[0].frame saveTrace(bestTrace, index, name, 'passed') + bar.stop() return { name, status: 'passed', From 4a2f82114961e1223243e809d5e13647a96ecb5f Mon Sep 17 00:00:00 2001 From: Romain Ruetschi Date: Fri, 30 Aug 2024 17:02:06 +0200 Subject: [PATCH 2/4] Add progress bar to `quint run` --- examples/language-features/counters.qnt | 16 +++++++++++++++- quint/src/runtime/impl/compilerImpl.ts | 17 +++++++++++++++++ 2 files changed, 32 insertions(+), 1 deletion(-) diff --git a/examples/language-features/counters.qnt b/examples/language-features/counters.qnt index a316a9e05..202e4aa2a 100644 --- a/examples/language-features/counters.qnt +++ b/examples/language-features/counters.qnt @@ -70,13 +70,27 @@ module counters { } // this test should not fail - run passingTest = { + run passing1Test = { init.then(10.reps(_ => all { assert(n > 0), step, })) } + run passing2Test = { + init.then(5.reps(_ => all { + assert(n > 0), + step, + })) + } + + run passing3Test = { + init.then(15.reps(_ => all { + assert(n > 0), + step, + })) + } + // this tests for a failing condition run failingTest = { init diff --git a/quint/src/runtime/impl/compilerImpl.ts b/quint/src/runtime/impl/compilerImpl.ts index e825ed166..7c7f6cee3 100644 --- a/quint/src/runtime/impl/compilerImpl.ts +++ b/quint/src/runtime/impl/compilerImpl.ts @@ -12,6 +12,7 @@ import { strict as assert } from 'assert' import { Maybe, just, none } from '@sweet-monads/maybe' import { OrderedMap, Set } from 'immutable' +import { Presets, SingleBar } from 'cli-progress' import { LookupTable } from '../../names/base' import { IRVisitor } from '../../ir/IRVisitor' @@ -1479,7 +1480,21 @@ export class CompilerVisitor implements IRVisitor { // do multiple runs, stop at the first failing run const nruns = (nrunsRes as RuntimeValue).toInt() const ntraces = (nTracesRes as RuntimeValue).toInt() + + const bar = new SingleBar( + { + clearOnComplete: true, + forceRedraw: true, + format: 'Running... [{bar}] {percentage}% | ETA: {eta}s | {value}/{total} samples', + }, + Presets.rect + ) + + bar.start(Number(nruns), 0) + for (let runNo = 0; errorsFound < ntraces && !failure && runNo < nruns; runNo++) { + bar.update(runNo) + this.execListener.onRunCall() this.trace.reset() // check Init() @@ -1540,6 +1555,8 @@ export class CompilerVisitor implements IRVisitor { this.recoverNextVars(nextVars) } // end of a single random run + bar.stop() + // finally, return true, if no error was found return !failure ? right(rv.mkBool(errorsFound == 0)) : left({ code: 'QNT501', message: 'Simulation failure' }) }) From fac77a44fe45321311318559014a463144af4de0 Mon Sep 17 00:00:00 2001 From: Romain Ruetschi Date: Fri, 30 Aug 2024 17:07:00 +0200 Subject: [PATCH 3/4] Revert modifications to counters example --- examples/language-features/counters.qnt | 16 +--------------- 1 file changed, 1 insertion(+), 15 deletions(-) diff --git a/examples/language-features/counters.qnt b/examples/language-features/counters.qnt index 202e4aa2a..a316a9e05 100644 --- a/examples/language-features/counters.qnt +++ b/examples/language-features/counters.qnt @@ -70,27 +70,13 @@ module counters { } // this test should not fail - run passing1Test = { + run passingTest = { init.then(10.reps(_ => all { assert(n > 0), step, })) } - run passing2Test = { - init.then(5.reps(_ => all { - assert(n > 0), - step, - })) - } - - run passing3Test = { - init.then(15.reps(_ => all { - assert(n > 0), - step, - })) - } - // this tests for a failing condition run failingTest = { init From 4aebc547f12619000417227edc68f4642bb4e17c Mon Sep 17 00:00:00 2001 From: Romain Ruetschi Date: Fri, 30 Aug 2024 17:23:27 +0200 Subject: [PATCH 4/4] Add changelog entry --- CHANGELOG.md | 1 + 1 file changed, 1 insertion(+) diff --git a/CHANGELOG.md b/CHANGELOG.md index 32df82b74..134add92c 100644 --- a/CHANGELOG.md +++ b/CHANGELOG.md @@ -10,6 +10,7 @@ and this project adheres to [Semantic Versioning](https://semver.org/spec/v2.0.0 ### Added - In the `verify` command, add warning if `--out-itf` option contains `{test}` or `{seq}` as those have no effect since Apalache only produces a single trace (#1485) +- The `run` and `test` commands now display a progress bar (#1457) ### Changed