Merge pull request #1521 from konnov/igor/apalache-version

Add the option `--apalache-version` to `quint verify`

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

quint/apalache-dist-tests.md

@@ -31,7 +31,7 @@ quint verify --verbosity=1 ../examples/language-features/booleans.qnt | \
 
 <!-- !test out server not running -->
 ```
-Downloading Apalache distribution... done.
+Downloading Apalache distribution 0.46.1... done.
 [ok] No violation found (duration).
 [ok] No violation found (duration).
 ```

quint/src/apalache.ts

@@ -75,16 +75,16 @@ 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'
 
 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<ApalacheResult<null>> {
-  const url = `https://github.com/apalache-mc/apalache/releases/download/v${APALACHE_VERSION_TAG}/apalache.tgz`
+function downloadAndUnpackApalache(apalacheVersion: string): Promise<ApalacheResult<null>> {
+  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<ApalacheResult<null>> {
  *    - a `right<string>` equal to the path the Apalache dist was unpacked to,
  *    - a `left<ApalacheError>` indicating an error.
  */
-async function fetchApalache(verbosityLevel: number): Promise<ApalacheResult<string>> {
+async function fetchApalache(apalacheVersion: string, verbosityLevel: number): Promise<ApalacheResult<string>> {
   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<ApalacheResult<str
  */
 export async function connect(
   serverEndpoint: ServerEndpoint,
+  apalacheVersion: string,
   verbosityLevel: number
 ): Promise<ApalacheResult<Apalache>> {
   // 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(

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

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<CLIProcedure<Trac
 
   const startMs = Date.now()
 
-  return verify(args.serverEndpoint, config, verbosityLevel).then(res => {
+  return verify(args.serverEndpoint, args.apalacheVersion, config, verbosityLevel).then(res => {
     const elapsedMs = Date.now() - startMs
     return res
       .map(_ => {

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<ApalacheResult<string>> {
@@ -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))
 }

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<ApalacheResult<void>> {
-  const connectionResult = await connect(serverEndpoint, verbosityLevel)
+  const connectionResult = await connect(serverEndpoint, apalacheVersion, verbosityLevel)
   return connectionResult.asyncChain(conn => conn.check(config))
 }