diff --git a/CHANGELOG.md b/CHANGELOG.md index c9a32dc73..d9a175aa7 100644 --- a/CHANGELOG.md +++ b/CHANGELOG.md @@ -8,6 +8,9 @@ and this project adheres to [Semantic Versioning](https://semver.org/spec/v2.0.0 ## UNRELEASED ### Added + +- `quint verify` has the option `--apalache-version` to pull a custom version (#1521) + ### Changed ### Deprecated ### Removed diff --git a/quint/apalache-dist-tests.md b/quint/apalache-dist-tests.md index c4ded45fb..8fecfac7d 100644 --- a/quint/apalache-dist-tests.md +++ b/quint/apalache-dist-tests.md @@ -31,7 +31,7 @@ quint verify --verbosity=1 ../examples/language-features/booleans.qnt | \ ``` -Downloading Apalache distribution... done. +Downloading Apalache distribution 0.46.1... done. [ok] No violation found (duration). [ok] No violation found (duration). ``` diff --git a/quint/src/apalache.ts b/quint/src/apalache.ts index 211bc38ae..abb44398c 100644 --- a/quint/src/apalache.ts +++ b/quint/src/apalache.ts @@ -75,7 +75,7 @@ export function serverEndpointToConnectionString(endpoint: ServerEndpoint): stri return `${endpoint.hostname}:${endpoint.port}` } -const APALACHE_VERSION_TAG = '0.46.1' +export const DEFAULT_APALACHE_VERSION_TAG = '0.46.1' // TODO: used by GitHub api approach: https://github.com/informalsystems/quint/issues/1124 // const APALACHE_TGZ = 'apalache.tgz' @@ -83,8 +83,8 @@ function quintConfigDir(): string { return path.join(os.homedir(), '.quint') } -function apalacheDistDir(): string { - return path.join(quintConfigDir(), `apalache-dist-${APALACHE_VERSION_TAG}`) +function apalacheDistDir(apalacheVersion: string): string { + return path.join(quintConfigDir(), `apalache-dist-${apalacheVersion}`) } // The structure used to report errors @@ -335,12 +335,12 @@ async function tryConnect(serverEndpoint: ServerEndpoint, retry: boolean = false .map(apalache) } -function downloadAndUnpackApalache(): Promise> { - const url = `https://github.com/apalache-mc/apalache/releases/download/v${APALACHE_VERSION_TAG}/apalache.tgz` +function downloadAndUnpackApalache(apalacheVersion: string): Promise> { + const url = `https://github.com/apalache-mc/apalache/releases/download/v${apalacheVersion}/apalache.tgz` return fetch(url) .then( // unpack response body - res => pipeline(res.body!, tar.extract({ cwd: apalacheDistDir(), strict: true })), + res => pipeline(res.body!, tar.extract({ cwd: apalacheDistDir(apalacheVersion), strict: true })), error => err(`Error fetching ${url}: ${error}`) ) .then( @@ -356,17 +356,17 @@ function downloadAndUnpackApalache(): Promise> { * - a `right` equal to the path the Apalache dist was unpacked to, * - a `left` indicating an error. */ -async function fetchApalache(verbosityLevel: number): Promise> { +async function fetchApalache(apalacheVersion: string, verbosityLevel: number): Promise> { const filename = process.platform === 'win32' ? 'apalache-mc.bat' : 'apalache-mc' - const apalacheBinary = path.join(apalacheDistDir(), 'apalache', 'bin', filename) + const apalacheBinary = path.join(apalacheDistDir(apalacheVersion), 'apalache', 'bin', filename) if (fs.existsSync(apalacheBinary)) { // Use existing download 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() + fs.mkdirSync(apalacheDistDir(apalacheVersion), { recursive: true }) + process.stdout.write(`Downloading Apalache distribution ${apalacheVersion}...`) + const res = await downloadAndUnpackApalache(apalacheVersion) process.stdout.write(' done.\n') return res.map(_ => apalacheBinary) } @@ -430,6 +430,7 @@ async function fetchApalache(verbosityLevel: number): Promise> { // Try to connect to Shai, and try to ping it @@ -441,7 +442,7 @@ export async function connect( // Connection or pinging failed, download Apalache debugLog(verbosityLevel, 'No running Apalache server found, launching...') - const exeResult = await fetchApalache(verbosityLevel) + const exeResult = await fetchApalache(apalacheVersion, verbosityLevel) // Launch Apalache from download return exeResult .asyncChain( diff --git a/quint/src/cli.ts b/quint/src/cli.ts index af27fe333..0acbcd42f 100755 --- a/quint/src/cli.ts +++ b/quint/src/cli.ts @@ -31,7 +31,7 @@ import { import { verbosity } from './verbosity' import { version } from './version' -import { parseServerEndpoint } from './apalache' +import { DEFAULT_APALACHE_VERSION_TAG, parseServerEndpoint } from './apalache' const defaultOpts = (yargs: any) => yargs.option('out', { @@ -123,6 +123,11 @@ const compileCmd = { type: 'number', default: verbosity.defaultLevel, }) + .option('apalache-version', { + desc: 'The version of Apalache to use, if no running server is found (using this option may result in incompatibility)', + type: 'string', + default: DEFAULT_APALACHE_VERSION_TAG, + }) .option('server-endpoint', { desc: 'Apalache server endpoint hostname:port', type: 'string', @@ -322,6 +327,11 @@ const verifyCmd = { type: 'number', default: verbosity.defaultLevel, }) + .option('apalache-version', { + desc: 'The version of Apalache to use, if no running server is found (using this option may result in incompatibility)', + type: 'string', + default: DEFAULT_APALACHE_VERSION_TAG, + }) .option('server-endpoint', { desc: 'Apalache server endpoint hostname:port', type: 'string', diff --git a/quint/src/cliCommands.ts b/quint/src/cliCommands.ts index b4daaf930..18616cb2a 100644 --- a/quint/src/cliCommands.ts +++ b/quint/src/cliCommands.ts @@ -710,7 +710,12 @@ export async function outputCompilationTarget(compiled: CompiledStage): Promise< process.stdout.write(parsedSpecJson) return right(compiled) case 'tlaplus': { - const toTlaResult = await compileToTlaplus(args.serverEndpoint, parsedSpecJson, verbosityLevel) + const toTlaResult = await compileToTlaplus( + args.serverEndpoint, + args.apalacheVersion, + parsedSpecJson, + verbosityLevel + ) return toTlaResult .mapRight(tla => { process.stdout.write(tla) // Write out, since all went right @@ -791,7 +796,7 @@ export async function verifySpec(prev: CompiledStage): Promise { + return verify(args.serverEndpoint, args.apalacheVersion, config, verbosityLevel).then(res => { const elapsedMs = Date.now() - startMs return res .map(_ => { diff --git a/quint/src/compileToTlaplus.ts b/quint/src/compileToTlaplus.ts index 1ac0e62a1..b4229903e 100644 --- a/quint/src/compileToTlaplus.ts +++ b/quint/src/compileToTlaplus.ts @@ -21,12 +21,16 @@ import { ApalacheResult, ServerEndpoint, connect } from './apalache' * @param serverEndpoint * a server endpoint * + * @param apalacheVersion + * the version of Apalache to use if there is no active server connection + * * @param parseDataJson the flattened, analyzed, parse data, in as a json string * * @returns right(tlaString) if parsing succeeds, or left(err) explaining the failure */ export async function compileToTlaplus( serverEndpoint: ServerEndpoint, + apalacheVersion: string, parseDataJson: string, verbosityLevel: number ): Promise> { @@ -39,6 +43,6 @@ export async function compileToTlaplus( }, }, } - const connectionResult = await connect(serverEndpoint, verbosityLevel) + const connectionResult = await connect(serverEndpoint, apalacheVersion, verbosityLevel) return connectionResult.asyncChain(conn => conn.tla(config)) } diff --git a/quint/src/quintVerifier.ts b/quint/src/quintVerifier.ts index 0ee24f023..11931cacc 100644 --- a/quint/src/quintVerifier.ts +++ b/quint/src/quintVerifier.ts @@ -30,9 +30,10 @@ import { ApalacheResult, ServerEndpoint, connect } from './apalache' */ export async function verify( serverEndpoint: ServerEndpoint, + apalacheVersion: string, config: any, verbosityLevel: number ): Promise> { - const connectionResult = await connect(serverEndpoint, verbosityLevel) + const connectionResult = await connect(serverEndpoint, apalacheVersion, verbosityLevel) return connectionResult.asyncChain(conn => conn.check(config)) }