Merge branch 'main' into gabriela/get-only-element

CHANGELOG.md

@@ -7,6 +7,18 @@ and this project adheres to [Semantic Versioning](https://semver.org/spec/v2.0.0
 
 ## UNRELEASED
 
+### Added
+### Changed
+### Deprecated
+### Removed
+### Fixed
+
+- Hashbang lines are now properly highlighted as comments in vscode and in highlight.js.
+
+### Security
+
+## v0.22.2 -- 2024-10-08
+
 ### Added
 
 - `quint verify` has the option `--apalache-version` to pull a custom version (#1521)
@@ -17,6 +29,9 @@ and this project adheres to [Semantic Versioning](https://semver.org/spec/v2.0.0
 ### Deprecated
 ### Removed
 ### Fixed
+
+- The seed was not being properly printed when the simulator found some runtime errors (#1524).
+
 ### Security
 
 ## v0.22.1 -- 2024-09-25

editor-plugins/highlight.js/quint.js

@@ -38,6 +38,7 @@ function quintHljs(hljs) {
         scope: 'number',
         begin: '-?(0x[0-9a-fA-F]([0-9a-fA-F]|_[0-9a-fA-F])*|0|[1-9]([0-9]|_[0-9])*)',
       },
+      hljs.SHEBANG, // file-leading hashbang
       hljs.C_LINE_COMMENT_MODE,  // single line comments
       hljs.C_BLOCK_COMMENT_MODE, // multiline comments
     ],

quint/io-cli-tests.md

@@ -101,7 +101,7 @@ in the lookup table for the expression with ID 7:
 
 <!-- !test in type and effect maps are output -->
 ```
-quint typecheck --out typecheck-out-example.json ../examples/language-features/tuples.qnt > /dev/null
+quint typecheck --out typecheck-out-example.json ../examples/language-features/tuples.qnt
 printf "first type: " && cat typecheck-out-example.json | jq '.types."7".type.kind'
 printf "first effect: " && cat typecheck-out-example.json | jq '.effects."8".effect.kind'
 rm typecheck-out-example.json
@@ -443,8 +443,8 @@ An example execution:
 [State 4] { n: 12 }
 
 [violation] Found an issue (duration).
-Use --seed=0x308623f2a48e7 to reproduce.
 Use --verbosity=3 to show executions.
+Use --seed=0x308623f2a48e7 to reproduce.
 error: Invariant violated
 ```
 
@@ -477,8 +477,8 @@ An example execution:
 [State 4] { action_taken: "OnDivByThree", n: 12, nondet_picks: {  } }
 
 [violation] Found an issue (duration).
-Use --seed=0x308623f2a48e7 to reproduce.
 Use --verbosity=3 to show executions.
+Use --seed=0x308623f2a48e7 to reproduce.
 error: Invariant violated
 ```
 
@@ -508,9 +508,9 @@ An example execution:
 [State 4] { n: 12 }
 
 [ok] No violation found (duration).
-Use --seed=0x11 to reproduce.
 You may increase --max-samples and --max-steps.
 Use --verbosity to produce more (or less) output.
+Use --seed=0x11 to reproduce.
 ```
 
 ### Repl evaluates coin
@@ -589,8 +589,8 @@ An example execution:
 }
 
 [violation] Found an issue (duration).
-Use --seed=0x1e352e160ffbb3 to reproduce.
 Use --verbosity=3 to show executions.
+Use --seed=0x1e352e160ffbb3 to reproduce.
 error: Invariant violated
 ```
 
@@ -721,8 +721,8 @@ q::stepAndInvariant => false
 }
 
 [violation] Found an issue (duration).
-Use --seed=0x1786e678d460fe to reproduce.
 Use --verbosity=3 to show executions.
+Use --seed=0x1786e678d460fe to reproduce.
 error: Invariant violated
 ```
 
@@ -1164,9 +1164,11 @@ error: Tests failed
 
 ### Fail on run with uninitialized constants
 
+FIXME: this should not be a runtime error
+
 <!-- !test in run uninitialized -->
 ```
-output=$(quint run testFixture/_1041compileConst.qnt 2>&1)
+output=$(quint run testFixture/_1041compileConst.qnt --seed=1 2>&1)
 exit_code=$?
 echo "$output" | sed -e 's/([0-9]*ms)/(duration)/g' \
   -e 's#^.*_1041compileConst.qnt#HOME/_1041compileConst.qnt#g'
@@ -1180,6 +1182,7 @@ HOME/_1041compileConst.qnt:5:24 - error: [QNT500] Uninitialized const N. Use: im
 5:   action init = { x' = N }
                           ^
 
+Use --seed=0x1 to reproduce.
 error: Runtime error
 ```
 

quint/package.json

@@ -1,6 +1,6 @@
 {
   "name": "@informalsystems/quint",
-  "version": "0.22.1",
+  "version": "0.22.2",
   "description": "Core tool for the Quint specification language",
   "keywords": [
     "temporal",

quint/src/cliCommands.ts

@@ -81,6 +81,7 @@ interface OutputStage {
   // Possible results from 'run'
   status?: 'ok' | 'violation' | 'failure' | 'error'
   trace?: QuintEx[]
+  seed?: bigint
   /* Docstrings by definition name by module name */
   documentation?: Map<string, Map<string, DocumentationEntry>>
   errors?: ErrorMessage[]
@@ -104,6 +105,7 @@ const pickOutputStage = ({
   ignored,
   status,
   trace,
+  seed,
 }: ProcedureStage) => {
   return {
     stage,
@@ -119,6 +121,7 @@ const pickOutputStage = ({
     ignored,
     status,
     trace,
+    seed,
   }
 }
 
@@ -567,6 +570,10 @@ export async function runSimulator(prev: TypecheckedStage): Promise<CLIProcedure
     ? { status: (evalResult.value as QuintBool).value ? 'ok' : 'violation' }
     : { status: 'error', errors: [evalResult.value] }
 
+  const states = recorder.bestTraces[0]?.frame?.args?.map(e => e.toQuintEx(zerog))
+  const frames = recorder.bestTraces[0]?.frame?.subframes
+  simulator.seed = recorder.bestTraces[0]?.seed
+
   recorder.bestTraces.forEach((trace, index) => {
     const maybeEvalResult = trace.frame.result
     if (maybeEvalResult.isLeft()) {
@@ -584,9 +591,6 @@ export async function runSimulator(prev: TypecheckedStage): Promise<CLIProcedure
     options.onTrace(index, status, evaluator.varNames(), states)
   })
 
-  const states = recorder.bestTraces[0]?.frame?.args?.map(e => e.toQuintEx(zerog))
-  const frames = recorder.bestTraces[0]?.frame?.subframes
-  const seed = recorder.bestTraces[0]?.seed
   switch (outcome.status) {
     case 'error':
       return cliErr('Runtime error', {
@@ -600,7 +604,6 @@ export async function runSimulator(prev: TypecheckedStage): Promise<CLIProcedure
       maybePrintCounterExample(verbosityLevel, states, frames)
       if (verbosity.hasResults(verbosityLevel)) {
         console.log(chalk.green('[ok]') + ' No violation found ' + chalk.gray(`(${elapsedMs}ms).`))
-        console.log(chalk.gray(`Use --seed=0x${seed.toString(16)} to reproduce.`))
         if (verbosity.hasHints(verbosityLevel)) {
           console.log(chalk.gray('You may increase --max-samples and --max-steps.'))
           console.log(chalk.gray('Use --verbosity to produce more (or less) output.'))
@@ -617,7 +620,6 @@ export async function runSimulator(prev: TypecheckedStage): Promise<CLIProcedure
       maybePrintCounterExample(verbosityLevel, states, frames)
       if (verbosity.hasResults(verbosityLevel)) {
         console.log(chalk.red(`[violation]`) + ' Found an issue ' + chalk.gray(`(${elapsedMs}ms).`))
-        console.log(chalk.gray(`Use --seed=0x${seed.toString(16)} to reproduce.`))
 
         if (verbosity.hasHints(verbosityLevel)) {
           console.log(chalk.gray('Use --verbosity=3 to show executions.'))
@@ -866,21 +868,28 @@ export async function docs(loaded: LoadedStage): Promise<CLIProcedure<Documentat
 export function outputResult(result: CLIProcedure<ProcedureStage>) {
   result
     .map(stage => {
+      const verbosityLevel = deriveVerbosity(stage.args)
       const outputData = pickOutputStage(stage)
       if (stage.args.out) {
         writeToJson(stage.args.out, outputData)
+      } else if (!stage.args.outItf && outputData.seed && verbosity.hasResults(verbosityLevel)) {
+        console.log(chalk.gray(`Use --seed=0x${outputData.seed.toString(16)} to reproduce.`))
       }
 
       process.exit(0)
     })
     .mapLeft(({ msg, stage }) => {
       const { args, errors, sourceCode } = stage
+      const verbosityLevel = deriveVerbosity(args)
       const outputData = pickOutputStage(stage)
       if (args.out) {
         writeToJson(args.out, outputData)
       } else {
         const finders = createFinders(sourceCode!)
         uniqWith(errors, isEqual).forEach(err => console.error(formatError(sourceCode, finders, err)))
+        if (!stage.args.outItf && outputData.seed && verbosity.hasResults(verbosityLevel)) {
+          console.log(chalk.gray(`Use --seed=0x${outputData.seed.toString(16)} to reproduce.`))
+        }
         console.error(`error: ${msg}`)
       }
       process.exit(1)

quint/src/version.ts

@@ -1,2 +1,2 @@
 // Generated by genversion.
-export const version = '0.22.1'
+export const version = '0.22.2'

vscode/quint-vscode/CHANGELOG.md

@@ -14,6 +14,24 @@ and this project adheres to [Semantic Versioning](https://semver.org/spec/v2.0.0
 ### Fixed
 ### Security
 
+## v0.14.8 -- 2024-10-18
+
+### Added
+### Changed
+### Deprecated
+### Removed
+### Fixed
+### Security
+
+## v0.14.7 -- 2024-10-08
+
+### Added
+### Changed
+### Deprecated
+### Removed
+### Fixed
+### Security
+
 ## v0.14.6 -- 2024-09-25
 
 ### Added

vscode/quint-vscode/package.json

@@ -3,7 +3,7 @@
 	"displayName": "Quint",
 	"description": "Language support for Quint specifications",
 	"icon": "./icons/logo.png",
-	"version": "0.14.6",
+	"version": "0.14.8",
 	"publisher": "informal",
 	"engines": {
 		"vscode": "^1.52.0"

vscode/quint-vscode/server/package.json

@@ -1,7 +1,7 @@
 {
   "name": "@informalsystems/quint-language-server",
   "description": "Language Server for the Quint specification language",
-  "version": "0.14.6",
+  "version": "0.14.8",
   "author": "Informal Systems",
   "contributors": [
     {
@@ -43,7 +43,7 @@
     "test/**/*.ts"
   ],
   "dependencies": {
-    "@informalsystems/quint": "^0.22.1",
+    "@informalsystems/quint": "^0.22.2",
     "vscode-languageserver": "^7.0.0",
     "vscode-languageserver-textdocument": "^1.0.1",
     "vscode-uri": "^3.0.7"

vscode/quint-vscode/syntaxes/quint.tmLanguage.json

@@ -2,6 +2,9 @@
 	"$schema": "https://raw.githubusercontent.com/martinring/tmlanguage/master/tmlanguage.json",
 	"name": "Quint",
 	"patterns": [
+		{
+			"include": "#hashbangLine"
+		},
 		{
 			"include": "#lineComments"
 		},
@@ -92,6 +95,14 @@
 				}
 			]
 		},
+		"hashbangLine": {
+			"patterns": [
+				{
+					"name": "comment.line.hashbang.quint",
+					"match": "^#!.*$"
+				}
+			]
+		},
 		"lineComments": {
 			"patterns": [
 				{