Settings

Visual Studio Code provides many configurable settings that allow you to fine-tune the behaviour of the tool and its extensions. This page describes the settings that are available for the VDM VSCode extension. Most settings have sensible default values and for normal usage they do not need to be changed.

Settings can be changed by using the cog wheel icon at the bottom right of the UI on the activity bar, and selecting Settings (or by typing CTRL+,). The settings UI can be filtered; entering "vdm-vscode" will filter out the settings for the VDM VSCode extension. Note that settings can be stored by User (i.e. they apply to all projects opened by the current user), by Workspace (i.e. they apply to all projects within a workspace, regardless of user), or by Folder (i.e. they apply specifically to one project, regardless of the workspace or user). More specific settings override more general ones (i.e. a Folder setting overrides a Workspace setting, which overrides a User setting).

Server Settings

• vdm-vscode.server.JVMArguments JVM arguments used when launching the server.
• vdm-vscode.server.classPathAdditions List of folder and/or file paths that should be included in the class path for the language server. Examples of things to add to the classpath are external format readers and QuickCheck strategies; to add libraries, plugins or annotations, instead use the configuration 'Server > Extension Search Paths' for better integration. Find folders, Find files, or type in manually.
• vdm-vscode.server.highPrecision Use high precision variant of VDMJ.
• vdm-vscode.server.strict Activate the VDMJ -strict flag that highlights (with warnings) where a specification is taking advantage of lenient parsing rule.
• vdm-vscode.server.release Activates the selected release of VDMJ, allowing VDMJ to parse specs that adhere to the this VDM release. Either "classic" or "vdm10".
• vdm-vscode.server.extensionSearchPaths Specifies additional paths to search for VDMJ extensions, i.e. plugins, libraries and annotations. Other types of extensions are not natively supported by the extension, and will need to be added to the class path through the 'Server > Class Path Additions' configuration. The paths can either point directly to an extension jar or a directory containing multiple extension jars. Add directories to the search path, Add jars to the search path, or type a path manually.
• vdm-vscode.server.plugins.enabled Plugins to enable/disable. If a plugin is enabled in the User settings but explicitly disabled in the Workspace or Workspace Folder settings, the Workspace settings take precedence. This setting only affects plugins found in the search paths.
• vdm-vscode.server.annotations.enabled Annotations to enable/disable. If an annotation is enabled in the User settings but explicitly disabled in the Workspace or Workspace Folder settings, the Workspace settings take precedence. This setting only affects annotations found in the search paths. Built-in annotations are enabled by default and must be explicitly disabled if not needed.

Code Generation Settings

• vdm-vscode.javaCodeGen.disableCloning Disable cloning (may lead to code being generated that does not preserve the semantics of the input specification)
• vdm-vscode.javaCodeGen.sequencesAsStrings Generate character sequences as strings
• vdm-vscode.javaCodeGen.concurrencyMechanisms Generate concurrency mechanisms
• vdm-vscode.javaCodeGen.vdmLocationInformation Generate VDM location information for code generated constructs
• vdm-vscode.javaCodeGen.outputPackage Choose output package e.g : my.code
• vdm-vscode.javaCodeGen.skipClassesModules Skip classes/modules during the code generation process. Separate by ';' e.g : World;Env

Translation Settings

