-
Notifications
You must be signed in to change notification settings - Fork 6
Including and Excluding Project Files
VDM VSCode projects do a depth-first search for files that match their dialect, i.e. *.vdmsl
, *.vdmpp
or *.vdmrt
. But in some cases, you may want to exclude individual files or folders from the search.
To do this, you can manually create a file called .vscode/vdmignore
in your project, and add a list of files and folders to ignore, one name per line. The filenames that match are relative to your project root. So for example:
ignoreme.vdmsl
**/temp
ignoredfolder
That will ignore a file called ignoreme.vdmsl
at the top level of the project, ignore the entire content of any subfolder called temp
and ignore everything within a top level folder called ignoredfolder
. The globbing syntax is defined here.
You can ignore files that are generated from external file formats, but in that case you should include the name of the extracted file, not the name of the external format file (e.g. design.docx.vdmsl
rather than design.docx
).
With extremely large specifications, the order in which modules or classes are parsed can make a big difference to the time it takes to type check the specification. The optimal order has the fewest forward references, so files early in the order should depend on as few of the others as possible, and files that follow them should only depend on definitions earlier in the order. This may be impossible to do perfectly, if files have mutual dependencies.
You can create a file called .vscode/ordering
which contains a list of relative project filenames (note, not glob patterns). If this file exists, then the parser will (a) only parse the files listed and (b) it will parse them in the order given. Even if the list is not optimal, or does have some forward references, creating an ordering file can still make a big performance improvement for very large projects.
Note that an ordering file defines the order of files rather than modules or classes. If you define more than one module or class within a single source file, the only way to change the ordering is to edit that file.
Complex projects may include a large number of documentation sources (like *.docx
or *.tex
) mixed in with VDM sources. By default, these will be regarded as external files (see here) - that is, they will be parsed to see whether they contain embedded VDM source. If they do not contain VDM source this is harmless, though if there are very many such files it will start to slow down the language server unnecessarily. The simplest way to avoid this performance hit is to locate all of the documentation files in a subfolder somewhere, and then add that subfolder to the .vscode/vdmignore
file.
In projects that cannot be restructured to have an ignorable subfolder, you can list all of the individual external files to ignore, but this is tedious and error prone, even with patterns. Therefore you can optionally create a file list called .vscode/externals
which explicitly includes just those external files and ignores any others. So this would be the (hopefully small) list of (say) *.docx
files that actually include VDM source that you want to include in the project. The externals
file can contain glob patterns (see above).
- Home
- Getting Started
- Editor Features
- Including and Excluding Project Files
- Interpretation and Debugging
- Including Libraries
- Proof Obligation Generation
- Combinatorial Testing
- Animated Usage Examples
- Worked AlarmSL Examples
- Extension Settings
- Changing VDMJ Properties
- Translation
- Coverage
- Dependency Graph
- Real-time Log Viewer
- Code Generation
- Remote Control
- External File Formats
- Annotation Output
- Using VDM Values in Java
- VS Code Live Share
- Design
- The Specification Language Server Protocol
- For Developers/Contributors