From 62a7b8fca38f949d440d8accca0edb0c59b314a5 Mon Sep 17 00:00:00 2001 From: Thomas Pani Date: Wed, 20 Sep 2023 10:26:15 +0200 Subject: [PATCH] Log Apalache distribution-related `verify` messages only at --verbosity >=4 (#1169) * Log Apalache distribution-related `verify` messages only at --verbosity >=4 * Update integration test * Update debug message --- quint/apalache-dist-tests.md | 9 +-------- quint/src/cliCommands.ts | 4 ++-- quint/src/quintVerifier.ts | 36 +++++++++++++++++++++++++----------- quint/src/verbosity.ts | 7 +++++++ 4 files changed, 35 insertions(+), 21 deletions(-) diff --git a/quint/apalache-dist-tests.md b/quint/apalache-dist-tests.md index 82af2ac96..c4a0a9294 100644 --- a/quint/apalache-dist-tests.md +++ b/quint/apalache-dist-tests.md @@ -31,18 +31,11 @@ quint verify ../examples/language-features/booleans.qnt | \ ``` -Couldn't connect to Apalache, checking for latest supported release -Downloading Apalache distribution from (asseturl) -Launching Apalache server +Downloading Apalache distribution... done. [ok] No violation found (duration). You may increase --max-steps. Use --verbosity to produce more (or less) output. -Shutting down Apalache server -Couldn't connect to Apalache, checking for latest supported release -Using existing Apalache distribution in (distdir) -Launching Apalache server [ok] No violation found (duration). You may increase --max-steps. Use --verbosity to produce more (or less) output. -Shutting down Apalache server ``` diff --git a/quint/src/cliCommands.ts b/quint/src/cliCommands.ts index b6b05f016..7376bbe59 100644 --- a/quint/src/cliCommands.ts +++ b/quint/src/cliCommands.ts @@ -649,8 +649,8 @@ export async function verifySpec(prev: TypecheckedStage): Promise { - const verbosityLevel = !prev.args.out && !prev.args.outItf ? prev.args.verbosity : 0 + const verbosityLevel = !prev.args.out && !prev.args.outItf ? prev.args.verbosity : 0 + return verify(config, verbosityLevel).then(res => { const elapsedMs = Date.now() - startMs return res .map(_ => { diff --git a/quint/src/quintVerifier.ts b/quint/src/quintVerifier.ts index 7756d85e4..85355b355 100644 --- a/quint/src/quintVerifier.ts +++ b/quint/src/quintVerifier.ts @@ -31,6 +31,7 @@ import * as protobufDescriptor from 'protobufjs/ext/descriptor' import { setTimeout } from 'timers/promises' import { promisify } from 'util' import { ItfTrace } from './itf' +import { verbosity } from './verbosity' // TODO: used by GitHub api approach: https://github.com/informalsystems/quint/issues/1124 // import { request as octokitRequest } from '@octokit/request' @@ -273,7 +274,6 @@ async function tryConnect(retry: boolean = false): Promise> { const url = `https://github.com/informalsystems/apalache/releases/download/v${APALACHE_VERSION_TAG}/apalache.tgz` - console.log(`Downloading Apalache distribution from ${url}...`) return fetch(url) .then( // unpack response body @@ -293,15 +293,17 @@ function downloadAndUnpackApalache(): Promise> { * - a `right` equal to the path the Apalache dist was unpacked to, * - a `left` indicating an error. */ -async function fetchApalache(): Promise> { +async function fetchApalache(verbosityLevel: number): Promise> { const apalacheBinary = path.join(apalacheDistDir(), 'apalache', 'bin', 'apalache-mc') if (fs.existsSync(apalacheBinary)) { // Use existing download - console.log(`Using existing Apalache distribution in ${apalacheBinary}`) + debugLog(verbosityLevel, `Using existing Apalache distribution in ${apalacheBinary}`) return right(apalacheBinary) } else { fs.mkdirSync(apalacheDistDir(), { recursive: true }) + process.stdout.write('Downloading Apalache distribution...') const res = await downloadAndUnpackApalache() + process.stdout.write(' done.\n') return res.map(_ => apalacheBinary) } @@ -359,7 +361,7 @@ async function fetchApalache(): Promise> { * - a `right` equal to the path the Apalache dist was unpacked to, * - a `left` indicating an error. */ -async function connect(): Promise> { +async function connect(verbosityLevel: number): Promise> { // Try to connect to Shai, and try to ping it const connectionResult = await tryConnect() // We managed to connect, simply return this connection @@ -368,26 +370,26 @@ async function connect(): Promise> { } // Connection or pinging failed, download Apalache - console.log("Couldn't connect to Apalache, checking for latest supported release") - const exeResult = await fetchApalache() + debugLog(verbosityLevel, 'No running Apalache server found, launching...') + const exeResult = await fetchApalache(verbosityLevel) // Launch Apalache from download return exeResult .asyncChain( async exe => new Promise>((resolve, _) => { - console.log('Launching Apalache server') + debugLog(verbosityLevel, 'Launching Apalache server') const apalache = child_process.spawn(exe, ['server']) // Exit handler that kills Apalache if Quint exists function exitHandler() { - console.log('Shutting down Apalache server') + debugLog(verbosityLevel, 'Shutting down Apalache server') try { process.kill(apalache.pid!) } catch (error: any) { // ESRCH is raised if no process with `pid` exists, i.e., // if Apalache server exited on its own if (error.code == 'ESRCH') { - console.log('Apalache already exited') + debugLog(verbosityLevel, 'Apalache already exited') } else { throw error } @@ -414,6 +416,18 @@ async function connect(): Promise> { .then(chain(() => tryConnect(true))) } +/** + * Log `msg` to the console if `verbosityLevel` implies debug output. + * + * @param verbosityLevel the current verbosity level (set with --verbosity) + * @param msg the message to log + */ +function debugLog(verbosityLevel: number, msg: string) { + if (verbosity.hasDebugInfo(verbosityLevel)) { + console.log(msg) + } +} + /** * Verifies the configuration `config` by model checking it with the Apalache server * @@ -422,7 +436,7 @@ async function connect(): Promise> { * * @returns right(void) if verification succeeds, or left(err) explaining the failure */ -export async function verify(config: any): Promise> { - const connectionResult = await connect() +export async function verify(config: any, verbosityLevel: number): Promise> { + const connectionResult = await connect(verbosityLevel) return connectionResult.asyncChain(conn => conn.check(config)) } diff --git a/quint/src/verbosity.ts b/quint/src/verbosity.ts index 67b24816a..fe30f164c 100644 --- a/quint/src/verbosity.ts +++ b/quint/src/verbosity.ts @@ -76,4 +76,11 @@ export const verbosity = { hasUserOpTracking: (level: number): boolean => { return level >= 3 }, + + /** + * Shall the tool output debug info. + */ + hasDebugInfo: (level: number): boolean => { + return level >= 4 + }, }