Skip to content

Commit f781775

Browse files
Add beginner mode (#542)
* Add presentation mode * Change to beginner mode * updated server version --------- Co-authored-by: Nicolas Klose <nicolas.klose@inf.ethz.ch>
1 parent f797b8b commit f781775

7 files changed

Lines changed: 25 additions & 10 deletions

File tree

client/package-lock.json

Lines changed: 6 additions & 6 deletions
Some generated files are not rendered by default. Learn more about customizing how changed files appear on GitHub.

client/package.json

Lines changed: 7 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -1,7 +1,7 @@
11
{
22
"name": "viper",
33
"displayName": "Viper",
4-
"version": "5.2.0",
4+
"version": "5.3.0",
55
"publisher": "viper-admin",
66
"description": "This extension provides interactive IDE features for verifying programs in Viper (Verification Infrastructure for Permission-based Reasoning).",
77
"license": "SEE LICENSE IN LICENSE.txt",
@@ -320,14 +320,19 @@
320320
},
321321
"viper.viperServer.customArguments": {
322322
"type": "string",
323-
"default": "--serverMode LSP --singleClient $backendSpecificCache$ --logLevel $logLevel$ --logFile $logFile$",
323+
"default": "--serverMode LSP --singleClient $backendSpecificCache$ $beginnerMode$ --logLevel $logLevel$ --logFile $logFile$",
324324
"description": "The command line arguments used for starting the Viper Server."
325325
},
326326
"viper.viperServer.backendSpecificCache": {
327327
"type": "boolean",
328328
"default": true,
329329
"markdownDescription": "Use a separate cache for both backends, the option `$backendSpecificCache$` turns into `\"--backendSpecificCache\"` or `\"\"`, depending on this setting."
330330
},
331+
"viper.viperServer.beginnerMode": {
332+
"type": "boolean",
333+
"default": true,
334+
"markdownDescription": "Disable some advanced features that can be confusing for beginners. The option `$beginnerMode$` turns into `\"--beginnerMode\"` or `\"\"`, depending on this setting."
335+
},
331336
"viper.viperServer.disableCaching": {
332337
"type": "boolean",
333338
"default": false,

client/src/ExtensionState.ts

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -29,7 +29,7 @@ import { ProjectManager, ProjectRoot } from './ProjectManager';
2929

3030
export class State {
3131
public static get MIN_SERVER_VERSION(): string {
32-
return "3.0.0"; // has to be a valid semver
32+
return "3.1.0"; // has to be a valid semver
3333
}
3434
public static serverVersion: string;
3535

client/src/Settings.ts

Lines changed: 2 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -942,8 +942,10 @@ export class Settings {
942942

943943
const configuredArgString = Settings.getConfiguration("viperServer").customArguments;
944944
const useBackendSpecificCache = Settings.getConfiguration("viperServer").backendSpecificCache === true;
945+
const beginnerMode = Settings.getConfiguration("viperServer").beginnerMode === true;
945946
return configuredArgString
946947
.replace("$backendSpecificCache$", useBackendSpecificCache ? "--backendSpecificCache" : "")
948+
.replace("$beginnerMode$", beginnerMode ? "--beginnerMode" : "")
947949
.replace("$logLevel$", convertLogLevel(logLevel))
948950
// note that we use functions as 2nd argument since we do not want that
949951
// the special replacement patterns kick in

client/src/ViperProtocol.ts

Lines changed: 2 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -396,6 +396,8 @@ export interface ViperServerSettings {
396396
customArguments: string;
397397
//it set to false, cached errors are reused across backends
398398
backendSpecificCache: boolean;
399+
//if set to true, some advanced features are disabled that can be confusing for beginners
400+
beginnerMode: boolean;
399401
//disable the caching mechanism
400402
disableCaching: boolean;
401403
//After timeout ms the startup of the viperServer is expected to have failed and thus aborted

client/viperserver-version

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -1 +1 @@
1-
v-2026-01-24-0712
1+
v-2026-02-17-0930

package-lock.json

Lines changed: 6 additions & 0 deletions
Some generated files are not rendered by default. Learn more about customizing how changed files appear on GitHub.

0 commit comments

Comments
 (0)