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 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/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' }) }) 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',