Skip to content

Commit 2d139a0

Browse files
bugarelabugarela
authored
Merge branch 'main' into igor/tendermint-imports
2 parents 9160200 + 4ee5c50 commit 2d139a0

10 files changed

+369
-97
lines changed

‎CHANGELOG.md

+27-2
Original file line numberDiff line numberDiff line change
@@ -9,9 +9,34 @@ and this project adheres to [Semantic Versioning](https://semver.org/spec/v2.0.0
99

1010
### Added
1111
### Changed
12+
### Deprecated
13+
### Removed
14+
### Fixed
15+
### Security
16+
17+
## v0.14.1 -- 2023-08-28
18+
19+
### Added
20+
### Changed
21+
### Deprecated
22+
### Removed
23+
### Fixed
24+
25+
- Fix problem with broken dependency by pinning versions (#1129)
26+
27+
### Security
28+
29+
## v0.14.0 -- 2023-08-25
30+
31+
### Added
32+
33+
- The `verify` command now automatically acquires the Apalache distribution and
34+
starts the server, if the server is not already running (#1115)
35+
36+
### Changed
1237

13-
- The `verify` command now manages Apalache server, if no already running
14-
instance is detected (#1115)
38+
- Module management was rewritten, and instances should behave much better in
39+
the simulator, REPL, and in integration with Apalache (#1119)
1540

1641
### Deprecated
1742
### Removed

‎quint/package-lock.json

+26-26
Some generated files are not rendered by default. Learn more about customizing how changed files appear on GitHub.

‎quint/package.json

+3-3
Original file line numberDiff line numberDiff line change
@@ -1,6 +1,6 @@
11
{
22
"name": "@informalsystems/quint",
3-
"version": "0.13.0",
3+
"version": "0.14.1",
44
"description": "Core tool for the Quint specification language",
55
"keywords": [
66
"temporal",
@@ -51,8 +51,8 @@
5151
"@grpc/grpc-js": "^1.8.14",
5252
"@grpc/proto-loader": "^0.7.7",
5353
"@octokit/request": "^8.1.1",
54-
"@sweet-monads/either": "^3.0.1",
55-
"@sweet-monads/maybe": "^3.1.0",
54+
"@sweet-monads/either": "~3.2.0",
55+
"@sweet-monads/maybe": "~3.2.0",
5656
"@types/line-column": "^1.0.0",
5757
"@types/seedrandom": "^3.0.4",
5858
"antlr4ts": "^0.5.0-alpha.4",

‎quint/src/quintVerifier.ts

+86-45
Original file line numberDiff line numberDiff line change
@@ -19,7 +19,8 @@ import { ErrorMessage } from './parsing/quintParserFrontend'
1919
import path from 'path'
2020
import fs from 'fs'
2121
import os from 'os'
22-
import semver from 'semver'
22+
// TODO: used by GitHub api approach: https://github.com/informalsystems/quint/issues/1124
23+
// import semver from 'semver'
2324
import fetch from 'node-fetch'
2425
import { pipeline } from 'stream/promises'
2526
import child_process from 'child_process'
@@ -30,14 +31,16 @@ import * as protobufDescriptor from 'protobufjs/ext/descriptor'
3031
import { setTimeout } from 'timers/promises'
3132
import { promisify } from 'util'
3233
import { ItfTrace } from './itf'
33-
import { request as octokitRequest } from '@octokit/request'
34+
// TODO: used by GitHub api approach: https://github.com/informalsystems/quint/issues/1124
35+
// import { request as octokitRequest } from '@octokit/request'
3436

3537
import type { Buffer } from 'buffer'
3638
import type { PackageDefinition as ProtoPackageDefinition } from '@grpc/proto-loader'
3739

3840
const APALACHE_SERVER_URI = 'localhost:8822'
39-
const APALACHE_VERSION_TAG = '0.42.x'
40-
const APALACHE_TGZ = 'apalache.tgz'
41+
const APALACHE_VERSION_TAG = '0.42.0'
42+
// TODO: used by GitHub api approach: https://github.com/informalsystems/quint/issues/1124
43+
// const APALACHE_TGZ = 'apalache.tgz'
4144

4245
// The structure used to report errors
4346
type VerifyError = {
@@ -46,6 +49,14 @@ type VerifyError = {
4649
traces?: ItfTrace[]
4750
}
4851

52+
function quintConfigDir(): string {
53+
return path.join(os.homedir(), '.quint')
54+
}
55+
56+
function apalacheDistDir(): string {
57+
return path.join(quintConfigDir(), `apalache-dist-${APALACHE_VERSION_TAG}`)
58+
}
59+
4960
export type VerifyResult<T> = Either<VerifyError, T>
5061

5162
// An object representing the Apalache configuration
@@ -260,6 +271,21 @@ async function tryConnect(retry: boolean = false): Promise<VerifyResult<Apalache
260271
return (await loadProtoDefViaReflection(retry)).map(loadGrpcClient).map(apalache)
261272
}
262273

274+
function downloadAndUnpackApalache(): Promise<VerifyResult<null>> {
275+
const url = `https://github.com/informalsystems/apalache/releases/download/v${APALACHE_VERSION_TAG}/apalache.tgz`
276+
console.log(`Downloading Apalache distribution from ${url}...`)
277+
return fetch(url)
278+
.then(
279+
// unpack response body
280+
res => pipeline(res.body, tar.extract({ cwd: apalacheDistDir(), strict: true })),
281+
error => err(`Error fetching ${url}: ${error}`)
282+
)
283+
.then(
284+
_ => right(null),
285+
error => err(`Error unpacking .tgz: ${error}`)
286+
)
287+
}
288+
263289
/**
264290
* Fetch the latest Apalache release pinned by `APALACHE_VERSION_TAG` from Github.
265291
*
@@ -268,43 +294,59 @@ async function tryConnect(retry: boolean = false): Promise<VerifyResult<Apalache
268294
* - a `left<VerifyError>` indicating an error.
269295
*/
270296
async function fetchApalache(): Promise<VerifyResult<string>> {
297+
const apalacheBinary = path.join(apalacheDistDir(), 'apalache', 'bin', 'apalache-mc')
298+
if (fs.existsSync(apalacheBinary)) {
299+
// Use existing download
300+
console.log(`Using existing Apalache distribution in ${apalacheBinary}`)
301+
return right(apalacheBinary)
302+
} else {
303+
fs.mkdirSync(apalacheDistDir(), { recursive: true })
304+
const res = await downloadAndUnpackApalache()
305+
return res.map(_ => apalacheBinary)
306+
}
307+
308+
// TODO: This logic makes the CLI tool extremely sensitive to environment.
309+
// See https://github.com/informalsystems/quint/issues/1124
271310
// Fetch Github releases
272-
return octokitRequest('GET /repos/informalsystems/apalache/releases').then(
273-
async resp => {
274-
// Find latest that satisfies `APALACHE_VERSION_TAG`
275-
const versions = resp.data.map((element: any) => element.tag_name)
276-
const latestTaggedVersion = semver.maxSatisfying(versions, APALACHE_VERSION_TAG)
277-
// Check if we have already downloaded this release
278-
const unpackPath = path.join(os.homedir(), '.quint', `apalache-dist-${latestTaggedVersion}`)
279-
const apalacheBinary = path.join(unpackPath, 'apalache', 'bin', 'apalache-mc')
280-
if (fs.existsSync(apalacheBinary)) {
281-
// Use existing download
282-
console.log(`Using existing Apalache distribution in ${unpackPath}`)
283-
return right(unpackPath)
284-
} else {
285-
// No existing download, download Apalache dist
286-
fs.mkdirSync(unpackPath, { recursive: true })
287-
288-
// Filter release response to get dist archive asset URL
289-
const taggedRelease = resp.data.find((element: any) => element.tag_name == latestTaggedVersion)
290-
const tgzAsset = taggedRelease.assets.find((asset: any) => asset.name == APALACHE_TGZ)
291-
const downloadUrl = tgzAsset.browser_download_url
292-
293-
console.log(`Downloading Apalache distribution from ${downloadUrl}...`)
294-
return fetch(downloadUrl)
295-
.then(
296-
// unpack response body
297-
res => pipeline(res.body, tar.extract({ cwd: unpackPath, strict: true })),
298-
error => err(`Error fetching ${downloadUrl}: ${error}`)
299-
)
300-
.then(
301-
_ => right(unpackPath),
302-
error => err(`Error unpacking .tgz: ${error}`)
303-
)
304-
}
305-
},
306-
error => err(`Error listing the Apalache releases: ${error}`)
307-
)
311+
// return octokitRequest('GET /repos/informalsystems/apalache/releases').then(
312+
// async resp => {
313+
// // Find latest that satisfies `APALACHE_VERSION_TAG`
314+
// const versions = resp.data.map((element: any) => element.tag_name)
315+
// const latestTaggedVersion = semver.parse(semver.maxSatisfying(versions, APALACHE_VERSION_TAG))
316+
// if (latestTaggedVersion === null) {
317+
// return err(`Failed to deteremine a valid semver version vesion from ${versions} and ${APALACHE_VERSION_TAG}`)
318+
// }
319+
// // Check if we have already downloaded this release
320+
// const unpackPath = apalacheDistDir()
321+
// const apalacheBinary = path.join(unpackPath, 'apalache', 'bin', 'apalache-mc')
322+
// if (fs.existsSync(apalacheBinary)) {
323+
// // Use existing download
324+
// console.log(`Using existing Apalache distribution in ${unpackPath}`)
325+
// return right(unpackPath)
326+
// } else {
327+
// // No existing download, download Apalache dist
328+
// fs.mkdirSync(unpackPath, { recursive: true })
329+
330+
// // Filter release response to get dist archive asset URL
331+
// const taggedRelease = resp.data.find((element: any) => element.tag_name == latestTaggedVersion)
332+
// const tgzAsset = taggedRelease.assets.find((asset: any) => asset.name == APALACHE_TGZ)
333+
// const downloadUrl = tgzAsset.browser_download_url
334+
335+
// console.log(`Downloading Apalache distribution from ${downloadUrl}...`)
336+
// return fetch(downloadUrl)
337+
// .then(
338+
// // unpack response body
339+
// res => pipeline(res.body, tar.extract({ cwd: unpackPath, strict: true })),
340+
// error => err(`Error fetching ${downloadUrl}: ${error}`)
341+
// )
342+
// .then(
343+
// _ => right(unpackPath),
344+
// error => err(`Error unpacking .tgz: ${error}`)
345+
// )
346+
// }
347+
// },
348+
// error => err(`Error listing the Apalache releases: ${error}`)
349+
// )
308350
}
309351

310352
/**
@@ -327,15 +369,14 @@ async function connect(): Promise<VerifyResult<Apalache>> {
327369

328370
// Connection or pinging failed, download Apalache
329371
console.log("Couldn't connect to Apalache, checking for latest supported release")
330-
const distDir = await fetchApalache()
372+
const exeResult = await fetchApalache()
331373
// Launch Apalache from download
332-
return distDir
374+
return exeResult
333375
.asyncChain(
334-
async distDir =>
376+
async exe =>
335377
new Promise<VerifyResult<void>>((resolve, _) => {
336378
console.log('Launching Apalache server')
337-
const apalacheBinary = path.join(distDir, 'apalache', 'bin', 'apalache-mc')
338-
const apalache = child_process.spawn(apalacheBinary, ['server'])
379+
const apalache = child_process.spawn(exe, ['server'])
339380

340381
// Exit handler that kills Apalache if Quint exists
341382
function exitHandler() {

‎quint/src/version.ts

+1-1
Original file line numberDiff line numberDiff line change
@@ -1,2 +1,2 @@
11
// Generated by genversion.
2-
export const version = '0.13.0'
2+
export const version = '0.14.1'

‎vscode/quint-vscode/CHANGELOG.md

+9
Original file line numberDiff line numberDiff line change
@@ -14,6 +14,15 @@ and this project adheres to [Semantic Versioning](https://semver.org/spec/v2.0.0
1414
### Fixed
1515
### Security
1616

17+
## v0.8.0 -- 2023-08-25
18+
19+
### Added
20+
### Changed
21+
### Deprecated
22+
### Removed
23+
### Fixed
24+
### Security
25+
1726
## v0.7.0 -- 2023-08-06
1827

1928
### Added

‎vscode/quint-vscode/package-lock.json

+2-2
Some generated files are not rendered by default. Learn more about customizing how changed files appear on GitHub.

‎vscode/quint-vscode/package.json

+1-1
Original file line numberDiff line numberDiff line change
@@ -2,7 +2,7 @@
22
"name": "quint-vscode",
33
"displayName": "Quint",
44
"description": "Language support for Quint specifications",
5-
"version": "0.7.0",
5+
"version": "0.8.0",
66
"publisher": "informal",
77
"engines": {
88
"vscode": "^1.52.0"

0 commit comments

Comments
 (0)