• vdm-vscode.translate.latex.modelOnly Only model part will be included in the Latex translation, i.e., everything enclosed within '\begin{vdm_al}' and '\end{vdm_al}'
• vdm-vscode.translate.latex.markCoverage Mark coverage in the Latex translation
• vdm-vscode.translate.latex.insertCoverageTables Insert coverage tables in the Latex translation
• vdm-vscode.translate.general.storeAllTranslations Stores each translation in a timestamped folder instead of overwriting the previous content
• vdm-vscode.translate.general.allowSingleFileTranslation If enabled, translates only the selected file. If disabled, translate is always applied to the whole project
• vdm-vscode.translate.isabelle.strict Strict handling of certain errors (e.g. print output or not, raise VDMJ warnings as translation errors, etc.).
• vdm-vscode.translate.isabelle.maxErrors Maximum number (default=100) of translation errors to report. This is similar to VDMJ's maxErrors
• vdm-vscode.translate.isabelle.isaVersion Isabelle/HOL version target for translation.
• vdm-vscode.translate.isabelle.reportVDMWarnings Report VDMJ warnings as part of the plugin output.
• vdm-vscode.translate.isabelle.debug Report VDMJ warnings as part of the plugin output.
• vdm-vscode.translate.isabelle.linientInvCheck Exu invariant type checks allow subtyping instead of explicit invariant/pre calls.
• vdm-vscode.translate.isabelle.retypecheck Exu module sorting creates a new module, which you can re typecheck to ensure no VDM type errors have occured as a result of sorting.
• vdm-vscode.translate.isabelle.linientPost Translate VDM source as an Isabelle comment alongside its translation.
• vdm-vscode.translate.isabelle.printVDMComments Prints VDM user comments as Isabelle comments when true, or ignore them when false.
• vdm-vscode.translate.isabelle.printIsaComments Prints Isabelle translation comments to the user (e.g., explanatory comments about translation's implicit VDM checks).
• vdm-vscode.translate.isabelle.runExu Chooses whether to run the Exu VDM analyser prior to translation. Exu will provide information about VDM style and potential translation issues.
• vdm-vscode.translate.isabelle.valueAsAbbreviation Translate VDM values as Isabelle abbreviations when true, and as Isabelle definitions when false.
• vdm-vscode.translate.isabelle.translateTypeDefMinMax Translate VDM min_T or max_T when translating ordering predicates for type definitions.
• vdm-vscode.translate.isabelle.printVDMSource Translate VDM source as an Isabelle comment immediately before its translation.
• vdm-vscode.translate.isabelle.printLocations Translate VDM source location information as an Isabelle comment alongside its VDM source translation.
• vdm-vscode.translate.isabelle.runIsapog Translate VDM POs as a separate theory file associated with the recently translated VDM model.
• vdm-vscode.translate.isabelle.createPogLocaleLemmas Translate VDM POs within an Isabelle locale with separate lemmas per PO.
• vdm-vscode.translate.isabelle.proofStrategy Proof strategy choice for the isapog plugin. It determines what kind of proof script the plugin will generate for the translated PO.

Other Settings

• vdm-vscode.coverage.UseHeatmapColouring If enabled, the number of hits (larger than zero) corresponds to a brighter green. If disabled, all sections with any number (hits larger than zero) are colored the same green.
• vdm-vscode.coverage.OverlayLatestCoverage If enabled, the latest generated coverage is utilised for overlaying. If disabled, it is possible to choose which coverage should be used for overlaying.
• vdm-vscode.encoding.showWarning If enabled, shows a warning if document encoding is not UTF-8
• vdm-vscode.combinatorialTesting.groupSize Determine the maximum group size for tests in the combinatorial testing view
• vdm-vscode.codeLenses.enabled Enable/disable code lenses
• vdm-vscode.vdmtools.path.vdmpp Path to VDMTools for VDM++.
• vdm-vscode.vdmtools.path.vdmsl Path to VDMTools for VDM-SL.
• vdm-vscode.real-timeLogViewer.scaleWithEditorFont Enable scaling of the view relative to the current font size of the editor
• vdm-vscode.real-timeLogViewer.matchTheme Enable colours of the view to match the current theme of the editor
• vdm-vscode.real-timeLogViewer.fontSize Font size to use for the relative scaling of elements in the diagram. Only used if #vdm-vscode.other.real-timeLogViewer.scaleWithEditorFont# is disabled

Development Settings

• vdm-vscode.trace.server Enables tracing of LSP messages between VS Code and the VDMJ language server. The trace may contain file paths, source code, and other potentially sensitive information from your project
• vdm-vscode.trace.debug Enables tracing of DAP messages
• vdm-vscode.server.development.experimentalServer Use experimental server. True if the client should not launch the server, but connect to a server on a socket connection determined by #vdm-vscode.server.development.experimentalServer#.
• vdm-vscode.server.development.lspPort Port used for LSP. NOTE: Only used when #vdm-vscode.server.development.experimentalServer# is active.
• vdm-vscode.server.logLevel Enables logging of the VDMJ server to a file in this folder. This log can be used to diagnose server issues. The log may contain file paths, source code, and other potentially sensitive information from your project.
• vdm-vscode.server.stdio.activateStdoutLogging Activate logging of stdout/stderr to the terminal window. NOTE: This may cause performance slowdown if specifications have many annotations.
• vdm-vscode.server.stdio.stdioLogPath File path for the directory that should be used to store stdout/stderr logs. NOTE: If empty, terminal logging is used instead of file logging. The setting is only used when #vdm-vscode.server.stdio.activateStdoutLogging# is active.
• vdm-vscode.server.verbose Activate the VDMJ -verbose flag that sends detailed information to the VDMJ console.