Including and Excluding Project Files - overturetool/vdm-vscode GitHub Wiki

Ignoring 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).

Ordering Files

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.

Limiting External Files

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).