diff --git a/client/package-lock.json b/client/package-lock.json index 45696369..66f4a29c 100644 --- a/client/package-lock.json +++ b/client/package-lock.json @@ -1,12 +1,12 @@ { "name": "viper", - "version": "5.2.0", + "version": "5.3.0", "lockfileVersion": 3, "requires": true, "packages": { "": { "name": "viper", - "version": "5.2.0", + "version": "5.3.0", "license": "SEE LICENSE IN LICENSE.txt", "dependencies": { "@octokit/rest": "19.0.13" @@ -732,7 +732,6 @@ "version": "4.2.4", "resolved": "https://registry.npmjs.org/@octokit/core/-/core-4.2.4.tgz", "integrity": "sha512-rYKilwgzQ7/imScn3M9/pFfUf4I1AZEH3KhyJmtPdE2zfaXAn2mFfUy4FbKewzc2We5y/LlKLj36fWJLKC2SIQ==", - "peer": true, "dependencies": { "@octokit/auth-token": "^3.0.0", "@octokit/graphql": "^5.0.0", @@ -1291,7 +1290,6 @@ "resolved": "https://registry.npmjs.org/@types/node/-/node-24.9.1.tgz", "integrity": "sha512-QoiaXANRkSXK6p0Duvt56W208du4P9Uye9hWLWgGMDTEoKPhuenzNcC4vGUmrNkiOKTlIrBoyNQYNpSwfEZXSg==", "dev": true, - "peer": true, "dependencies": { "undici-types": "~7.16.0" } @@ -1394,7 +1392,6 @@ "resolved": "https://registry.npmjs.org/@typescript-eslint/parser/-/parser-8.46.2.tgz", "integrity": "sha512-BnOroVl1SgrPLywqxyqdJ4l3S2MsKVLDVxZvjI1Eoe8ev2r3kGDo+PcMihNmDE+6/KjkTubSJnmqGZZjQSBq/g==", "dev": true, - "peer": true, "dependencies": { "@typescript-eslint/scope-manager": "8.46.2", "@typescript-eslint/types": "8.46.2", @@ -2038,7 +2035,6 @@ "resolved": "https://registry.npmjs.org/acorn/-/acorn-8.15.0.tgz", "integrity": "sha512-NZyJarBfL7nWwIq+FDL6Zp/yHEhePMNnnJ0y3qfieCrmNvYct8uvtiV41UvlSe6apAfk0fY1FbWx+NwfmpvtTg==", "dev": true, - "peer": true, "bin": { "acorn": "bin/acorn" }, @@ -2093,7 +2089,6 @@ "resolved": "https://registry.npmjs.org/ajv/-/ajv-8.17.1.tgz", "integrity": "sha512-B/gBuNg5SiMTrPkC+A2+cW0RszwxYmn6VYxB/inlBStS5nx6xHIt/ehKRhIMhqusl7a8LjQoZnjCs5vhwxOQ1g==", "dev": true, - "peer": true, "dependencies": { "fast-deep-equal": "^3.1.3", "fast-uri": "^3.0.1", @@ -2424,7 +2419,6 @@ "url": "https://github.com/sponsors/ai" } ], - "peer": true, "dependencies": { "baseline-browser-mapping": "^2.8.19", "caniuse-lite": "^1.0.30001751", @@ -3540,7 +3534,6 @@ "resolved": "https://registry.npmjs.org/eslint/-/eslint-9.38.0.tgz", "integrity": "sha512-t5aPOpmtJcZcz5UJyY2GbvpDlsK5E8JqRqoKtfiKE3cNh437KIqfJr3A3AKf5k64NPx6d0G3dno6XDY05PqPtw==", "dev": true, - "peer": true, "dependencies": { "@eslint-community/eslint-utils": "^4.8.0", "@eslint-community/regexpp": "^4.12.1", @@ -8644,7 +8637,6 @@ "resolved": "https://registry.npmjs.org/typescript/-/typescript-5.9.3.tgz", "integrity": "sha512-jl1vZzPDinLr9eUt3J/t7V6FgNEw9QjvBPdysz9KfQDD41fQrC2Y4vKQdiaUpFT4bXlb1RHhLpp8wtm6M5TgSw==", "dev": true, - "peer": true, "bin": { "tsc": "bin/tsc", "tsserver": "bin/tsserver" @@ -8924,7 +8916,6 @@ "resolved": "https://registry.npmjs.org/webpack/-/webpack-5.102.1.tgz", "integrity": "sha512-7h/weGm9d/ywQ6qzJ+Xy+r9n/3qgp/thalBbpOi5i223dPXKi04IBtqPN9nTd+jBc7QKfvDbaBnFipYp4sJAUQ==", "dev": true, - "peer": true, "dependencies": { "@types/eslint-scope": "^3.7.7", "@types/estree": "^1.0.8", @@ -8973,7 +8964,6 @@ "resolved": "https://registry.npmjs.org/webpack-cli/-/webpack-cli-6.0.1.tgz", "integrity": "sha512-MfwFQ6SfwinsUVi0rNJm7rHZ31GyTcpVE5pgVA3hwFRb7COD4TzjUUwhGWKfO50+xdc2MQPuEBBJoqIMGt3JDw==", "dev": true, - "peer": true, "dependencies": { "@discoveryjs/json-ext": "^0.6.1", "@webpack-cli/configtest": "^3.0.1", diff --git a/client/package.json b/client/package.json index bfb55bfe..1999f4de 100644 --- a/client/package.json +++ b/client/package.json @@ -1,7 +1,7 @@ { "name": "viper", "displayName": "Viper", - "version": "5.2.0", + "version": "5.3.0", "publisher": "viper-admin", "description": "This extension provides interactive IDE features for verifying programs in Viper (Verification Infrastructure for Permission-based Reasoning).", "license": "SEE LICENSE IN LICENSE.txt", @@ -320,7 +320,7 @@ }, "viper.viperServer.customArguments": { "type": "string", - "default": "--serverMode LSP --singleClient $backendSpecificCache$ --logLevel $logLevel$ --logFile $logFile$", + "default": "--serverMode LSP --singleClient $backendSpecificCache$ $beginnerMode$ --logLevel $logLevel$ --logFile $logFile$", "description": "The command line arguments used for starting the Viper Server." }, "viper.viperServer.backendSpecificCache": { @@ -328,6 +328,11 @@ "default": true, "markdownDescription": "Use a separate cache for both backends, the option `$backendSpecificCache$` turns into `\"--backendSpecificCache\"` or `\"\"`, depending on this setting." }, + "viper.viperServer.beginnerMode": { + "type": "boolean", + "default": true, + "markdownDescription": "Disable some advanced features that can be confusing for beginners. The option `$beginnerMode$` turns into `\"--beginnerMode\"` or `\"\"`, depending on this setting." + }, "viper.viperServer.disableCaching": { "type": "boolean", "default": false, diff --git a/client/src/ExtensionState.ts b/client/src/ExtensionState.ts index 9087ccec..bd791929 100644 --- a/client/src/ExtensionState.ts +++ b/client/src/ExtensionState.ts @@ -29,7 +29,7 @@ import { ProjectManager, ProjectRoot } from './ProjectManager'; export class State { public static get MIN_SERVER_VERSION(): string { - return "3.0.0"; // has to be a valid semver + return "3.1.0"; // has to be a valid semver } public static serverVersion: string; diff --git a/client/src/Settings.ts b/client/src/Settings.ts index 99ba3e4a..06187bbc 100644 --- a/client/src/Settings.ts +++ b/client/src/Settings.ts @@ -942,8 +942,10 @@ export class Settings { const configuredArgString = Settings.getConfiguration("viperServer").customArguments; const useBackendSpecificCache = Settings.getConfiguration("viperServer").backendSpecificCache === true; + const beginnerMode = Settings.getConfiguration("viperServer").beginnerMode === true; return configuredArgString .replace("$backendSpecificCache$", useBackendSpecificCache ? "--backendSpecificCache" : "") + .replace("$beginnerMode$", beginnerMode ? "--beginnerMode" : "") .replace("$logLevel$", convertLogLevel(logLevel)) // note that we use functions as 2nd argument since we do not want that // the special replacement patterns kick in diff --git a/client/src/ViperProtocol.ts b/client/src/ViperProtocol.ts index aa3f72e9..f8ebe194 100644 --- a/client/src/ViperProtocol.ts +++ b/client/src/ViperProtocol.ts @@ -396,6 +396,8 @@ export interface ViperServerSettings { customArguments: string; //it set to false, cached errors are reused across backends backendSpecificCache: boolean; + //if set to true, some advanced features are disabled that can be confusing for beginners + beginnerMode: boolean; //disable the caching mechanism disableCaching: boolean; //After timeout ms the startup of the viperServer is expected to have failed and thus aborted