Output the execution stack on undefined values in REPL

CHANGELOG.md

@@ -8,6 +8,9 @@ and this project adheres to [Semantic Versioning](https://semver.org/spec/v2.0.0
 ## UNRELEASED
 
 ### Added
+
+- `quint repl` produces an evaluation trace on errors too (#1056)
+
 ### Changed
 
 - `quint run` produces a friendlier message when it meets a `const` (#1050)

quint/io-cli-tests.md

@@ -279,6 +279,7 @@ exit $exit_code
 
 
   Use --verbosity=3 to show executions.
+      HOME/failingTestCounters.qnt
 ```
 
 ### test counters produces no execution

quint/src/cliCommands.ts

@@ -421,7 +421,8 @@ export async function runTests(prev: TypecheckedStage): Promise<CLIProcedure<Tes
     }
 
     if (failed.length > 0 && verbosity.hasHints(options.verbosity) && !verbosity.hasActionTracking(options.verbosity)) {
-      out(chalk.gray('\n  Use --verbosity=3 to show executions.'))
+      out(chalk.gray(`\n  Use --verbosity=3 to show executions.`))
+      out(chalk.gray(`  Further debug with: quint --verbosity=3 ${prev.args.input}`))
     }
   }
 

quint/src/repl.ts

@@ -699,7 +699,7 @@ function countBraces(str: string): [number, number, number] {
 function evalExpr(state: ReplState, out: writer): Either<string, QuintEx> {
   const computable = contextNameLookup(state.evaluationState.context, 'q::input', 'callable')
   const columns = terminalWidth()
-  return computable
+  const result = computable
     .mapRight(comp => {
       return comp
         .eval()
@@ -708,18 +708,6 @@ function evalExpr(state: ReplState, out: writer): Either<string, QuintEx> {
           out(format(columns, 0, prettyQuintEx(ex)))
           out('\n')
 
-          if (verbosity.hasUserOpTracking(state.verbosity)) {
-            const trace = state.recorder.getBestTrace()
-            if (trace.subframes.length > 0) {
-              out('\n')
-              trace.subframes.forEach((f, i) => {
-                out(`[Frame ${i}]\n`)
-                printExecutionFrameRec({ width: columns, out }, f, [])
-                out('\n')
-              })
-            }
-          }
-
           if (ex.kind === 'bool' && ex.value) {
             // A Boolean expression may be an action or a run.
             // Save the state, if there were any updates to variables.
@@ -735,6 +723,20 @@ function evalExpr(state: ReplState, out: writer): Either<string, QuintEx> {
         .unwrap()
     })
     .join()
+
+  if (verbosity.hasUserOpTracking(state.verbosity)) {
+    const trace = state.recorder.getBestTrace()
+    if (trace.subframes.length > 0) {
+      out('\n')
+      trace.subframes.forEach((f, i) => {
+        out(`[Frame ${i}]\n`)
+        printExecutionFrameRec({ width: columns, out }, f, [])
+        out('\n')
+      })
+    }
+  }
+
+  return result
 }
 
 function getMainModuleAnnotation(moduleHist: string): string | undefined {

quint/test/repl.test.ts

@@ -249,6 +249,34 @@ describe('repl ok', () => {
     await assertRepl(input, output)
   })
 
+  it('change verbosity and show execution on failure', async () => {
+    const input = dedent(
+      `pure def div(x, y) = x / y
+      |.verbosity=4
+      |div(2, 0)
+      |`
+    )
+    const output = dedent(
+      `>>> pure def div(x, y) = x / y
+      |
+      |>>> .verbosity=4
+      |.verbosity=4
+      |>>> div(2, 0)
+      |
+      |[Frame 0]
+      |q::input() => none
+      |└─ div(2, 0) => none
+      |
+      |runtime error: error: Division by zero
+      |div(2, 0)
+      |                     ^^^^^
+      |
+      |<undefined value>
+      |>>> `
+    )
+    await assertRepl(input, output)
+  })
+
   it('caching nullary definitions', async () => {
     const input = dedent(
       `var x: int