Merge pull request #1490 from informalsystems/romac/progress

Add progress bar to `quint test` and `quint run`

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
 

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",

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

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,15 +158,14 @@ 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), [])
           }
 
           const bestTrace = recorder.bestTraces[0].frame
           // 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',